CompletedGroupAlgebra/UniversalProperty/FiniteQuotient.lean
1import CompletedGroupAlgebra.UniversalProperty.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/UniversalProperty/FiniteQuotient.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Finite-quotient and discrete-target lifts
14This module proves the finite-quotient form of the universal property: maps to finite discrete targets are determined by sufficiently deep finite stages.
15-/
17open scoped Topology
19namespace CompletedGroupAlgebra
21noncomputable section
23open ProCGroups
24open ProCGroups.ProC
25open ProCGroups.InverseSystems
26open ProCGroups.Completion
28universe u v w
30variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
31variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
33/-- Finite-quotient construction used in Lemma 5.3.5(d): a map on one finite quotient
34`G/U` extends linearly and continuously from `[[RG]]`. -/
36 (U : CompletedGroupAlgebraIndex G) (N : Type (max u v))
37 [AddCommGroup N] [TopologicalSpace N] [Module R N] [ContinuousAdd N]
38 [ContinuousSMul R N] (f : CompletedGroupAlgebraQuotient G U → N) :
39 Carrier R G →L[R] N := by
40 letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
41 (completedGroupAlgebraSystem R G).topologicalSpace U
42 exact (finiteGroupAlgebraLift R (CompletedGroupAlgebraQuotient G U) N f).comp
45/-- The finite-quotient lift has the prescribed value on completed group-like elements. -/
46@[simp]
48 (U : CompletedGroupAlgebraIndex G) (N : Type (max u v))
49 [AddCommGroup N] [TopologicalSpace N] [Module R N] [ContinuousAdd N]
50 [ContinuousSMul R N] (f : CompletedGroupAlgebraQuotient G U → N) (g : G) :
51 completedGroupAlgebraLiftOfFiniteQuotient (R := R) (G := G) U N f
52 (completedGroupAlgebraOf R G g) =
54 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) := by
55 letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
56 (completedGroupAlgebraSystem R G).topologicalSpace U
57 change finiteGroupAlgebraLift R (CompletedGroupAlgebraQuotient G U) N f
58 (completedGroupAlgebraProjection R G U (completedGroupAlgebraOf R G g)) =
60 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g)
62 exact finiteGroupAlgebraLift_apply_of R (CompletedGroupAlgebraQuotient G U) N f
64 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g)
66/-- If a continuous target map already factors through one finite quotient `G/U`, the
69 (hG : ProCGroups.IsProfiniteGroup G)
70 (N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
71 [ContinuousAdd N] [ContinuousSMul R N] [T2Space N]
72 (U : CompletedGroupAlgebraIndex G) (f : G → N)
73 (fbar : CompletedGroupAlgebraQuotient G U → N)
74 (hfac : ∀ g : G,
76 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) = f g) :
77 ∃! F : Carrier R G →L[R] N,
78 ∀ g : G, F (completedGroupAlgebraOf R G g) = f g := by
79 let F := completedGroupAlgebraLiftOfFiniteQuotient (R := R) (G := G) U N fbar
80 refine ⟨F, ?_, ?_⟩
81 · intro g
83 · intro K hK
84 apply completedGroupAlgebraContinuousLinearMap_ext_of_basis (R := R) (G := G) hG
85 intro g
86 rw [completedGroupAlgebraLiftOfFiniteQuotient_apply_of, hfac, hK]
88/-- A continuous map from a profinite group to a discrete space is unchanged on the cosets of
89some finite open normal quotient. This is the topological factorization input in the book proof of
90Lemma 5.3.5(d). -/
92 (hG : ProCGroups.IsProfiniteGroup G)
93 (N : Type (max u v)) [TopologicalSpace N] [DiscreteTopology N]
94 (f : G → N) (hf : Continuous f) :
95 ∃ U : CompletedGroupAlgebraIndex G, ∃ fbar : CompletedGroupAlgebraQuotient G U → N,
96 ∀ g : G,
98 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) = f g := by
99 letI : CompactSpace G := ProCGroups.IsProfiniteGroup.compactSpace hG
100 let T : Set (G × G) := {p | f p.1 = f p.2}
101 have hTopen : IsOpen T := by
102 have hpair : Continuous fun p : G × G => (f p.1, f p.2) :=
103 (hf.comp continuous_fst).prodMk (hf.comp continuous_snd)
104 change IsOpen ((fun p : G × G => (f p.1, f p.2)) ⁻¹'
105 {q : N × N | q.1 = q.2})
106 exact hpair.isOpen_preimage _ (isOpen_discrete _)
107 let A : Set (G × G) := {p | f p.1 = f (p.1 * p.2)}
108 have hAopen : IsOpen A := by
109 have hmul : Continuous fun p : G × G => (p.1, p.1 * p.2) :=
110 continuous_fst.prodMk (continuous_fst.mul continuous_snd)
111 change IsOpen ((fun p : G × G => (p.1, p.1 * p.2)) ⁻¹' T)
112 exact hTopen.preimage hmul
113 have hcontains : (Set.univ : Set G) ×ˢ ({1} : Set G) ⊆ A := by
114 rintro ⟨g, u⟩ ⟨_hg, hu⟩
115 change u = 1 at hu
116 change f g = f (g * u)
117 rw [hu, mul_one]
118 rcases generalized_tube_lemma (s := (Set.univ : Set G)) isCompact_univ
119 (t := ({1} : Set G)) isCompact_singleton hAopen hcontains with
120 ⟨W, V, _hWopen, hVopen, hWuniv, h1V, hWV⟩
121 have hVone : (1 : G) ∈ V := h1V (by simp only [Set.mem_singleton_iff])
122 have hProC : IsProCGroup ProCGroups.FiniteGroupClass.allFinite G :=
123 (isProC_allFinite_iff_isProfiniteGroup (G := G)).2 hG
124 rcases hProC.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hVopen hVone with
125 ⟨U0, hU0V⟩
126 let U : CompletedGroupAlgebraIndex G := OrderDual.toDual U0
127 let fbar : CompletedGroupAlgebraQuotient G U → N := Quotient.lift f (by
128 intro a b hab
129 have habU : a⁻¹ * b ∈ (U0.1 : Subgroup G) :=
130 (QuotientGroup.leftRel_apply).1 hab
131 have habV : a⁻¹ * b ∈ V := hU0V habU
132 have hA : (a, a⁻¹ * b) ∈ A :=
133 hWV ⟨hWuniv (Set.mem_univ a), habV⟩
134 simpa [A, mul_assoc] using hA)
135 refine ⟨U, fbar, ?_⟩
136 intro g
137 rfl
139/-- Discrete-target form of Lemma 5.3.5(d): a continuous map from the profinite group `G` to a
140discrete `R`-module extends uniquely to a continuous `R`-linear map out of `[[RG]]`. -/
142 (hG : ProCGroups.IsProfiniteGroup G)
143 (N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
144 [ContinuousAdd N] [ContinuousSMul R N] [DiscreteTopology N]
145 (f : G → N) (hf : Continuous f) :
146 ∃! F : Carrier R G →L[R] N,
147 ∀ g : G, F (completedGroupAlgebraOf R G g) = f g := by
148 letI : T2Space N := inferInstance
150 (G := G) hG N f hf with
151 ⟨U, fbar, hfac⟩
152 exact completedGroupAlgebra_existsUnique_lift_of_factors (R := R) (G := G) hG N
153 U f fbar hfac
155/-- The chosen discrete-target extension in Lemma 5.3.5(d). -/
157 (hG : ProCGroups.IsProfiniteGroup G)
158 (N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
159 [ContinuousAdd N] [ContinuousSMul R N] [DiscreteTopology N]
160 (f : G → N) (hf : Continuous f) :
161 Carrier R G →L[R] N :=
162 Classical.choose
164 (R := R) (G := G) hG N f hf)
166/-- The chosen discrete-target lift has the prescribed value on completed group-like elements. -/
167@[simp]
169 (hG : ProCGroups.IsProfiniteGroup G)
170 (N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
171 [ContinuousAdd N] [ContinuousSMul R N] [DiscreteTopology N]
172 (f : G → N) (hf : Continuous f) (g : G) :
174 (R := R) (G := G) hG N f hf
175 (completedGroupAlgebraOf R G g) = f g := by
176 exact (Classical.choose_spec
178 (R := R) (G := G) hG N f hf)).1 g
179end