Yamaguchi Lean 4 Library
ProCGroups/ProC/Subgroups/Closed.lean
ProCGroups/ProC/Subgroups/Closed/Source

ProCGroups/ProC/Subgroups/Closed.lean

1import ProCGroups.ProC.InverseLimits.Limits
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/ProC/Subgroups/Closed.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/-- Closed-subgroup permanence for pro-`C` groups.
35The proof follows the standard finite-quotient argument: for an open normal subgroup `U` of the
36closed subgroup `H`, choose an ambient open normal subgroup `V` of `G` with `V ∩ H ≤ U`, identify
37`H / (V ∩ H)` with a subgroup of `G / V`, then pass to the quotient `H / U`.
39The proof uses ambient open-normal approximation and finite quotient comparison. -/
40theorem of_closedSubgroup
41 (hIso : FiniteGroupClass.IsomClosed C)
42 (hSub : FiniteGroupClass.SubgroupClosed C)
43 (_hQuot : FiniteGroupClass.QuotientClosed C)
44 (hG : IsProCGroup C G) (H : ClosedSubgroup G) :
45 IsProCGroup C ↥(H : Subgroup G) := by
46 refine ⟨IsProfiniteGroup.of_closedSubgroup (G := G) hG.isProfinite H, ?_⟩
47 intro W hW h1W
48 letI : CompactSpace G := IsProCGroup.compactSpace hG
49 letI : T2Space G := IsProCGroup.t2Space hG
50 letI : TotallyDisconnectedSpace G := IsProCGroup.totallyDisconnectedSpace hG
51 have hW_nhds : W ∈ 𝓝 (1 : H) := hW.mem_nhds h1W
52 rcases (mem_nhds_subtype (H : Set G) (1 : H) W).1 hW_nhds with
53 ⟨W₀, hW₀_nhds, hW₀W⟩
54 rcases mem_nhds_iff.mp hW₀_nhds with ⟨W', hW'W₀, hW'open, h1W'⟩
55 rcases hG.hasOpenNormalBasisInClass W' hW'open h1W' with
56 ⟨V, hVW', hCV⟩
57 let VH : OpenNormalSubgroup H :=
58 OpenNormalSubgroup.comap ((H : Subgroup G).subtype) continuous_subtype_val V
59 have hVHW : (((VH : Subgroup H) : Set H)) ⊆ W := by
60 intro x hx
61 exact hW₀W <| by
62 change x.1 ∈ W₀
63 exact hW'W₀ (hVW' hx)
64 let ψ : H →* G ⧸ (V : Subgroup G) :=
65 (QuotientGroup.mk' (V : Subgroup G)).comp ((H : Subgroup G).subtype)
66 have hRange : C ψ.range := hSub ψ.range hCV
67 have hKerEq : (VH : Subgroup H) = ψ.ker := by
68 ext x
69 constructor
70 · intro hx
71 simpa [MonoidHom.mem_ker, ψ] using
72 (QuotientGroup.eq_one_iff (N := (V : Subgroup G)) x.1).2 hx
73 · intro hx
74 exact (QuotientGroup.eq_one_iff (N := (V : Subgroup G)) x.1).1
75 (by simpa [MonoidHom.mem_ker, ψ] using hx)
76 have hQuotVH : C (H ⧸ (VH : Subgroup H)) := by
77 let e1 : H ⧸ (VH : Subgroup H) ≃* H ⧸ ψ.ker :=
78 QuotientGroup.quotientMulEquivOfEq hKerEq
79 exact hIso
80 ⟨(e1.trans (QuotientGroup.quotientKerEquivRange ψ)).symm⟩
81 hRange
82 exact ⟨VH, hVHW, hQuotVH⟩
84/-- Closed-subgroup permanence using an ordinary subgroup together with a closedness proof. -/
85theorem of_isClosed_subgroup
86 (hIso : FiniteGroupClass.IsomClosed C)
87 (hSub : FiniteGroupClass.SubgroupClosed C)
88 (hQuot : FiniteGroupClass.QuotientClosed C)
89 (hG : IsProCGroup C G) (H : Subgroup G) (hH : IsClosed (H : Set G)) :
90 IsProCGroup C H := by
91 exact ProCGroups.of_isClosed_subgroup_of_closedSubgroup
92 (G := G) (P := fun H => IsProCGroup C ↥H)
93 (of_closedSubgroup (C := C) hIso hSub hQuot hG) H hH
95/-- Closed-subgroup permanence for pro-`C` groups from a full formation package. -/
97 (hC : FiniteGroupClass.FullFormation C)
98 (hG : IsProCGroup C G) (H : ClosedSubgroup G) :
99 IsProCGroup C ↥(H : Subgroup G) :=
100 of_closedSubgroup hC.isomClosed hC.subgroupClosed hC.quotientClosed hG H
102/-- Closed-subgroup permanence in ordinary subgroup form from a full formation package. -/
104 (hC : FiniteGroupClass.FullFormation C)
105 (hG : IsProCGroup C G) (H : Subgroup G) (hH : IsClosed (H : Set G)) :
106 IsProCGroup C H :=
107 of_isClosed_subgroup hC.isomClosed hC.subgroupClosed hC.quotientClosed hG H hH
109/-- The range of a continuous homomorphism from a pro-`C` group to a Hausdorff topological group is
110again pro-`C`, with the induced subtype topology. -/
111theorem range
112 (hIso : FiniteGroupClass.IsomClosed C)
113 (hQuot : FiniteGroupClass.QuotientClosed C)
114 (hG : IsProCGroup C G)
115 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
116 (f : G →ₜ* H) :
117 IsProCGroup C f.toMonoidHom.range := by
118 letI : CompactSpace G := hG.compactSpace
119 let K : Subgroup G := f.toMonoidHom.ker
120 have hKclosed : IsClosed (K : Set G) := by
121 dsimp [K]
122 exact f.isClosed_ker
123 letI : K.Normal := by
124 dsimp [K]
125 infer_instance
126 have hQuotG : IsProCGroup C (G ⧸ K) :=
127 quotient_closedNormalSubgroup (C := C) hIso hQuot hG K hKclosed
128 have e : (G ⧸ K) ≃ₜ* f.toMonoidHom.range := by
130 exact IsProCGroup.ofContinuousMulEquiv (C := C) (G := G ⧸ K) hIso hQuot hQuotG e
132end IsProCGroup
134namespace ProCGroup
136/-- A closed subgroup of a `ProCGroup`, bundled as a `ClosedSubgroup`, is again a `ProCGroup`. -/
137theorem of_closedSubgroup
138 (ProC : ProCGroupPredicate.{u})
139 [ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
140 [ProC.DeterminedByFiniteQuotients]
141 [hG : ProCGroup ProC G] (H : ClosedSubgroup G) :
142 ProCGroup ProC ↥(H : Subgroup G) :=
143 ProCGroup.of_isProCGroup ProC ↥(H : Subgroup G)
144 (IsProCGroup.of_closedSubgroup
145 ProC.finiteQuotientIsomClosed
146 ProC.finiteQuotientHereditary.subgroupClosed
147 ProC.finiteQuotientQuotientClosed
148 hG.isProCGroup H)
150/-- A closed subgroup of a `ProCGroup` is again a `ProCGroup`.
152The finite quotient input is the standard Melnikov-formation package together with hereditary
153subgroup closure. -/
154theorem of_isClosed_subgroup
155 (ProC : ProCGroupPredicate.{u})
156 [ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
157 [ProC.DeterminedByFiniteQuotients]
158 [hG : ProCGroup ProC G] (H : Subgroup G) (hH : IsClosed (H : Set G)) :
159 ProCGroup ProC H :=
160 ProCGroup.of_isProCGroup ProC H
161 (IsProCGroup.of_isClosed_subgroup
162 ProC.finiteQuotientIsomClosed
163 ProC.finiteQuotientHereditary.subgroupClosed
164 ProC.finiteQuotientQuotientClosed
165 hG.isProCGroup H hH)
167/-- A quotient by a closed normal subgroup of a `ProCGroup` is again a
169theorem quotient_closedNormalSubgroup
170 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientMelnikovFormation]
171 [ProC.DeterminedByFiniteQuotients]
172 [hG : ProCGroup ProC G] (K : Subgroup G) [K.Normal] (hK : IsClosed (K : Set G)) :
173 ProCGroup ProC (G ⧸ K) :=
174 ProCGroup.of_isProCGroup ProC (G ⧸ K)
176 ProC.finiteQuotientIsomClosed
177 ProC.finiteQuotientQuotientClosed
178 hG.isProCGroup K hK)
180/-- The range of a continuous homomorphism from a `ProCGroup` to a Hausdorff topological group is
181again a `ProCGroup`, with the induced subtype topology. -/
182theorem range
183 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation]
184 [ProC.DeterminedByFiniteQuotients]
185 [hG : ProCGroup ProC G]
186 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
187 (f : G →ₜ* H) :
188 ProCGroup ProC f.toMonoidHom.range :=
189 ProCGroup.of_isProCGroup ProC f.toMonoidHom.range
190 (IsProCGroup.range
191 ProC.finiteQuotientIsomClosed
192 ProC.finiteQuotientQuotientClosed
193 hG.isProCGroup f)
195/-- A Hausdorff continuous quotient of a `ProCGroup` is again a `ProCGroup`. -/
196theorem of_surjective
197 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation]
198 [ProC.DeterminedByFiniteQuotients]
199 [hG : ProCGroup ProC G]
200 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
201 (f : G →ₜ* H) (hf : Function.Surjective f) :
202 ProCGroup ProC H := by
203 let R : Subgroup H := f.toMonoidHom.range
204 have hR : ProCGroup ProC R := range (ProC := ProC) (G := G) f
205 letI : ProCGroup ProC R := hR
206 have hcompactR : CompactSpace R := hR.isProCGroup.compactSpace
207 letI : CompactSpace R := hcompactR
208 let e : R ≃ₜ* H :=
209 ContinuousMulEquiv.ofBijectiveCompactToT2 (Subgroup.subtype R)
210 continuous_subtype_val
211 ⟨by
212 intro x y hxy
213 exact Subtype.ext hxy,
214 by
215 intro h
216 rcases hf h with ⟨g, rfl⟩
217 exact ⟨⟨f g, ⟨g, rfl⟩⟩, rfl⟩⟩
218 exact ProCGroup.ofContinuousMulEquiv (G := R) ProC e
222namespace IsProCGroup
224variable {E : Type u} [Group E] [TopologicalSpace E] [IsTopologicalGroup E]
226/-- Extension permanence for pro-`C` groups.
228We assume `E` is already profinite; the `pro-`C` conclusion is then obtained by checking each
229open-normal finite quotient of `E`.
231Extensions of pro-`C` groups remain pro-`C` once the ambient group is known to be profinite. -/
232theorem extension
233 (hIso : FiniteGroupClass.IsomClosed C)
234 (hQuot : FiniteGroupClass.QuotientClosed C)
235 (hExt : FiniteGroupClass.ExtensionClosed C)
237 (K : Subgroup E) [K.Normal]
238 (hK : IsProCGroup C K) (hQ : IsProCGroup C (E ⧸ K)) :
239 IsProCGroup C E := by
240 refine IsProCGroup.of_allOpenNormalQuotients (C := C) hE ?_
241 intro U
242 letI : CompactSpace E := IsProfiniteGroup.compactSpace hE
243 letI : T2Space E := IsProfiniteGroup.t2Space hE
244 letI : CompactSpace (E ⧸ K) := IsProfiniteGroup.compactSpace hQ.isProfinite
245 letI : T2Space (E ⧸ K) := IsProfiniteGroup.t2Space hQ.isProfinite
246 letI : CompactSpace K := IsProfiniteGroup.compactSpace hK.isProfinite
247 letI : T2Space K := IsProfiniteGroup.t2Space hK.isProfinite
248 let M : Subgroup E := K ⊔ (U : Subgroup E)
249 let Wsub : Subgroup (E ⧸ K) := Subgroup.map (QuotientGroup.mk' K) M
250 have hWclosed : IsClosed (Wsub : Set (E ⧸ K)) := by
251 have hMclosed : IsClosed (M : Set E) := by
252 have hMopen : IsOpen (M : Set E) := by
253 exact Subgroup.isOpen_of_openSubgroup M (show (U : Subgroup E) ≤ M from le_sup_right)
254 exact Subgroup.isClosed_of_isOpen M hMopen
255 have hMcompact : IsCompact (M : Set E) := hMclosed.isCompact
256 have hcont : Continuous (QuotientGroup.mk' K : E → E ⧸ K) := continuous_quotient_mk'
257 have himage : IsCompact ((QuotientGroup.mk' K) '' (M : Set E)) := hMcompact.image hcont
258 have hEq : (QuotientGroup.mk' K) '' (M : Set E) = (Wsub : Set (E ⧸ K)) := by
259 ext x
260 simp only [QuotientGroup.mk'_apply, mem_image, SetLike.mem_coe, Subgroup.coe_map, M, Wsub]
261 rw [← hEq]
262 exact himage.isClosed
263 have hWfinite : Finite ((E ⧸ K) ⧸ Wsub) := by
264 have hMopen : IsOpen (M : Set E) := by
265 exact Subgroup.isOpen_of_openSubgroup M (show (U : Subgroup E) ≤ M from le_sup_right)
266 have hMfinite : Finite (E ⧸ M) :=
267 (subgroup_isOpen_iff_isClosed_finite_quotient (G := E) (U := M)).1 hMopen |>.2
268 let e : (E ⧸ K) ⧸ Wsub ≃* E ⧸ M := by
269 simpa [Wsub, M, Subgroup.map_sup] using
270 (QuotientGroup.quotientQuotientEquivQuotient K M (show K ≤ M from le_sup_left))
271 exact Finite.of_injective e e.injective
272 have hWopen : IsOpen (Wsub : Set (E ⧸ K)) :=
273 (subgroup_isOpen_iff_isClosed_finite_quotient (G := E ⧸ K) (U := Wsub)).2
274 ⟨hWclosed, hWfinite⟩
275 letI : Wsub.Normal := by
276 dsimp [Wsub, M]
277 have hMnormal : M.Normal := by infer_instance
278 exact Subgroup.Normal.map hMnormal (QuotientGroup.mk' K) (QuotientGroup.mk'_surjective K)
279 let W : OpenNormalSubgroup (E ⧸ K) :=
280 { toOpenSubgroup := ⟨Wsub, hWopen⟩
281 isNormal' := inferInstance }
282 have hQuotM : C (E ⧸ M) := by
283 let e : (E ⧸ K) ⧸ (W : Subgroup (E ⧸ K)) ≃* E ⧸ M := by
284 simpa [W, Wsub, M, Subgroup.map_sup] using
285 (QuotientGroup.quotientQuotientEquivQuotient K M (show K ≤ M from le_sup_left))
286 exact hIso ⟨e⟩
287 (IsProCGroup.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
288 hIso hQuot hQ W)
289 let KU : OpenNormalSubgroup K :=
290 OpenNormalSubgroup.comap (K.subtype) continuous_subtype_val U
291 let ψ : K →* E ⧸ (U : Subgroup E) :=
292 (QuotientGroup.mk' (U : Subgroup E)).comp K.subtype
293 have hKerEq : (KU : Subgroup K) = ψ.ker := by
294 ext x
295 constructor
296 · intro hx
297 simpa [MonoidHom.mem_ker, KU, ψ] using
298 (QuotientGroup.eq_one_iff (N := (U : Subgroup E)) x.1).2 hx
299 · intro hx
300 exact (QuotientGroup.eq_one_iff (N := (U : Subgroup E)) x.1).1
301 (by simpa [MonoidHom.mem_ker, KU, ψ] using hx)
302 have hKernelC : C ψ.range := by
303 have hQuotKU : C (K ⧸ (KU : Subgroup K)) :=
304 IsProCGroup.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
305 hIso hQuot hK KU
306 let e1 : K ⧸ (KU : Subgroup K) ≃* K ⧸ ψ.ker :=
307 QuotientGroup.quotientMulEquivOfEq hKerEq
308 exact hIso ⟨e1.trans (QuotientGroup.quotientKerEquivRange ψ)⟩ hQuotKU
309 let L : Subgroup (E ⧸ (U : Subgroup E)) := Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) K
310 have hRangeEq : ψ.range = L := by
311 ext x
312 simp only [MonoidHom.mem_range, MonoidHom.coe_comp, QuotientGroup.coe_mk', Subgroup.coe_subtype,
313 Function.comp_apply, Subtype.exists, exists_prop, Subgroup.mem_map, QuotientGroup.mk'_apply, ψ, L]
314 have hLC : C L := by
315 exact hIso ⟨MulEquiv.subgroupCongr hRangeEq⟩ hKernelC
316 have hMapUbot : Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) (U : Subgroup E) = ⊥ := by
317 ext x
318 constructor
319 · intro hx
320 rcases (Subgroup.mem_map).1 hx with ⟨u, hu, hux⟩
321 rw [Subgroup.mem_bot]
322 have hu1 : QuotientGroup.mk' (U : Subgroup E) u = 1 :=
323 (QuotientGroup.eq_one_iff (N := (U : Subgroup E)) u).2 hu
324 exact hux.symm.trans hu1
325 · intro hx
326 rcases Subgroup.mem_bot.1 hx with rfl
327 exact ⟨1, U.one_mem, by simp only [QuotientGroup.mk'_apply, QuotientGroup.mk_one]⟩
328 have hMapM : Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) M = L := by
329 calc
330 Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) M
331 = Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) K ⊔
332 Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) (U : Subgroup E) := by
333 simp only [Subgroup.map_sup, QuotientGroup.map_mk'_self, bot_le, sup_of_le_left, M]
334 _ = L ⊔ ⊥ := by simp only [hMapUbot, bot_le, sup_of_le_left, L]
335 _ = L := by simp only [bot_le, sup_of_le_left]
336 have hQuotL : C ((E ⧸ (U : Subgroup E)) ⧸ L) := by
337 let e0 : (E ⧸ (U : Subgroup E)) ⧸ L ≃* (E ⧸ (U : Subgroup E)) ⧸
338 Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) M :=
339 QuotientGroup.quotientMulEquivOfEq hMapM.symm
340 let e1 : (E ⧸ (U : Subgroup E)) ⧸
341 Subgroup.map (QuotientGroup.mk' (U : Subgroup E)) M ≃* E ⧸ M :=
342 QuotientGroup.quotientQuotientEquivQuotient (U : Subgroup E) M
343 (show (U : Subgroup E) ≤ M from le_sup_right)
344 exact hIso ⟨(e0.trans e1).symm⟩ hQuotM
345 letI : L.Normal := by
346 dsimp [L]
347 exact Subgroup.Normal.map inferInstance (QuotientGroup.mk' (U : Subgroup E))
348 (QuotientGroup.mk'_surjective (U : Subgroup E))
349 exact hExt L hLC hQuotL
351end IsProCGroup
353end
355end ProCGroups.ProC