Source: ProCGroups.ProC.InverseLimits.Predicates
1import ProCGroups.FiniteGroups.StandardClasses
2import ProCGroups.Generation.QuotientCriteria
3import ProCGroups.ProC.InverseLimits.FiniteQuotients
5/-!
6# Finite-quotient predicates for profinite groups
8This file defines cyclic, abelian, and \(p\)-group open-normal quotient bases. It derives the
9cyclic basis associated with a single topological generator and the basic implications between
10these predicates.
11-/
13open Set
14open scoped Topology Pointwise
16namespace ProCGroups.ProC
18universe u v
20open InverseSystems
22section
24variable {G : Type u} [Group G] [TopologicalSpace G]
26/-- The identity-neighborhood basis property for open normal subgroups with cyclic quotients. -/
27def HasCyclicOpenNormalBasis
28 (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
29 HasOpenNormalBasisInClass FiniteGroupClass.cyclic G
31/-- The identity-neighborhood basis property for open normal subgroups with abelian quotients. -/
32def HasAbelianOpenNormalBasis
33 (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
34 HasOpenNormalBasisInClass FiniteGroupClass.abelian G
36/-- The identity-neighborhood basis property for open normal subgroups with finite
37\(p\)-group quotients. -/
38def HasPGroupOpenNormalBasis (p : ℕ) [Fact (Nat.Prime p)]
39 (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
40 HasOpenNormalBasisInClass (FiniteGroupClass.pGroup p) G
42namespace HasCyclicOpenNormalBasis
44/-- A cyclic open-normal quotient basis is also an abelian open-normal quotient basis. -/
45theorem hasAbelianOpenNormalBasis (hG : HasCyclicOpenNormalBasis G) : HasAbelianOpenNormalBasis
46 G := by
47 exact hG.mono (fun {Q} [Group Q] hQ => by
48 rcases hQ with ⟨hfin, hcyc⟩
49 refine ⟨hfin, ?_⟩
50 letI : IsCyclic Q := hcyc
51 letI : CommGroup Q := IsCyclic.commGroup
52 intro a b
53 exact mul_comm a b)
55end HasCyclicOpenNormalBasis
57/-- A profinite group topologically generated by one element has a cyclic open-normal quotient
58basis. -/
59theorem hasCyclicOpenNormalBasis_of_topologicallyGenerates_singleton
60 [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
61 [TotallyDisconnectedSpace G] {g : G}
62 (hg : Generation.TopologicallyGenerates (G := G) ({g} : Set G)) :
63 HasCyclicOpenNormalBasis G := by
64 refine HasOpenNormalBasisInClass.of_allOpenNormalQuotients (C := FiniteGroupClass.cyclic) ?_
65 intro U
66 let qg : G ⧸ (U : Subgroup G) := QuotientGroup.mk' (U : Subgroup G) g
67 have hquot :
68 Generation.TopologicallyGenerates (G := G ⧸ (U : Subgroup G)) ({qg} : Set _) := by
69 have hmap := Generation.topologicallyGenerates_quotient_image
70 (G := G) (N := (U : Subgroup G)) (X := ({g} : Set G)) hg
71 simpa [qg] using hmap
72 have hdense :
73 Dense (((Subgroup.closure ({qg} : Set (G ⧸ (U : Subgroup G))) : Subgroup
74 (G ⧸ (U : Subgroup G))) : Set (G ⧸ (U : Subgroup G)))) :=
75 (Generation.topologicallyGenerates_iff_dense
76 (G := G ⧸ (U : Subgroup G)) (X := ({qg} : Set _))).1 hquot
77 have htop : Subgroup.zpowers qg = ⊤ := by
78 apply SetLike.ext'
79 rw [Subgroup.zpowers_eq_closure]
80 exact dense_discrete.1 hdense
81 have hcyc : IsCyclic (G ⧸ (U : Subgroup G)) :=
82 (isCyclic_iff_exists_zpowers_eq_top).2 ⟨qg, htop⟩
83 letI : Finite (G ⧸ (U : Subgroup G)) := openNormalSubgroup_finiteQuotient (G := G) U
84 exact ⟨inferInstance, hcyc⟩
86end
88end ProCGroups.ProC