ProCGroups/ProC/InverseLimits/FiniteQuotients.lean
1import ProCGroups.ProC.GroupPredicates.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/ProC/InverseLimits/FiniteQuotients.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Pro-C groups and open normal quotients
14Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.
15-/
17open Set
18open scoped Topology Pointwise
20namespace ProCGroups.ProC
22universe u v
24open InverseSystems
26section
28variable {C : FiniteGroupClass.{u}}
29variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31namespace IsProCGroup
33/-- Any finite discrete group already lying in the class `C` is pro-`C`. -/
34theorem of_finite_discrete (hquot : FiniteGroupClass.QuotientClosed C)
35 [Finite G] [DiscreteTopology G] (hCG : C G) : IsProCGroup C G := by
36 refine IsProCGroup.of_allOpenNormalQuotients (C := C)
37 (G := G) (ProCGroups.IsProfiniteGroup.of_finite_discrete G) ?_
38 intro U
39 exact hquot (N := (U : Subgroup G)) hCG
41/-- If `G` is pro-`C` and `C` is closed
42under quotients, then every quotient of `G` by an open normal subgroup is again pro-`C`. -/
43theorem quotient_openNormalSubgroup
44 (hForm : FiniteGroupClass.Formation C)
45 (hG : IsProCGroup C G) (U : OpenNormalSubgroup G) :
46 IsProCGroup C (G ⧸ (U : Subgroup G)) := by
47 letI : Finite (G ⧸ (U : Subgroup G)) := hG.finite_quotient U
48 letI : DiscreteTopology (G ⧸ (U : Subgroup G)) :=
49 QuotientGroup.discreteTopology (openNormalSubgroup_isOpen (G := G) U)
50 exact IsProCGroup.of_finite_discrete (C := C) (G := G ⧸ (U : Subgroup G))
51 hForm.quotientClosed (hG.quotient_mem hForm U)
53/-- Quotients by open normal subgroups in the class-indexing family are pro-`C`. -/
54theorem quotient_openNormalSubgroupInClass
55 (hquot : FiniteGroupClass.QuotientClosed C)
56 (hG : IsProCGroup C G) (U : OpenNormalSubgroupInClass C G) :
57 IsProCGroup C (G ⧸ (U.1 : Subgroup G)) :=
58 by
59 letI : Finite (G ⧸ (U.1 : Subgroup G)) := hG.finite_quotient U.1
60 letI : DiscreteTopology (G ⧸ (U.1 : Subgroup G)) :=
61 QuotientGroup.discreteTopology (openNormalSubgroup_isOpen (G := G) U.1)
62 exact IsProCGroup.of_finite_discrete (C := C)
63 (G := G ⧸ (U.1 : Subgroup G)) hquot U.2
65-- Product permanence for pro-`C` groups reduces an open normal subgroup of a product to a finite
66-- product of open normal subgroups, then uses formation closure for the resulting finite quotient.
67/-- Arbitrary products of pro-`C` groups remain pro-`C` when `C` is a formation. -/
68theorem pi {α : Type u} {β : α → Type u}
69 [∀ a, Group (β a)] [∀ a, TopologicalSpace (β a)] [∀ a, IsTopologicalGroup (β a)]
70 (hForm : FiniteGroupClass.Formation C)
71 (hβ : ∀ a, IsProCGroup C (β a)) :
72 IsProCGroup C ((a : α) → β a) := by
73 classical
74 let G : Type u := (a : α) → β a
75 letI : Group G := by
76 dsimp [G]
77 infer_instance
78 letI : TopologicalSpace G := by
79 dsimp [G]
80 infer_instance
81 letI : IsTopologicalGroup G := by
82 dsimp [G]
83 infer_instance
84 have hProf : IsProfiniteGroup G := by
85 letI : ∀ a, CompactSpace (β a) := fun a => IsProCGroup.compactSpace (hβ a)
86 letI : ∀ a, T2Space (β a) := fun a => IsProCGroup.t2Space (hβ a)
87 letI : ∀ a, TotallyDisconnectedSpace (β a) := fun a =>
88 IsProCGroup.totallyDisconnectedSpace (hβ a)
89 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
90 refine IsProCGroup.of_allOpenNormalQuotients (C := C) (G := G) hProf ?_
91 intro U
92 letI : CompactSpace G := IsProfiniteGroup.compactSpace hProf
93 letI : T2Space G := IsProfiniteGroup.t2Space hProf
94 let hUnhds : ((U : Subgroup G) : Set G) ∈ 𝓝 (1 : G) := by
95 exact U.toOpenSubgroup.isOpen'.mem_nhds U.one_mem'
96 rcases mem_nhds_iff.mp hUnhds with ⟨W, hWU, hWopen, h1W⟩
97 rcases (isOpen_pi_iff.mp hWopen) (1 : G) h1W with ⟨J, WJ, hJ1, hJ2⟩
98 let V : ∀ j : J, OpenNormalSubgroup (β j) := fun j =>
99 Classical.choose <|
100 IsProCGroup.hasOpenNormalBasisInClass (C := C) (G := β j) (hβ j) (WJ j)
101 (hJ1 j j.property).1 (hJ1 j j.property).2
102 have hVsub : ∀ j : J, ((V j : Subgroup (β j)) : Set (β j)) ⊆ WJ j := fun j =>
103 (Classical.choose_spec <|
104 IsProCGroup.hasOpenNormalBasisInClass (C := C) (G := β j) (hβ j) (WJ j)
105 (hJ1 j j.property).1 (hJ1 j j.property).2).1
106 have hVquot : ∀ j : J, C (β j ⧸ (V j : Subgroup (β j))) := fun j =>
107 (Classical.choose_spec <|
108 IsProCGroup.hasOpenNormalBasisInClass (C := C) (G := β j) (hβ j) (WJ j)
109 (hJ1 j j.property).1 (hJ1 j j.property).2).2
110 let M : Subgroup G :=
111 iInf fun j : J =>
112 ((OpenNormalSubgroup.comap
113 ({ toFun := fun g : G => g j.1
114 map_one' := rfl
115 map_mul' := by intro x y; rfl } : G →* β j.1)
116 (continuous_apply j.1) (V j) : OpenNormalSubgroup G) : Subgroup G)
117 letI : M.Normal := by
118 exact Subgroup.normal_iInf_normal fun j : J =>
119 (OpenNormalSubgroup.comap
120 ({ toFun := fun g : G => g j.1
121 map_one' := rfl
122 map_mul' := by intro x y; rfl } : G →* β j.1)
123 (continuous_apply j.1) (V j)).isNormal'
124 have hMU : M ≤ (U : Subgroup G) := by
125 intro x hx
126 apply hWU
127 apply hJ2
128 intro j hj
129 have hxall :
130 ∀ k : J,
131 x ∈ OpenNormalSubgroup.comap
132 ({ toFun := fun g : G => g k.1
133 map_one' := rfl
134 map_mul' := by intro a b; rfl } : G →* β k.1)
135 (continuous_apply k.1) (V k) := by
136 simpa [M, Subgroup.mem_iInf] using hx
137 have hxj :
138 x ∈ OpenNormalSubgroup.comap
139 ({ toFun := fun g : G => g j
140 map_one' := rfl
141 map_mul' := by intro a b; rfl } : G →* β j)
142 (continuous_apply j) (V ⟨j, hj⟩) :=
143 hxall ⟨j, hj⟩
144 have hxj' : x j ∈ (V ⟨j, hj⟩ : Subgroup (β j)) := by
145 simpa using hxj
146 exact hVsub ⟨j, hj⟩ hxj'
147 let φ : G →* ∀ j : J, β j ⧸ (V j : Subgroup (β j)) :=
148 { toFun := fun g j => QuotientGroup.mk' (V j : Subgroup (β j)) (g j)
149 map_one' := by funext j; rfl
150 map_mul' := by intro x y; funext j; rfl }
151 have hProd : C (∀ j : J, β j ⧸ (V j : Subgroup (β j))) := by
152 exact FiniteGroupClass.Formation.finiteProductClosed (C := C) hForm hVquot
153 have hRange : C φ.range := by
154 let ψ : φ.range →* ∀ j : J, β j ⧸ (V j : Subgroup (β j)) :=
155 φ.range.subtype
156 have hψinj : Function.Injective ψ := Subtype.coe_injective
157 have hψsurj : ∀ j : J, Function.Surjective fun x : φ.range => ψ x j := by
158 intro j y
159 rcases QuotientGroup.mk'_surjective (V j : Subgroup (β j)) y with ⟨xj, rfl⟩
160 let g : G := Function.update 1 j.1 xj
161 refine ⟨⟨φ g, ⟨g, rfl⟩⟩, ?_⟩
162 simp only [QuotientGroup.mk'_apply, MonoidHom.coe_mk, OneHom.coe_mk, Subgroup.subtype_apply,
163 Function.update_self, φ, ψ, g]
164 exact hForm.finiteSubdirectProductClosed ψ hψinj hψsurj hVquot
165 have hKerEq : M = φ.ker := by
166 ext x
167 constructor
168 · intro hx
169 have hxM : ∀ j : J, x j.1 ∈ (V j : Subgroup (β j)) := by
170 simpa [M, Subgroup.mem_iInf] using hx
171 change (fun j : J => QuotientGroup.mk' (V j : Subgroup (β j)) (x j.1)) = 1
172 funext j
173 exact (QuotientGroup.eq_one_iff (N := (V j : Subgroup (β j))) (x j.1)).2 (hxM j)
174 · intro hx
175 have hxker :
176 (fun j : J => QuotientGroup.mk' (V j : Subgroup (β j)) (x j.1)) = 1 := by
177 simpa [MonoidHom.mem_ker, φ] using hx
178 have hxM : ∀ j : J, x j.1 ∈ (V j : Subgroup (β j)) := by
179 intro j
180 exact (QuotientGroup.eq_one_iff (N := (V j : Subgroup (β j))) (x j.1)).1
181 (congrArg (fun f : (j : J) → β j ⧸ (V j : Subgroup (β j)) => f j) hxker)
182 simpa [M, Subgroup.mem_iInf] using hxM
183 have hQuotM : C (G ⧸ M) := by
184 let e1 : G ⧸ M ≃* G ⧸ φ.ker :=
185 QuotientGroup.quotientMulEquivOfEq hKerEq
186 exact hForm.isomClosed
187 ⟨(e1.trans (QuotientGroup.quotientKerEquivRange φ)).symm⟩
188 hRange
189 have hQuotU' :
190 C ((G ⧸ M) ⧸ Subgroup.map (QuotientGroup.mk' M) (U : Subgroup G)) := by
191 exact hForm.quotientClosed
192 (N := Subgroup.map (QuotientGroup.mk' M) (U : Subgroup G)) hQuotM
193 exact hForm.isomClosed
194 ⟨QuotientGroup.quotientQuotientEquivQuotient M (U : Subgroup G) hMU⟩
195 hQuotU'
197/-- Pro-`C` is preserved by continuous multiplicative equivalences. -/
198theorem ofContinuousMulEquiv {H : Type u} [Group H] [TopologicalSpace H]
199 [IsTopologicalGroup H]
200 (hIso : FiniteGroupClass.IsomClosed C)
201 (hQuot : FiniteGroupClass.QuotientClosed C)
202 (hG : IsProCGroup C G) (e : G ≃ₜ* H) :
203 IsProCGroup C H := by
204 letI : CompactSpace G := IsProCGroup.compactSpace hG
205 letI : T2Space G := IsProCGroup.t2Space hG
206 letI : TotallyDisconnectedSpace G := IsProCGroup.totallyDisconnectedSpace hG
207 letI : CompactSpace H := e.toHomeomorph.compactSpace
208 letI : T2Space H := e.toHomeomorph.t2Space
209 letI : TotallyDisconnectedSpace H := e.toHomeomorph.totallyDisconnectedSpace
210 refine IsProCGroup.of_allOpenNormalQuotients (C := C) (G := H)
211 ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩ ?_
212 intro U
213 let V : OpenNormalSubgroup G :=
214 OpenNormalSubgroup.comap
215 (e.toMulEquiv.toMonoidHom : G →* H)
216 e.continuous
217 U
218 have hquotV : C (G ⧸ (V : Subgroup G)) :=
219 IsProCGroup.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
220 hIso hQuot hG V
221 let φ : G ⧸ (V : Subgroup G) →* H ⧸ (U : Subgroup H) :=
222 QuotientGroup.map _ _ (e.toMulEquiv.toMonoidHom) <| by
223 intro g hg
224 change e g ∈ (U : Subgroup H)
225 simpa [V, OpenNormalSubgroup.toSubgroup_comap] using hg
226 have hφinj : Function.Injective φ := by
227 intro x y hxy
228 rcases QuotientGroup.mk'_surjective (V : Subgroup G) x with ⟨gx, rfl⟩
229 rcases QuotientGroup.mk'_surjective (V : Subgroup G) y with ⟨gy, rfl⟩
230 apply QuotientGroup.eq.2
231 change e (gx⁻¹ * gy) ∈ (U : Subgroup H)
233 simpa [φ] using hxy)
234 have hφsurj : Function.Surjective φ := by
235 intro x
236 rcases QuotientGroup.mk'_surjective (U : Subgroup H) x with ⟨h, rfl⟩
237 refine ⟨QuotientGroup.mk' (V : Subgroup G) (e.symm h), ?_⟩
238 change QuotientGroup.mk' (U : Subgroup H) (e (e.symm h)) = QuotientGroup.mk' (U : Subgroup H) h
239 simp only [ContinuousMulEquiv.apply_symm_apply, QuotientGroup.mk'_apply]
240 exact hIso ⟨MulEquiv.ofBijective φ ⟨hφinj, hφsurj⟩⟩ hquotV
242end IsProCGroup
246/-- A finite discrete group in the induced finite quotient class is a bundled `ProCGroup`. -/
247theorem of_finite_discrete
248 (ProC : ProCGroupPredicate.{u})
249 [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
250 {Q : Type u} [Group Q] [TopologicalSpace Q]
251 [Finite Q] [DiscreteTopology Q]
252 (hQ : ProC.finiteQuotientClass Q) :
254 ProCGroup.of_isProCGroup ProC Q
255 (IsProCGroup.of_finite_discrete
256 (C := ProC.finiteQuotientClass) ProC.finiteQuotientQuotientClosed hQ)
258/-- Transport a bundled `ProCGroup` structure across a continuous multiplicative equivalence. -/
259theorem ofContinuousMulEquiv
260 (ProC : ProCGroupPredicate.{u})
261 [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
262 {G H : Type u}
263 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
264 [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
267 ProCGroup.of_isProCGroup ProC H
268 (IsProCGroup.ofContinuousMulEquiv
269 (C := ProC.finiteQuotientClass)
270 ProC.finiteQuotientIsomClosed ProC.finiteQuotientQuotientClosed hG.isProCGroup e)
272/-- Products of bundled `ProCGroup`s are bundled `ProCGroup`s. -/
273theorem pi
274 (ProC : ProCGroupPredicate.{u})
275 [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
276 {α : Type u} {β : α → Type u}
277 [∀ a, Group (β a)] [∀ a, TopologicalSpace (β a)]
278 [∀ a, IsTopologicalGroup (β a)]
281 ProCGroup.of_isProCGroup ProC ((a : α) → β a)
282 (IsProCGroup.pi
283 (C := ProC.finiteQuotientClass)
284 ProC.finiteQuotientFormation
285 (fun a => (hβ a).isProCGroup))
287/-- Open normal quotients of a bundled `ProCGroup` are bundled `ProCGroup`s. -/
288theorem quotient_openNormalSubgroup
289 (ProC : ProCGroupPredicate.{u})
290 [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
293 ProCGroup.of_isProCGroup ProC (G ⧸ (U : Subgroup G))
294 (IsProCGroup.quotient_openNormalSubgroup
295 ProC.finiteQuotientFormation hG.isProCGroup U)
297/-- Open-normal-in-class quotients of a bundled `ProCGroup` are bundled `ProCGroup`s. -/
298theorem quotient_openNormalSubgroupInClass
299 (ProC : ProCGroupPredicate.{u})
300 [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
301 [hG : ProCGroup ProC G] (U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G) :
303 quotient_openNormalSubgroup (G := G) ProC U.1
307/-- Specialization of `IsProCGroup` to the class of all finite groups: this is exactly
308profiniteness. -/
310 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
311 IsProCGroup FiniteGroupClass.allFinite G ↔ IsProfiniteGroup G := by
312 constructor
313 · intro hG
314 exact hG.isProfinite
315 · intro hG
316 refine ⟨hG, ?_⟩
317 intro W hW h1W
318 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
319 letI : T2Space G := IsProfiniteGroup.t2Space hG
320 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
321 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hW h1W with ⟨U, hUW⟩
322 exact ⟨U, hUW, openNormalSubgroup_finiteQuotient (G := G) U⟩
324end
326end ProCGroups.ProC