Yamaguchi Lean 4 Library
ProCGroups/ProC/GroupPredicates/Basic.lean
ProCGroups/ProC/GroupPredicates/Basic/Source

ProCGroups/ProC/GroupPredicates/Basic.lean

1import ProCGroups.ProC.GroupPredicate
2import ProCGroups.ProC.OpenNormalSubgroups.ProCGroup
3import Mathlib.GroupTheory.Commutator.Basic
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/ProC/GroupPredicates/Basic.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Pro-C predicate bridge API
16The primary concrete predicate is `IsProCGroup C G`, where `C` is a `FiniteGroupClass`.
17The local basis predicate `HasExactOpenNormalQuotientBasisInClass C G` is a construction and
18recognition tool, connected to `IsProCGroup` by bridge theorems in the open-normal-subgroup
19files. `ProCGroupPredicate` and `ProCTheory` are auxiliary packaging layers for theorems that
20must range over abstract pro-`C` predicates while still exposing their finite quotient class and
21closure hypotheses.
22-/
24namespace ProCGroups.ProC
26universe u v
28open InverseSystems
30/-- The all-finite pro-`C` predicate is profiniteness. -/
31def allFiniteProC : ProCGroupPredicate.{u} where
32 holds := fun {G} [_] [_] [_] => IsProfiniteGroup G
34/-- The canonical topological pro-`C` predicate attached to a concrete finite-group class `C`.
36This declaration is `protected` to keep unqualified resolution stable when several pro-`C`
37namespaces are open at once. -/
39 (C : FiniteGroupClass.{u}) : ProCGroupPredicate where
40 holds := fun {G} [_] [_] [_] =>
41 IsProCGroup C G
43/-- The concrete finite-class pro-`C` predicate unfolds to `IsProCGroup`. -/
45 {C : FiniteGroupClass.{u}}
46 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
48 IsProCGroup C G :=
49 Iff.rfl
51/-- A group satisfying the concrete finite-class pro-`C` predicate is profinite. -/
53 (C : FiniteGroupClass.{u})
54 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
57 hG.isProfinite
59/-- Concrete class inclusion induces monotonicity of the corresponding `ProC` predicates. -/
61 {C C' : FiniteGroupClass.{u}}
62 (hmono :
63 ∀ {G : Type u} [Group G], C' G → C G)
64 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
67 intro hG
68 exact ⟨hG.isProfinite, hG.basis.mono hmono⟩
70/-- A bundled pro-`C` theory: a topological predicate, the finite quotient class that controls it,
71and the formation data for that finite class.
73This is the preferred package when a theorem needs to move between an abstract pro-`C` predicate
74and finite quotient closure hypotheses without carrying several unrelated arguments. -/
75structure ProCTheory where
76 predicate : ProCGroupPredicate.{u}
77 finiteQuotientClass : FiniteGroupClass.{u}
78 formation : FiniteGroupClass.Formation finiteQuotientClass
79 predicate_iff_isProCGroup :
80 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
81 predicate (G := G) ↔ IsProCGroup finiteQuotientClass G
83/-- One-directional version of `ProCTheory`, for predicates known to contain the concrete
84finite-quotient pro-`C` groups but not known to be equivalent to them. -/
85structure ProCTheorySound where
86 predicate : ProCGroupPredicate.{u}
87 finiteQuotientClass : FiniteGroupClass.{u}
88 formation : FiniteGroupClass.Formation finiteQuotientClass
89 sound :
90 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
91 IsProCGroup finiteQuotientClass G → predicate (G := G)
93namespace ProCTheory
95/-- View a theory as its topological pro-`C` predicate. -/
96abbrev holds (T : ProCTheory.{u})
97 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop :=
98 T.predicate (G := G)
100/-- The concrete pro-`C` group condition controlled by a theory. -/
101abbrev IsProCGroup (T : ProCTheory.{u})
102 (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
103 ProCGroups.ProC.IsProCGroup T.finiteQuotientClass G
105/-- A finite-group formation gives the corresponding concrete pro-`C` theory. -/
107 (C : FiniteGroupClass.{u}) [hC : FiniteGroupClass.IsFormation C] :
108 ProCTheory.{u} where
111 formation := hC.formation
112 predicate_iff_isProCGroup := by
113 intro G _ _ _
114 exact Iff.rfl
116/-- Build a theory from an abstract predicate once the controlling finite quotient class and
117equivalence theorem are explicit. -/
119 (ProC : ProCGroupPredicate.{u}) (C : FiniteGroupClass.{u})
120 (hForm : FiniteGroupClass.Formation C)
121 (hiff :
122 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
123 ProC (G := G) ↔ ProCGroups.ProC.IsProCGroup C G) :
124 ProCTheory.{u} where
125 predicate := ProC
127 formation := hForm
128 predicate_iff_isProCGroup := hiff
130/-- Build the one-directional package from an abstract predicate and a soundness theorem. -/
132 (ProC : ProCGroupPredicate.{u}) (C : FiniteGroupClass.{u})
133 (hForm : FiniteGroupClass.Formation C)
134 (hsound :
135 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
136 ProCGroups.ProC.IsProCGroup C G → ProC (G := G)) :
137 ProCTheorySound.{u} where
138 predicate := ProC
140 formation := hForm
141 sound := hsound
143/-- A theory predicate is equivalent to the concrete pro-`C` condition for its finite quotient
144class. -/
145theorem holds_iff_isProCGroup (T : ProCTheory.{u})
146 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
147 T.holds (G := G) ↔ T.IsProCGroup G :=
148 T.predicate_iff_isProCGroup
150/-- The predicate side of a theory implies the concrete pro-`C` condition. -/
151theorem isProCGroup_of_holds (T : ProCTheory.{u})
152 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
153 (hG : T.holds (G := G)) : T.IsProCGroup G :=
154 (T.holds_iff_isProCGroup).1 hG
156/-- The concrete pro-`C` condition implies the predicate side of a theory. -/
157theorem holds_of_isProCGroup (T : ProCTheory.{u})
158 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
159 (hG : T.IsProCGroup G) : T.holds (G := G) :=
160 (T.holds_iff_isProCGroup).2 hG
162/-- The finite quotient class packaged by a theory is a formation. -/
163def finiteQuotientFormation (T : ProCTheory.{u}) :
164 FiniteGroupClass.Formation T.finiteQuotientClass :=
165 T.formation
167/-- Formation data gives quotient closure for the finite quotient class of a theory. -/
168def quotientClosed (T : ProCTheory.{u}) :
169 FiniteGroupClass.QuotientClosed T.finiteQuotientClass :=
170 T.formation.quotientClosed
172/-- Formation data gives isomorphism closure for the finite quotient class of a theory. -/
173def isomClosed (T : ProCTheory.{u}) :
174 FiniteGroupClass.IsomClosed T.finiteQuotientClass :=
175 T.formation.isomClosed
181/-- The discrete finite-quotient class induced by a topological pro-`C` predicate. -/
182def finiteQuotientClass (ProC : ProCGroupPredicate.{u}) :
183 FiniteGroupClass.{u} where
184 pred := fun Q [Group Q] =>
185 Finite Q ∧
186 letI : TopologicalSpace Q := ⊥
187 letI : DiscreteTopology Q := ⟨rfl⟩
188 letI : IsTopologicalGroup Q := inferInstance
189 ProC (G := Q)
190 finite_of_mem := fun hQ => hQ.1
192/-- A topological pro-`C` predicate is determined by its finite quotient class. -/
194 (ProC : ProCGroupPredicate.{u}) : Prop where
196 ∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
197 IsProCGroup ProC.finiteQuotientClass G → ProC (G := G)
199/-- Formation data for the finite quotient class attached to a pro-`C` predicate. -/
201 (ProC : ProCGroupPredicate.{u}) : Prop where
202 formation : FiniteGroupClass.Formation (ProC.finiteQuotientClass)
204/-- Melnikov formation data for the finite quotient class attached to a pro-`C` predicate. -/
206 (ProC : ProCGroupPredicate.{u}) : Prop where
207 melnikovFormation : FiniteGroupClass.MelnikovFormation (ProC.finiteQuotientClass)
209/-- Full formation data for the finite quotient class attached to a pro-`C` predicate. -/
211 (ProC : ProCGroupPredicate.{u}) : Prop where
212 fullFormation : FiniteGroupClass.FullFormation (ProC.finiteQuotientClass)
214/-- Hereditary data for the finite quotient class attached to a pro-`C` predicate. -/
216 (ProC : ProCGroupPredicate.{u}) : Prop where
217 hereditary : FiniteGroupClass.Hereditary (ProC.finiteQuotientClass)
219/-- Finiteness of the finite quotient class attached to a pro-`C` predicate. -/
221 (ProC : ProCGroupPredicate.{u}) : Prop where
222 finite : ∀ {Q : Type u} [Group Q], ProC.finiteQuotientClass Q → Finite Q
224/-- Extension-closure data for the finite quotient class attached to a pro-`C` predicate. -/
226 (ProC : ProCGroupPredicate.{u}) : Prop where
227 extensionClosed : FiniteGroupClass.ExtensionClosed (ProC.finiteQuotientClass)
229/-- Permanence data for quotienting a `Source` pro-`C` group by the commutator subgroup of the
230kernel of a continuous homomorphism to a `Target` pro-`C` group.
232The mixed source/target form is useful for maximal-quotient arguments, where the source is often
233known to be pro-`C_e` while the quotient must be pro-`C`. -/
235 (Target Source : ProCGroupPredicate.{u}) : Prop where
237 ∀ {E F : Type u} [Group E] [TopologicalSpace E] [IsTopologicalGroup E]
238 [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
239 (φ : E →ₜ* F),
240 Source (G := E) → Target (G := F) →
241 Target (G := E ⧸ ⁅φ.toMonoidHom.ker, φ.toMonoidHom.ker⁆)
243/-- Accessor for commutator-kernel quotient permanence. -/
245 (Target Source : ProCGroupPredicate.{u})
246 [Target.ClosedUnderCommutatorKernelQuotientsFrom Source]
247 {E F : Type u} [Group E] [TopologicalSpace E] [IsTopologicalGroup E]
248 [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
249 (φ : E →ₜ* F)
250 (hE : Source (G := E)) (hF : Target (G := F)) :
251 Target (G := E ⧸ ⁅φ.toMonoidHom.ker, φ.toMonoidHom.ker⁆) :=
252 ClosedUnderCommutatorKernelQuotientsFrom.quotient_by_kernel_commutator φ hE hF
254/-- Accessor for finite quotient formation data. -/
255def finiteQuotientFormation
256 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation] :
257 FiniteGroupClass.Formation (ProC.finiteQuotientClass) :=
258 ProCGroupPredicate.HasFiniteQuotientFormation.formation
260/-- Accessor for finite quotient Melnikov formation data. -/
262 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientMelnikovFormation] :
263 FiniteGroupClass.MelnikovFormation (ProC.finiteQuotientClass) :=
264 ProCGroupPredicate.HasFiniteQuotientMelnikovFormation.melnikovFormation
266/-- Accessor for finite quotient full formation data. -/
268 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFullFormation] :
269 FiniteGroupClass.FullFormation (ProC.finiteQuotientClass) :=
270 ProCGroupPredicate.HasFiniteQuotientFullFormation.fullFormation
272/-- Accessor for hereditary finite quotient data. -/
274 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientHereditary] :
275 FiniteGroupClass.Hereditary (ProC.finiteQuotientClass) :=
276 ProCGroupPredicate.HasFiniteQuotientHereditary.hereditary
278/-- Accessor for finiteness of finite quotient class members. -/
280 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFinite] :
281 ∀ {Q : Type u} [Group Q], ProC.finiteQuotientClass Q → Finite Q :=
282 ProCGroupPredicate.HasFiniteQuotientFinite.finite
284/-- Accessor for finite quotient extension closure. -/
286 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientExtensionClosed] :
287 FiniteGroupClass.ExtensionClosed (ProC.finiteQuotientClass) :=
288 ProCGroupPredicate.HasFiniteQuotientExtensionClosed.extensionClosed
290/-- Formation data supplies isomorphism closure for the induced finite quotient class. -/
292 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation] :
293 FiniteGroupClass.IsomClosed (ProC.finiteQuotientClass) :=
294 ProC.finiteQuotientFormation.isomClosed
296/-- Formation data supplies quotient closure for the induced finite quotient class. -/
298 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation] :
299 FiniteGroupClass.QuotientClosed (ProC.finiteQuotientClass) :=
300 ProC.finiteQuotientFormation.quotientClosed
302/-- Formation data supplies finite-product closure for the induced finite quotient class. -/
304 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation] :
305 FiniteGroupClass.FiniteProductClosed (ProC.finiteQuotientClass) :=
306 ProC.finiteQuotientFormation.finiteProductClosed
308/-- Formation data supplies the trivial-quotient condition for the induced finite quotient class. -/
310 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation] :
311 FiniteGroupClass.ContainsTrivialQuotients (ProC.finiteQuotientClass) :=
312 ProC.finiteQuotientFormation.containsTrivialQuotients
314/-- Full formation data supplies quotient closure. -/
316 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFullFormation] :
317 FiniteGroupClass.QuotientClosed (ProC.finiteQuotientClass) :=
318 (ProC.finiteQuotientFullFormation).quotientClosed
320/-- Full formation data supplies isomorphism closure. -/
322 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFullFormation] :
323 FiniteGroupClass.IsomClosed (ProC.finiteQuotientClass) :=
324 (ProC.finiteQuotientFullFormation).isomClosed
326/-- Full formation data supplies finiteness of members. -/
328 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFullFormation] :
329 ∀ {Q : Type u} [Group Q], ProC.finiteQuotientClass Q → Finite Q :=
330 (ProC.finiteQuotientFullFormation).finiteOnly
332/-- Full formation data supplies extension closure. -/
334 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFullFormation] :
335 FiniteGroupClass.ExtensionClosed (ProC.finiteQuotientClass) :=
336 (ProC.finiteQuotientFullFormation).extensionClosed
338/-- Full formation data supplies hereditary subgroup closure. -/
340 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFullFormation] :
341 FiniteGroupClass.Hereditary (ProC.finiteQuotientClass) :=
342 (ProC.finiteQuotientFullFormation).hereditary
344/-- Full formation data supplies ordinary subgroup closure. -/
346 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFullFormation] :
347 FiniteGroupClass.SubgroupClosed (ProC.finiteQuotientClass) :=
348 (ProC.finiteQuotientFullFormation).subgroupClosed
350/-- A Melnikov formation supplies the underlying formation structure. -/
351@[instance 100]
353 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientMelnikovFormation] :
354 ProC.HasFiniteQuotientFormation where
355 formation := ProC.finiteQuotientMelnikovFormation.formation
357/-- Formation data supplies the trivial-quotient instance for the induced finite quotient class. -/
358@[instance 100]
360 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation] :
361 FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass :=
362 ProC.finiteQuotientFormation.containsTrivialQuotients
364/-- A Melnikov formation supplies finiteness of members of the induced finite quotient class. -/
365@[instance 100]
367 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientMelnikovFormation] :
368 ProC.HasFiniteQuotientFinite where
369 finite := (ProC.finiteQuotientMelnikovFormation).finiteOnly
371/-- A Melnikov formation supplies extension-closure of the induced finite quotient class. -/
372@[instance 100]
374 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientMelnikovFormation] :
375 ProC.HasFiniteQuotientExtensionClosed where
376 extensionClosed := (ProC.finiteQuotientMelnikovFormation).extensionClosed
378/-- A full formation supplies the underlying Melnikov formation. -/
379@[instance 100]
381 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFullFormation] :
382 ProC.HasFiniteQuotientMelnikovFormation where
383 melnikovFormation := ProC.finiteQuotientFullFormation.melnikovFormation
385/-- A full formation supplies hereditary closure of the induced finite quotient class. -/
386@[instance 100]
388 (ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFullFormation] :
389 ProC.HasFiniteQuotientHereditary where
390 hereditary := (ProC.finiteQuotientFullFormation).hereditary
396/-- Transport a `C`-quotient open-normal basis across a continuous multiplicative equivalence. -/
397theorem of_mulEquiv
398 {C : FiniteGroupClass.{u}} (hiso : FiniteGroupClass.IsomClosed C)
399 {G K : Type u}
400 [Group G] [TopologicalSpace G]
401 [Group K] [TopologicalSpace K]
402 (e : G ≃* K) (hcont : Continuous e) (hcontinuous_symm : Continuous e.symm)
405 intro W hW h1W
406 let V : Set K := e.symm ⁻¹' W
407 have hV : IsOpen V := hW.preimage hcontinuous_symm
408 have h1V : (1 : K) ∈ V := by
409 simpa [V] using h1W
410 rcases hbasis V hV h1V with ⟨U, hUV, hCU⟩
411 let Ucomap : OpenNormalSubgroup G :=
412 OpenNormalSubgroup.comap (e : G →* K) hcont U
413 refine ⟨Ucomap, ?_, ?_⟩
414 · intro g hg
415 have heg : e g ∈ ((U : OpenNormalSubgroup K) : Subgroup K) :=
416 (OpenNormalSubgroup.mem_comap
417 (f := (e : G →* K)) (hf := hcont) (U := U)).1 hg
418 have hVmem : e g ∈ V := hUV heg
419 simpa [V] using hVmem
420 · have hmap :
421 ((Ucomap : OpenNormalSubgroup G) : Subgroup G).map (e : G →* K) =
422 ((U : OpenNormalSubgroup K) : Subgroup K) := by
423 ext k
424 constructor
425 · rintro ⟨g, hg, rfl⟩
426 exact
427 (OpenNormalSubgroup.mem_comap
428 (f := (e : G →* K)) (hf := hcont) (U := U)).1 hg
429 · intro hk
430 refine ⟨e.symm k, ?_, by simp only [MonoidHom.coe_coe, MulEquiv.apply_symm_apply]⟩
431 exact
432 (OpenNormalSubgroup.mem_comap
433 (f := (e : G →* K)) (hf := hcont) (U := U)).2
434 (by simpa using hk)
435 exact hiso ⟨(QuotientGroup.congr
436 (Ucomap : Subgroup G) (U : Subgroup K) e hmap).symm⟩ hCU
440/-- In a profinite group, an element lying in every open normal subgroup is trivial. -/
442 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
443 (hG : IsProfiniteGroup G) {x : G}
444 (hx : ∀ U : OpenNormalSubgroup G, x ∈ (U : Subgroup G)) :
445 x = 1 := by
446 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
447 letI : T2Space G := IsProfiniteGroup.t2Space hG
448 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
449 by_contra hxne
450 let W : Set G := ({x} : Set G)ᶜ
451 have hW : IsOpen W := by
452 simp only [isOpen_compl_iff, Set.finite_singleton, Set.Finite.isClosed, W]
453 have h1W : (1 : G) ∈ W := by
454 have hx1 : (1 : G) ≠ x := by
455 intro h1x
456 exact hxne h1x.symm
457 simp only [Set.mem_compl_iff, Set.mem_singleton_iff, hx1, not_false_eq_true, W]
458 rcases ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
459 (G := G) hW h1W with
460 ⟨U, hUW⟩
461 have hxW : x ∈ W := hUW (hx U)
462 simp only [Set.mem_compl_iff, Set.mem_singleton_iff, not_true_eq_false, W] at hxW
464/-- Typeclass form of belonging to an ambient topological pro-`C` predicate. -/
465class ProCGroup (ProC : ProCGroupPredicate.{u})
466 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop where
467 isProC : ProC (G := G)
468 isProCGroup : IsProCGroup ProC.finiteQuotientClass G
470namespace ProCGroup
472/-- A pro-`C` group is profinite. -/
473theorem profiniteGroup (ProC : ProCGroupPredicate.{u})
474 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
475 [hG : ProCGroup ProC G] :
477 hG.isProCGroup.1
479/-- A pro-`C` group is a topological group. -/
480theorem isTopologicalGroup (ProC : ProCGroupPredicate.{u})
481 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
482 [hG : ProCGroup ProC G] :
483 IsTopologicalGroup G :=
484 hG.isProCGroup.isTopologicalGroup
486/-- A pro-`C` group is compact. -/
487theorem compactSpace (ProC : ProCGroupPredicate.{u})
488 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
489 [hG : ProCGroup ProC G] :
490 CompactSpace G :=
491 hG.isProCGroup.compactSpace
493/-- A pro-`C` group is Hausdorff. -/
494theorem t2Space (ProC : ProCGroupPredicate.{u})
495 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
496 [hG : ProCGroup ProC G] :
497 T2Space G :=
498 hG.isProCGroup.t2Space
500/-- A pro-`C` group is `T1`. -/
501theorem t1Space (ProC : ProCGroupPredicate.{u})
502 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
503 [hG : ProCGroup ProC G] :
504 T1Space G := by
505 letI : T2Space G := ProCGroup.t2Space ProC G
506 infer_instance
508/-- A pro-`C` group is totally disconnected. -/
509theorem totallyDisconnectedSpace (ProC : ProCGroupPredicate.{u})
510 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
511 [hG : ProCGroup ProC G] :
512 TotallyDisconnectedSpace G :=
513 hG.isProCGroup.totallyDisconnectedSpace
515/-- Open normal quotients of a pro-`C` group are finite. -/
516theorem finite_quotient (ProC : ProCGroupPredicate.{u})
517 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
518 [hG : ProCGroup ProC G] (U : OpenNormalSubgroup G) :
519 Finite (G ⧸ (U : Subgroup G)) :=
520 hG.isProCGroup.finite_quotient U
522/-- Open normal quotients of a pro-`C` group lie in the induced finite quotient class. -/
523theorem quotient_mem (ProC : ProCGroupPredicate.{u})
524 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
525 [hG : ProCGroup ProC G] [ProC.HasFiniteQuotientFormation] (U : OpenNormalSubgroup G) :
526 ProC.finiteQuotientClass (G ⧸ (U : Subgroup G)) :=
527 hG.isProCGroup.quotient_mem ProC.finiteQuotientFormation U
529/-- A pro-`C` group has an open-normal basis whose quotients lie in the induced finite quotient
530class. -/
531theorem hasOpenNormalBasisInClass (ProC : ProCGroupPredicate.{u})
532 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
533 [hG : ProCGroup ProC G] :
534 HasOpenNormalBasisInClass ProC.finiteQuotientClass G :=
535 hG.isProCGroup.hasOpenNormalBasisInClass
537/-- Every neighborhood of `1` in a pro-`C` group contains an open normal subgroup whose quotient lies
538in the induced finite quotient class. -/
539theorem exists_openNormalSubgroupInClass_sub_open_nhds_of_one
540 (ProC : ProCGroupPredicate.{u})
541 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
542 [hG : ProCGroup ProC G]
543 {W : Set G} (hW : IsOpen W) (h1W : (1 : G) ∈ W) :
544 ∃ U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
545 (((U.1 : Subgroup G) : Set G)) ⊆ W :=
546 hG.isProCGroup.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hW h1W
548/-- The open-normal-in-class family of a pro-`C` group is nonempty. -/
549theorem openNormalSubgroupInClass_nonempty (ProC : ProCGroupPredicate.{u})
550 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
551 [hG : ProCGroup ProC G] :
552 Nonempty (OpenNormalSubgroupInClass ProC.finiteQuotientClass G) :=
553 hG.isProCGroup.openNormalSubgroupInClass_nonempty
555/-- The open-normal-in-class subgroups of a pro-`C` group have trivial infimum. -/
556theorem iInf_openNormalSubgroupInClass_eq_bot (ProC : ProCGroupPredicate.{u})
557 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
558 [hG : ProCGroup ProC G] :
559 iInf (fun U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G =>
560 (U.1 : Subgroup G)) = (⊥ : Subgroup G) :=
561 hG.isProCGroup.iInf_openNormalSubgroupInClass_eq_bot
563/-- The open-normal-in-class subgroups of a pro-`C` group have singleton intersection. -/
564theorem iInter_openNormalSubgroupInClass_eq_singleton (ProC : ProCGroupPredicate.{u})
565 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
566 [hG : ProCGroup ProC G] :
567 (⋂ U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
568 (((U.1 : Subgroup G) : Set G))) = ({1} : Set G) :=
569 hG.isProCGroup.iInter_openNormalSubgroupInClass_eq_singleton
571/-- Membership in every open-normal-in-class subgroup of a pro-`C` group forces an element to be
572trivial. -/
573theorem eq_one_of_mem_all_openNormalSubgroupInClass (ProC : ProCGroupPredicate.{u})
574 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
575 [hG : ProCGroup ProC G] {x : G}
576 (hx : ∀ U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
577 x ∈ (U.1 : Subgroup G)) :
578 x = 1 :=
579 hG.isProCGroup.eq_one_of_mem_all_openNormalSubgroupInClass hx
581/-- A nontrivial element of a pro-`C` group is omitted by some open-normal-in-class subgroup. -/
582theorem exists_openNormalSubgroupInClass_not_mem (ProC : ProCGroupPredicate.{u})
583 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
584 [hG : ProCGroup ProC G] {x : G} (hx : x ≠ 1) :
585 ∃ U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
586 x ∉ (U.1 : Subgroup G) :=
587 hG.isProCGroup.exists_openNormalSubgroupInClass_not_mem hx
589/-- Two elements of a pro-`C` group are equal when they agree in every open-normal-in-class
590quotient. -/
591theorem eq_of_forall_openNormalSubgroupInClass_quotient_eq
592 (ProC : ProCGroupPredicate.{u})
593 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
594 [hG : ProCGroup ProC G] {x y : G}
595 (hxy : ∀ U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
596 QuotientGroup.mk' (U.1 : Subgroup G) x = QuotientGroup.mk' (U.1 : Subgroup G) y) :
597 x = y :=
598 hG.isProCGroup.eq_of_forall_openNormalSubgroupInClass_quotient_eq hxy
600/-- Coordinatewise equality in the canonical open-normal-in-class quotient system forces equality in
601the ambient pro-`C` group. -/
602theorem eq_of_forall_openNormalSubgroupInClassProj_eq
603 (ProC : ProCGroupPredicate.{u})
604 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
605 [hG : ProCGroup ProC G] {x y : G}
606 (hxy : ∀ U : OrderDual (OpenNormalSubgroupInClass ProC.finiteQuotientClass G),
607 openNormalSubgroupInClassProj (C := ProC.finiteQuotientClass) (G := G) U x =
608 openNormalSubgroupInClassProj (C := ProC.finiteQuotientClass) (G := G) U y) :
609 x = y :=
610 hG.isProCGroup.eq_of_forall_openNormalSubgroupInClassProj_eq hxy
612/-- Build the public `ProCGroup` class from the concrete quotient condition. -/
614 (ProC : ProCGroupPredicate.{u}) [ProC.DeterminedByFiniteQuotients]
615 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
616 (hG : IsProCGroup ProC.finiteQuotientClass G) :
617 ProCGroup ProC G where
619 ProCGroupPredicate.DeterminedByFiniteQuotients.holds_of_isProCGroup hG
622/-- Enlarge the finite quotient class of a bundled pro-`C` group. -/
624 {ProC ProD : ProCGroupPredicate.{u}} [ProD.DeterminedByFiniteQuotients]
625 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
626 [hG : ProCGroup ProC G]
627 (hmono :
628 ∀ {Q : Type u} [Group Q],
629 ProC.finiteQuotientClass Q → ProD.finiteQuotientClass Q) :
630 ProCGroup ProD G :=
631 ProCGroup.of_isProCGroup ProD G (hG.isProCGroup.mono hmono)
635/-- A finite discrete group lies in the finite quotient class induced by `allFiniteProC`. -/
637 {Q : Type u} [Group Q] [Finite Q] :
638 allFiniteProC.finiteQuotientClass Q := by
639 refine ⟨inferInstance, ?_⟩
640 letI : TopologicalSpace Q := ⊥
641 letI : DiscreteTopology Q := ⟨rfl⟩
642 letI : IsTopologicalGroup Q := inferInstance
644 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
646/-- The finite quotient class induced by `allFiniteProC` is exactly the all-finite class. -/
648 {Q : Type u} [Group Q] :
649 allFiniteProC.finiteQuotientClass Q ↔ Finite Q := by
650 constructor
651 · intro hQ
652 exact hQ.1
653 · intro hQ
654 letI : Finite Q := hQ
657/-- The all-finite pro-`C` predicate has a full finite quotient formation. -/
659 ProCGroupPredicate.HasFiniteQuotientFullFormation allFiniteProC where
660 fullFormation :=
661 { melnikovFormation :=
663 { quotientClosed := by
664 intro G _ N _ hG
665 exact allFiniteProC_finiteQuotientClass_iff_finite.2
666 (FiniteGroupClass.allFinite_quotientClosed N
667 (allFiniteProC_finiteQuotientClass_iff_finite.1 hG))
668 finiteSubdirectProductClosed := by
669 intro ι _ G _ H _ f hf _hsurj hH
670 exact allFiniteProC_finiteQuotientClass_iff_finite.2
671 (FiniteGroupClass.allFinite_finiteSubdirectProductClosed f hf _hsurj
672 (fun i => allFiniteProC_finiteQuotientClass_iff_finite.1 (hH i))) }
674 intro Q _ N _ hQ
675 exact allFiniteProC_finiteQuotientClass_iff_finite.2
677 (allFiniteProC_finiteQuotientClass_iff_finite.1 hQ))
679 intro E _ N _ hN hQ
680 exact allFiniteProC_finiteQuotientClass_iff_finite.2
681 (FiniteGroupClass.allFinite_extensionClosed N
682 (allFiniteProC_finiteQuotientClass_iff_finite.1 hN)
683 (allFiniteProC_finiteQuotientClass_iff_finite.1 hQ)) }
685 intro G _ H hG
686 exact allFiniteProC_finiteQuotientClass_iff_finite.2
687 (FiniteGroupClass.allFinite_subgroupClosed H
688 (allFiniteProC_finiteQuotientClass_iff_finite.1 hG)) }
690/-- The all-finite pro-`C` predicate is determined by finite quotients. -/
692 ProCGroupPredicate.DeterminedByFiniteQuotients allFiniteProC where
693 holds_of_isProCGroup hG := hG.isProfinite
695/-- A profinite group is pro-`C` for the all-finite predicate in the concrete quotient sense. -/
697 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
699 IsProCGroup allFiniteProC.finiteQuotientClass G := by
700 refine ⟨hG, ?_⟩
701 intro W hW h1W
702 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
703 letI : T2Space G := IsProfiniteGroup.t2Space hG
704 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
705 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hW h1W with ⟨U, hUW⟩
706 have hfinite : Finite (G ⧸ (U : Subgroup G)) := by
707 exact
708 Subgroup.quotient_finite_of_isOpen (U : Subgroup G)
710 letI : Finite (G ⧸ (U : Subgroup G)) := hfinite
711 exact ⟨U, hUW, allFiniteProC_finiteQuotientClass_of_finite (Q := G ⧸ (U : Subgroup G))⟩
713/-- A profinite group is a bundled pro-`C` group for the all-finite predicate. -/
715 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
720end ProCGroups.ProC