Yamaguchi Lean 4 Library
ProCGroups/ProC/OpenNormalSubgroups/ProCGroup.lean
ProCGroups/ProC/OpenNormalSubgroups/ProCGroup/Source

ProCGroups/ProC/OpenNormalSubgroups/ProCGroup.lean

1import ProCGroups.FiniteGroups.AllFinite
2import ProCGroups.ProC.OpenNormalSubgroups.Basic
3import ProCGroups.ProC.OpenNormalSubgroups.BasisAtOne
4import ProCGroups.Profinite.Basic
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/ProCGroups/ProC/OpenNormalSubgroups/ProCGroup.lean
10translation_root: data/translation
11purpose: identifies the local data snapshot used to build pages/
12placement: after imports, never before imports
13-/
14/-!
15# Concrete pro-C groups via open normal quotient bases
17For a finite quotient class `C`, `IsProCGroup C G` is the main public predicate. The basis
18predicates in this file, including `HasOpenNormalBasisInClass C G` and
19`HasExactOpenNormalQuotientBasisInClass C G`, are auxiliary recognition principles and
20construction tools. Closure assumptions such as `FiniteGroupClass.Formation C` belong on the
21finite class `C`; abstract `ProCGroupPredicate` wrappers are reserved for bundled theorem
22families that need to carry those assumptions through a generic predicate parameter.
23-/
25namespace ProCGroups.ProC
27universe u v
29section
31variable {C : FiniteGroupClass.{u}}
32variable {G : Type u} [Group G] [TopologicalSpace G]
34/-- A neighborhood-basis formulation using open normal subgroups whose quotients lie in `C`.
36We isolate it as a separate predicate because it is the main usable local output for later
37formalization steps. -/
38def HasOpenNormalBasisInClass (C : FiniteGroupClass.{u})
39 (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
40 ∀ W : Set G, IsOpen W → (1 : G) ∈ W →
41 ∃ U : OpenNormalSubgroup G,
42 ((U : Subgroup G) : Set G) ⊆ W ∧ C (G ⧸ (U : Subgroup G))
46/-- Enlarge the finite-group class in an open-normal basis. -/
47theorem mono {C D : FiniteGroupClass.{u}} {G : Type u} [Group G] [TopologicalSpace G]
49 (hmono : ∀ {Q : Type u} [Group Q], C Q → D Q) :
51 intro W hW h1W
52 rcases hbasis W hW h1W with ⟨U, hUW, hCU⟩
53 exact ⟨U, hUW, hmono hCU⟩
57/-- Open normal subgroups whose quotient lies in the chosen class `C`.
59This packages the relevant family as an actual type so later inverse-limit and basis constructions
60can quantify over it directly. -/
61abbrev OpenNormalSubgroupInClass (C : FiniteGroupClass.{u})
62 (G : Type u) [Group G] [TopologicalSpace G] :=
63 {U : OpenNormalSubgroup G // C (G ⧸ (U : Subgroup G))}
67variable {C : FiniteGroupClass.{u}}
68variable {G : Type u} [Group G] [TopologicalSpace G]
70/-- Repackage an open normal subgroup together with a proof that its quotient lies in `C`. -/
71def ofOpenNormal (U : OpenNormalSubgroup G) (hU : C (G ⧸ (U : Subgroup G))) :
73 ⟨U, hU⟩
75/-- The defining quotient-membership proof carried by an open-normal-in-class subgroup. -/
76theorem quotient_mem (U : OpenNormalSubgroupInClass C G) :
77 C (G ⧸ (U.1 : Subgroup G)) :=
78 U.2
80/-- Move an open-normal-in-class subgroup along an inclusion of finite-group classes. -/
81def of_mono {D : FiniteGroupClass.{u}}
82 (hmono : ∀ {Q : Type u} [Group Q], C Q → D Q)
85 ⟨U.1, hmono U.2⟩
87/-- The top subgroup belongs to any finite-group class containing trivial quotients. -/
88def top [FiniteGroupClass.ContainsTrivialQuotients C] :
90 ⟨⊤, by
91 have hsub : Subsingleton (G ⧸ (⊤ : Subgroup G)) := by
92 constructor
93 intro x y
94 rcases QuotientGroup.mk'_surjective (⊤ : Subgroup G) x with ⟨a, rfl⟩
95 rcases QuotientGroup.mk'_surjective (⊤ : Subgroup G) y with ⟨b, rfl⟩
96 exact QuotientGroup.eq.2 (by simp only [Subgroup.mem_top])
97 exact FiniteGroupClass.ContainsTrivialQuotients.of_subsingleton hsub⟩
99/-- There is an open-normal-in-class subgroup whenever the class contains trivial quotients. -/
100theorem nonempty_of_containsTrivialQuotients [FiniteGroupClass.ContainsTrivialQuotients C] :
101 Nonempty (OpenNormalSubgroupInClass C G) :=
102 ⟨top (C := C) (G := G)⟩
104/-- Every open normal quotient of a compact group lies in the all-finite class. -/
105def of_allFinite [ContinuousMul G] [CompactSpace G] (U : OpenNormalSubgroup G) :
106 OpenNormalSubgroupInClass FiniteGroupClass.allFinite G :=
109/-- Pull back an open-normal-in-class subgroup along a continuous homomorphism, when the class is
110hereditary. -/
111noncomputable def comap {H : Type u} [Group H] [TopologicalSpace H]
112 (hHer : FiniteGroupClass.Hereditary C) (f : G →ₜ* H)
114 let N : OpenNormalSubgroup G :=
115 OpenNormalSubgroup.comap f.toMonoidHom f.continuous_toFun U.1
116 ⟨N, by
117 let qmap : G ⧸ (N : Subgroup G) →* H ⧸ (U.1 : Subgroup H) :=
118 QuotientGroup.map (N := (N : Subgroup G)) (M := (U.1 : Subgroup H))
119 f.toMonoidHom (by
120 intro x hx
121 exact hx)
122 have hqmap_inj : Function.Injective qmap := by
123 rw [← MonoidHom.ker_eq_bot_iff qmap]
124 ext z
125 constructor
126 · intro hz
127 rcases QuotientGroup.mk'_surjective (N : Subgroup G) z with ⟨x, rfl⟩
128 have hxU : f x ∈ (U.1 : Subgroup H) := by
129 apply (QuotientGroup.eq_one_iff (N := (U.1 : Subgroup H)) (f x)).1
130 simpa [qmap, MonoidHom.mem_ker] using hz
131 exact (QuotientGroup.eq_one_iff (N := (N : Subgroup G)) x).2 hxU
132 · intro hz
133 subst z
134 simp only [one_mem]
135 exact hHer.of_injective U.2 qmap hqmap_inj⟩
137/-- Push forward an open-normal-in-class subgroup along an open surjective continuous
138homomorphism, with the target quotient membership supplied explicitly. This is the lightweight
139bridge; stronger automatic versions can be derived from class closure hypotheses as needed. -/
140def mapOpenNormal {H : Type u} [Group H] [TopologicalSpace H]
141 (f : G →ₜ* H) (hfopen : IsOpenMap f) (hfsurj : Function.Surjective f)
143 (hC : C (H ⧸ ((OpenNormalSubgroup.map f hfopen hfsurj U.1 : OpenNormalSubgroup H) :
144 Subgroup H))) :
146 ⟨OpenNormalSubgroup.map f hfopen hfsurj U.1, hC⟩
148/-- Push forward an in-class open normal subgroup along an open surjective continuous
149homomorphism. Formation closure supplies the target quotient membership. -/
150def mapOpenNormal_of_formation {H : Type u} [Group H] [TopologicalSpace H]
151 (hForm : FiniteGroupClass.Formation C)
152 (f : G →ₜ* H) (hfopen : IsOpenMap f) (hfsurj : Function.Surjective f)
155 mapOpenNormal (C := C) (G := G) f hfopen hfsurj U (by
156 let M : OpenNormalSubgroup H := OpenNormalSubgroup.map f hfopen hfsurj U.1
157 let qmap : G ⧸ (U.1 : Subgroup G) →* H ⧸ (M : Subgroup H) :=
158 QuotientGroup.map (N := (U.1 : Subgroup G)) (M := (M : Subgroup H))
159 f.toMonoidHom (by
160 intro x hx
161 exact ⟨x, hx, rfl⟩)
162 have hqmap_surj : Function.Surjective qmap :=
163 QuotientGroup.map_surjective_of_surjective
164 (N := (U.1 : Subgroup G)) (M : Subgroup H) f.toMonoidHom (by
165 intro y
166 rcases QuotientGroup.mk'_surjective (M : Subgroup H) y with ⟨h, rfl⟩
167 rcases hfsurj h with ⟨g, rfl⟩
168 exact ⟨g, rfl⟩) (by
169 intro x hx
170 exact ⟨x, hx, rfl⟩)
171 have hquot :
172 C ((G ⧸ (U.1 : Subgroup G)) ⧸ qmap.ker) :=
173 hForm.quotientClosed qmap.ker U.2
174 let e :
175 (G ⧸ (U.1 : Subgroup G)) ⧸ qmap.ker ≃*
176 H ⧸ (M : Subgroup H) :=
177 QuotientGroup.quotientKerEquivOfSurjective qmap hqmap_surj
178 exact hForm.isomClosed ⟨e⟩ hquot)
180/-- Finite intersections stay in class for a formation. -/
181def inf (hForm : FiniteGroupClass.Formation C)
183 ⟨U.1 ⊓ V.1,
184 FiniteGroupClass.Formation.quotient_inf_mem
185 (C := C) (G := G) hForm U.1 V.1 U.2 V.2⟩
187/-- The quotient projection attached to an open-normal-in-class subgroup. -/
188def quotientProj (U : OpenNormalSubgroupInClass C G) :
189 G →ₜ* G ⧸ (U.1 : Subgroup G) :=
190 OpenNormalSubgroup.quotientProj U.1
192/-- The quotient projection evaluates to the quotient class of the element. -/
193@[simp]
194theorem quotientProj_apply (U : OpenNormalSubgroupInClass C G) (x : G) :
195 quotientProj (C := C) U x = QuotientGroup.mk' (U.1 : Subgroup G) x :=
196 rfl
198/-- The quotient projection attached to an open-normal-in-class subgroup is surjective. -/
199@[simp]
200theorem quotientProj_surjective (U : OpenNormalSubgroupInClass C G) :
201 Function.Surjective (quotientProj (C := C) U) :=
202 OpenNormalSubgroup.quotientProj_surjective U.1
204/-- The kernel predicate of the quotient projection is membership in the subgroup. -/
205@[simp]
206theorem quotientProj_eq_one_iff {U : OpenNormalSubgroupInClass C G} {x : G} :
207 quotientProj (C := C) U x = 1 ↔ x ∈ (U.1 : Subgroup G) :=
208 OpenNormalSubgroup.quotientProj_eq_one_iff (U := U.1)
210/-- Equality in the quotient attached to an open-normal-in-class subgroup. -/
211theorem quotientProj_eq_quotientProj_iff {U : OpenNormalSubgroupInClass C G} {x y : G} :
212 quotientProj (C := C) U x = quotientProj (C := C) U y ↔
213 x / y ∈ (U.1 : Subgroup G) :=
214 OpenNormalSubgroup.quotientProj_eq_quotientProj_iff (U := U.1)
216/-- Kernel membership for the quotient projection attached to an open-normal-in-class subgroup. -/
217@[simp]
218theorem mem_ker_quotientProj [ContinuousMul G] {U : OpenNormalSubgroupInClass C G} {x : G} :
219 x ∈ OpenNormalSubgroup.ker (quotientProj (C := C) U) ↔
220 x ∈ (U.1 : Subgroup G) :=
221 OpenNormalSubgroup.mem_ker_quotientProj (U := U.1)
223/-- The open-normal kernel of the quotient projection is the original subgroup. -/
224@[simp]
225theorem ker_quotientProj [ContinuousMul G] (U : OpenNormalSubgroupInClass C G) :
226 ((OpenNormalSubgroup.ker (quotientProj (C := C) U) : OpenNormalSubgroup G) :
227 Subgroup G) = (U.1 : Subgroup G) :=
228 OpenNormalSubgroup.ker_quotientProj U.1
230/-- The canonical transition map between quotients attached to nested open normal subgroups in the
231class-indexing family. -/
232def map {U V : OpenNormalSubgroupInClass C G}
233 (hUV : (V.1 : Subgroup G) ≤ (U.1 : Subgroup G)) :
234 G ⧸ (V.1 : Subgroup G) →* G ⧸ (U.1 : Subgroup G) :=
235 QuotientGroup.map _ _ (MonoidHom.id G) hUV
237/-- These transition maps are the natural quotient epimorphisms. -/
238theorem map_surjective {U V : OpenNormalSubgroupInClass C G}
239 (hUV : (V.1 : Subgroup G) ≤ (U.1 : Subgroup G)) :
240 Function.Surjective (map (C := C) (G := G) hUV) := by
241 intro x
242 rcases QuotientGroup.mk'_surjective (U.1 : Subgroup G) x with ⟨g, rfl⟩
243 exact ⟨QuotientGroup.mk' (V.1 : Subgroup G) g, rfl⟩
245/-- The identity transition map is the identity monoid homomorphism. -/
246theorem map_id (U : OpenNormalSubgroupInClass C G) :
247 map (C := C) (G := G) (le_rfl : (U.1 : Subgroup G) ≤ (U.1 : Subgroup G)) = MonoidHom.id _ := by
248 simp only [map, QuotientGroup.map_id]
250/-- The transition maps compose as expected. -/
251theorem map_comp {U V W : OpenNormalSubgroupInClass C G}
252 (hUV : (V.1 : Subgroup G) ≤ (U.1 : Subgroup G))
253 (hVW : (W.1 : Subgroup G) ≤ (V.1 : Subgroup G)) :
254 (map (C := C) (G := G) hUV).comp (map (C := C) (G := G) hVW) =
255 map (C := C) (G := G) (hVW.trans hUV) := by
256 simpa [map] using QuotientGroup.map_comp_map
257 (N := (W.1 : Subgroup G)) (M := (V.1 : Subgroup G)) (O := (U.1 : Subgroup G))
258 (f := MonoidHom.id G) (g := MonoidHom.id G) hVW hUV
260/-- The continuous transition map between quotients attached to nested open-normal-in-class
261subgroups. -/
262def transition [ContinuousMul G] {U V : OpenNormalSubgroupInClass C G}
263 (hUV : (U.1 : Subgroup G) ≤ (V.1 : Subgroup G)) :
264 G ⧸ (U.1 : Subgroup G) →ₜ* G ⧸ (V.1 : Subgroup G) :=
265 OpenNormalSubgroup.transition (G := G) (U := U.1) (V := V.1) hUV
267/-- Transition maps send quotient classes to the corresponding quotient classes. -/
268@[simp]
269theorem transition_mk [ContinuousMul G] {U V : OpenNormalSubgroupInClass C G}
270 (hUV : (U.1 : Subgroup G) ≤ (V.1 : Subgroup G)) (x : G) :
271 transition (C := C) (G := G) hUV (QuotientGroup.mk' (U.1 : Subgroup G) x) =
272 QuotientGroup.mk' (V.1 : Subgroup G) x :=
273 OpenNormalSubgroup.transition_mk (G := G) (U := U.1) (V := V.1) hUV x
275/-- The transition map composed with the smaller quotient projection is the larger quotient
276projection. -/
277@[simp]
278theorem transition_comp_quotientProj [ContinuousMul G] {U V : OpenNormalSubgroupInClass C G}
279 (hUV : (U.1 : Subgroup G) ≤ (V.1 : Subgroup G)) :
280 (transition (C := C) (G := G) hUV).comp (quotientProj (C := C) U) =
281 quotientProj (C := C) V :=
282 OpenNormalSubgroup.transition_comp_quotientProj (G := G) (U := U.1) (V := V.1) hUV
284/-- Transition maps between quotients by nested open-normal-in-class subgroups are surjective. -/
285theorem transition_surjective [ContinuousMul G] {U V : OpenNormalSubgroupInClass C G}
286 (hUV : (U.1 : Subgroup G) ≤ (V.1 : Subgroup G)) :
287 Function.Surjective (transition (C := C) (G := G) hUV) :=
288 OpenNormalSubgroup.transition_surjective (G := G) (U := U.1) (V := V.1) hUV
292section
294variable {C : FiniteGroupClass.{u}}
295variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
297/-- The inverse system of quotient groups indexed by open normal subgroups whose quotients lie in
298`C`, ordered by reverse inclusion. -/
299def openNormalSubgroupInClassSystem (C : FiniteGroupClass.{u})
300 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
301 InverseSystems.InverseSystem (I := OrderDual (OpenNormalSubgroupInClass C G)) where
302 X := fun U => G ⧸ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)
303 topologicalSpace := fun _ => inferInstance
304 map := fun {U V} hUV =>
305 OpenNormalSubgroupInClass.map (C := C) (G := G)
306 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV
307 continuous_map := by
308 intro U V hUV
309 letI : DiscreteTopology
310 (G ⧸ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)) :=
311 QuotientGroup.discreteTopology
312 (openNormalSubgroup_isOpen (G := G) ((OrderDual.ofDual U).1 : OpenNormalSubgroup G))
313 exact continuous_of_discreteTopology
314 map_id := by
315 intro U
316 funext x
317 exact congrFun
318 (congrArg DFunLike.coe
319 (OpenNormalSubgroupInClass.map_id
320 (C := C) (G := G) (U := OrderDual.ofDual U))) x
321 map_comp := by
322 intro U V W hUV hVW
323 funext x
324 rcases QuotientGroup.mk'_surjective
325 ((((OrderDual.ofDual W).1 : OpenNormalSubgroup G) : Subgroup G)) x with ⟨g, rfl⟩
326 rfl
328/-- Every coordinate of `openNormalSubgroupInClassSystem` is a quotient group. -/
330 (U : OrderDual (OpenNormalSubgroupInClass C G)) :
331 Group ((openNormalSubgroupInClassSystem C G).X U) := by
333 infer_instance
335/-- The canonical quotient homomorphisms from `G` into the inverse system from
338 (U : OrderDual (OpenNormalSubgroupInClass C G)) :
339 G →* G ⧸ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G) :=
340 QuotientGroup.mk' (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)
342/-- The canonical quotient homomorphisms are compatible with the transition maps. -/
345 (fun U : OrderDual (OpenNormalSubgroupInClass C G) =>
346 openNormalSubgroupInClassProj (C := C) (G := G) U) := by
347 intro U V hUV
348 funext g
349 rfl
351/-- The quotient system attached to the open normal subgroups in `C` is group-valued. -/
353 InverseSystems.IsGroupSystem (openNormalSubgroupInClassSystem C G) where
354 map_one := by
355 intro i j hij
356 change
357 OpenNormalSubgroupInClass.map
358 (C := C) (G := G)
359 (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij 1 = 1
360 exact
361 (OpenNormalSubgroupInClass.map
362 (C := C) (G := G)
363 (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij).map_one
364 map_mul := by
365 intro i j hij x y
366 change
367 OpenNormalSubgroupInClass.map
368 (C := C) (G := G)
369 (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij (x * y) =
370 OpenNormalSubgroupInClass.map
371 (C := C) (G := G)
372 (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij x *
373 OpenNormalSubgroupInClass.map
374 (C := C) (G := G)
375 (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij y
376 exact
377 (OpenNormalSubgroupInClass.map
378 (C := C) (G := G)
379 (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij).map_mul x y
380 map_inv := by
381 intro i j hij x
382 change
383 OpenNormalSubgroupInClass.map
384 (C := C) (G := G)
385 (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij x⁻¹ =
386 (OpenNormalSubgroupInClass.map
387 (C := C) (G := G)
388 (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij x)⁻¹
389 exact
390 (OpenNormalSubgroupInClass.map
391 (C := C) (G := G)
392 (U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij).map_inv x
394omit [IsTopologicalGroup G] in
395/-- Every open-normal-in-class quotient projection is surjective. -/
397 (U : OrderDual (OpenNormalSubgroupInClass C G)) :
398 Function.Surjective (openNormalSubgroupInClassProj (C := C) (G := G) U) :=
399 QuotientGroup.mk'_surjective _
401omit [IsTopologicalGroup G] in
402/-- The open-normal-in-class index family is directed under reverse inclusion. -/
404 (hForm : FiniteGroupClass.Formation C) :
405 Directed (α := OrderDual (OpenNormalSubgroupInClass C G)) (· ≤ ·) fun U => U := by
406 intro U V
408 ⟨U.1 ⊓ V.1,
409 FiniteGroupClass.Formation.quotient_inf_mem
410 (C := C) (G := G) hForm U.1 V.1 U.2 V.2⟩
411 refine ⟨OrderDual.toDual W, ?_, ?_⟩
412 · change ((W.1 : Subgroup G) ≤ (U.1 : Subgroup G))
413 exact inf_le_left
414 · change ((W.1 : Subgroup G) ≤ (V.1 : Subgroup G))
415 exact inf_le_right
417end
421variable {C : FiniteGroupClass.{u}}
422variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
424/-- Every quotient by an open normal subgroup belongs to the class `C`.
426This is stronger than the standard basis formulation unless `C` is quotient-closed. -/
427def HasAllOpenNormalQuotientsInClass (C : FiniteGroupClass.{u})
428 (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
429 ∀ U : OpenNormalSubgroup G, C (G ⧸ (U : Subgroup G))
431/-- Standard pro-`C` group: profinite, with a neighborhood basis of open normal subgroups whose
432quotients lie in `C`. -/
433structure IsProCGroup (C : FiniteGroupClass.{u})
434 (G : Type u) [Group G] [TopologicalSpace G] : Prop where
435 isProfinite : IsProfiniteGroup G
438/-- Strict pro-`C` group: profinite, and every open-normal quotient lies in `C`. -/
439structure IsStrictProCGroup (C : FiniteGroupClass.{u})
440 (G : Type u) [Group G] [TopologicalSpace G] : Prop where
441 isProfinite : IsProfiniteGroup G
442 all_open_normal_quotients : HasAllOpenNormalQuotientsInClass C G
446/-- A strict pro-`C` group is pro-`C` in the standard basis sense. -/
447theorem to_isProCGroup (hG : IsStrictProCGroup C G) : IsProCGroup C G := by
448 refine ⟨hG.isProfinite, ?_⟩
449 intro W hW h1W
450 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG.isProfinite
451 letI : T2Space G := IsProfiniteGroup.t2Space hG.isProfinite
452 letI : TotallyDisconnectedSpace G :=
453 IsProfiniteGroup.totallyDisconnectedSpace hG.isProfinite
454 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hW h1W with ⟨U, hUW⟩
455 exact ⟨U, hUW, hG.all_open_normal_quotients U⟩
459namespace IsProCGroup
461omit [IsTopologicalGroup G] in
462/-- The underlying profinite-group structure of a pro-`C` group. -/
463theorem isProfiniteGroup (hG : IsProCGroup C G) : IsProfiniteGroup G :=
464 hG.isProfinite
466omit [IsTopologicalGroup G] in
467/-- The topological group component of a pro-`C` group. -/
468theorem isTopologicalGroup (hG : IsProCGroup C G) : IsTopologicalGroup G :=
469 hG.isProfiniteGroup.isTopologicalGroup
471omit [IsTopologicalGroup G] in
472/-- Compactness of a pro-`C` group. -/
473theorem compactSpace (hG : IsProCGroup C G) : CompactSpace G :=
474 IsProfiniteGroup.compactSpace hG.isProfinite
476omit [IsTopologicalGroup G] in
477/-- Hausdorffness of a pro-`C` group. -/
478theorem t2Space (hG : IsProCGroup C G) : T2Space G :=
479 IsProfiniteGroup.t2Space hG.isProfinite
481omit [IsTopologicalGroup G] in
482/-- The `T1` property of a pro-`C` group. -/
483theorem t1Space (hG : IsProCGroup C G) : T1Space G :=
484 hG.isProfiniteGroup.t1Space
486omit [IsTopologicalGroup G] in
487/-- Total disconnectedness of a pro-`C` group. -/
488theorem totallyDisconnectedSpace (hG : IsProCGroup C G) : TotallyDisconnectedSpace G :=
489 IsProfiniteGroup.totallyDisconnectedSpace hG.isProfinite
491omit [IsTopologicalGroup G] in
492/-- Enlarge the finite-group class of a pro-`C` group. -/
493theorem mono {D : FiniteGroupClass.{u}}
494 (hG : IsProCGroup C G)
495 (hmono : ∀ {Q : Type u} [Group Q], C Q → D Q) :
496 IsProCGroup D G :=
497 ⟨hG.isProfiniteGroup, hG.basis.mono hmono⟩
499omit [IsTopologicalGroup G] in
500/-- In a pro-`C` group, every open neighborhood of `1` contains an open normal subgroup whose
501quotient still belongs to `C`. -/
502theorem hasOpenNormalBasisInClass (hG : IsProCGroup C G) :
504 hG.basis
506/-- With isomorphism and quotient closure, the basis definition implies the older all-open
507normal quotient condition. -/
509 (hIso : FiniteGroupClass.IsomClosed C)
510 (hQuot : FiniteGroupClass.QuotientClosed C)
511 (hG : IsProCGroup C G) :
513 intro U
514 rcases hG.basis (((U : Subgroup G) : Set G))
515 (openNormalSubgroup_isOpen (G := G) U) U.one_mem' with
516 ⟨V, hVU, hCV⟩
517 let q : G ⧸ (V : Subgroup G) →ₜ* G ⧸ (U : Subgroup G) :=
518 OpenNormalSubgroup.transition (G := G) hVU
519 have hqsurj : Function.Surjective q := OpenNormalSubgroup.transition_surjective (G := G) hVU
520 have hQuot :
521 C ((G ⧸ (V : Subgroup G)) ⧸ q.toMonoidHom.ker) :=
522 hQuot (N := q.toMonoidHom.ker) hCV
523 exact hIso ⟨QuotientGroup.quotientKerEquivOfSurjective q.toMonoidHom hqsurj⟩ hQuot
525/-- In a pro-`C` group over a formation, every open-normal quotient lies in `C`. -/
526theorem quotient_mem (hForm : FiniteGroupClass.Formation C)
527 (hG : IsProCGroup C G) (U : OpenNormalSubgroup G) :
528 C (G ⧸ (U : Subgroup G)) :=
530 hForm.isomClosed hForm.quotientClosed hG U
532/-- For formations, the strict and basis definitions agree. -/
534 (hForm : FiniteGroupClass.Formation C) :
535 IsStrictProCGroup C G ↔ IsProCGroup C G := by
536 constructor
537 · exact IsStrictProCGroup.to_isProCGroup
538 · intro hG
539 exact
540 { isProfinite := hG.isProfinite
541 all_open_normal_quotients :=
543 hForm.isomClosed hForm.quotientClosed hG }
545/-- Any quotient by an open normal subgroup of a pro-`C` group is finite. -/
546theorem finite_quotient (hG : IsProCGroup C G) (U : OpenNormalSubgroup G) :
547 Finite (G ⧸ (U : Subgroup G)) := by
548 letI : CompactSpace G := IsProCGroup.compactSpace hG
549 letI : T2Space G := IsProCGroup.t2Space hG
552omit [IsTopologicalGroup G] in
553/-- In a pro-`C` group, every open neighborhood of `1` contains an indexed open normal subgroup
554whose quotient lies in `C`. -/
555theorem exists_openNormalSubgroupInClass_sub_open_nhds_of_one (hG : IsProCGroup C G)
556 {W : Set G} (hW : IsOpen W) (h1W : (1 : G) ∈ W) :
557 ∃ U : OpenNormalSubgroupInClass C G, (((U.1 : Subgroup G) : Set G)) ⊆ W := by
558 rcases hG.hasOpenNormalBasisInClass W hW h1W with ⟨U, hUW, hCU⟩
559 exact ⟨⟨U, hCU⟩, hUW⟩
561section DiscreteCoset
563omit [IsTopologicalGroup G] in
564/-- A continuous map to a discrete target is locally fixed on a sufficiently small right coset,
565with the small subgroup chosen among the open normal pro-`C` quotients. -/
567 (hG : IsProCGroup C G)
568 {A : Type v} [TopologicalSpace A] [DiscreteTopology A]
569 (f : G → A) (hf : Continuous f) (g₀ : G) :
571 ∀ g : G, g * g₀⁻¹ ∈ (U.1 : Subgroup G) → f g = f g₀ := by
572 letI : IsTopologicalGroup G := hG.isTopologicalGroup
573 let W : Set G := {x | f (x * g₀) = f g₀}
574 have hW : IsOpen W := by
575 change IsOpen ((fun x : G => f (x * g₀)) ⁻¹' ({f g₀} : Set A))
576 exact isOpen_discrete _ |>.preimage (hf.comp (continuous_id.mul continuous_const))
577 have h1W : (1 : G) ∈ W := by
578 simp only [Set.mem_setOf_eq, one_mul, W]
579 rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hW h1W with ⟨U, hUW⟩
580 refine ⟨U, ?_⟩
581 intro g hg
582 have hmem : g * g₀⁻¹ ∈ W := hUW hg
583 have hrewrite : (g * g₀⁻¹) * g₀ = g := by
584 simp only [mul_assoc, inv_mul_cancel, mul_one]
585 simpa [W, hrewrite] using hmem
587end DiscreteCoset
589omit [IsTopologicalGroup G] in
590/-- In a pro-`C` group, the open normal subgroups whose quotients lie in `C` have trivial total
591intersection. -/
592theorem iInf_openNormalSubgroupInClass_eq_bot (hG : IsProCGroup C G) :
593 iInf (fun U : OpenNormalSubgroupInClass C G => (U.1 : Subgroup G)) = (⊥ : Subgroup G) := by
594 letI : T2Space G := IsProCGroup.t2Space hG
595 apply le_antisymm
596 · intro x hx
597 change x = 1
598 by_contra hxne
599 let W : Set G := ({x} : Set G)ᶜ
600 have hW : IsOpen W := by
601 simp only [isOpen_compl_iff, Set.finite_singleton, Set.Finite.isClosed, W]
602 have h1W : (1 : G) ∈ W := by
603 have hx1 : (1 : G) ≠ x := by
604 intro h1x
605 exact hxne h1x.symm
606 simpa [W] using hx1
607 rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hW h1W with ⟨U, hUW⟩
608 have hxall : ∀ U : OpenNormalSubgroupInClass C G, x ∈ (U.1 : Subgroup G) := by
609 simpa [Subgroup.mem_iInf] using hx
610 have hxU : x ∈ (U.1 : Subgroup G) := hxall U
611 have hxW : x ∈ W := hUW hxU
612 exact hxW (by simp only [Set.mem_singleton_iff])
613 · exact bot_le
615omit [IsTopologicalGroup G] in
616/-- Set-theoretic form of the trivial-intersection statement. -/
617theorem iInter_openNormalSubgroupInClass_eq_singleton (hG : IsProCGroup C G) :
618 (⋂ U : OpenNormalSubgroupInClass C G, (((U.1 : Subgroup G) : Set G))) = ({1} : Set G) := by
619 ext x
620 constructor
621 · intro hx
622 have hx' : x ∈ iInf (fun U : OpenNormalSubgroupInClass C G => (U.1 : Subgroup G)) := by
623 simpa [Subgroup.mem_iInf, Set.mem_iInter] using hx
624 have hxbot : x ∈ (⊥ : Subgroup G) := by
625 simpa [hG.iInf_openNormalSubgroupInClass_eq_bot] using hx'
626 simpa using hxbot
627 · rintro rfl
628 simp only [OpenSubgroup.coe_toSubgroup, Set.mem_iInter, SetLike.mem_coe, one_mem, implies_true]
630omit [IsTopologicalGroup G] in
631/-- Explicit family form of the open-normal basis and trivial-intersection package. -/
632theorem exists_openNormalBasisInClassFamily (hG : IsProCGroup C G) :
633 ∃ ι : Type u, ∃ U : ι → OpenNormalSubgroup G,
634 (∀ i, C (G ⧸ (U i : Subgroup G))) ∧
635 (∀ W : Set G, IsOpen W → (1 : G) ∈ W →
636 ∃ i, (((U i : Subgroup G) : Set G)) ⊆ W) ∧
637 iInf (fun i => (U i : Subgroup G)) = (⊥ : Subgroup G) := by
638 refine ⟨OpenNormalSubgroupInClass C G, fun i => i.1, ?_, ?_, ?_⟩
639 · intro i
640 exact i.2
641 · intro W hW h1W
642 rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hW h1W with ⟨U, hUW⟩
643 exact ⟨U, hUW⟩
644 · simpa using hG.iInf_openNormalSubgroupInClass_eq_bot
646omit [IsTopologicalGroup G] in
647/-- Membership in every open-normal-in-class subgroup forces an element to be trivial. -/
648theorem eq_one_of_mem_all_openNormalSubgroupInClass (hG : IsProCGroup C G) {x : G}
649 (hx : ∀ U : OpenNormalSubgroupInClass C G, x ∈ (U.1 : Subgroup G)) :
650 x = 1 := by
651 have hx' : x ∈ iInf (fun U : OpenNormalSubgroupInClass C G => (U.1 : Subgroup G)) := by
652 simpa [Subgroup.mem_iInf] using hx
653 have hxbot : x ∈ (⊥ : Subgroup G) := by
654 simpa [hG.iInf_openNormalSubgroupInClass_eq_bot] using hx'
655 simpa using hxbot
657omit [IsTopologicalGroup G] in
658/-- If `x ≠ 1`, then some open normal subgroup in the class-family omits `x`. -/
659theorem exists_openNormalSubgroupInClass_not_mem (hG : IsProCGroup C G) {x : G} (hx : x ≠ 1) :
660 ∃ U : OpenNormalSubgroupInClass C G, x ∉ (U.1 : Subgroup G) := by
661 by_contra h
662 apply hx
663 apply hG.eq_one_of_mem_all_openNormalSubgroupInClass
664 intro U
665 by_contra hxU
666 exact h ⟨U, hxU⟩
668omit [IsTopologicalGroup G] in
669/-- Two elements of a pro-`C` group are equal once they agree in every quotient by an open normal
670subgroup whose quotient lies in `C`. -/
671theorem eq_of_forall_openNormalSubgroupInClass_quotient_eq (hG : IsProCGroup C G) {x y : G}
672 (hxy : ∀ U : OpenNormalSubgroupInClass C G,
673 QuotientGroup.mk' (U.1 : Subgroup G) x = QuotientGroup.mk' (U.1 : Subgroup G) y) :
674 x = y := by
675 have hxy' : x⁻¹ * y = 1 := by
676 apply hG.eq_one_of_mem_all_openNormalSubgroupInClass
677 intro U
678 exact QuotientGroup.eq.1 (hxy U)
679 calc
680 x = x * 1 := by simp only [mul_one]
681 _ = x * (x⁻¹ * y) := by rw [hxy']
682 _ = y := by simp only [mul_inv_cancel_left]
684omit [IsTopologicalGroup G] in
685/-- Coordinatewise equality in the canonical inverse-system projections already forces equality in
686the ambient pro-`C` group. -/
687theorem eq_of_forall_openNormalSubgroupInClassProj_eq (hG : IsProCGroup C G) {x y : G}
688 (hxy : ∀ U : OrderDual (OpenNormalSubgroupInClass C G),
689 openNormalSubgroupInClassProj (C := C) (G := G) U x =
690 openNormalSubgroupInClassProj (C := C) (G := G) U y) :
691 x = y := by
692 apply hG.eq_of_forall_openNormalSubgroupInClass_quotient_eq
693 intro U
694 simpa [openNormalSubgroupInClassProj] using hxy (OrderDual.toDual U)
696/-- A direct constructor for `IsProCGroup` from the stronger open-normal quotient criterion. -/
699 IsProCGroup C G :=
700 (IsStrictProCGroup.mk hprof hquot).to_isProCGroup
702omit [IsTopologicalGroup G] in
703/-- In a pro-`C` group there is at least one open normal subgroup with quotient in `C`. -/
704theorem openNormalSubgroupInClass_nonempty (hG : IsProCGroup C G) :
705 Nonempty (OpenNormalSubgroupInClass C G) := by
706 rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one
707 (W := Set.univ) isOpen_univ (by simp only [Set.mem_univ]) with ⟨U, _⟩
708 exact ⟨U⟩
710end IsProCGroup
712/-- The chosen Lean definition of a pro-`C` group matches the open-normal basis condition. -/
713theorem isProCGroup_iff {C : FiniteGroupClass.{u}}
714 {G : Type u} [Group G] [TopologicalSpace G] :
715 IsProCGroup C G ↔
717 constructor
718 · intro hG
719 exact ⟨hG.isProfinite, hG.basis⟩
720 · rintro ⟨hprof, hbasis⟩
721 exact ⟨hprof, hbasis⟩
723/-- The strict pro-`C` definition matches the all-open-normal-quotient condition. -/
724theorem isStrictProCGroup_iff {C : FiniteGroupClass.{u}}
725 {G : Type u} [Group G] [TopologicalSpace G] :
728 constructor
729 · intro hG
730 exact ⟨hG.isProfinite, hG.all_open_normal_quotients⟩
731 · rintro ⟨hprof, hall⟩
732 exact ⟨hprof, hall⟩
734end
736end ProCGroups.ProC