Yamaguchi Lean 4 Library
ProCGroups/ProC/InverseLimits/Predicates.lean
ProCGroups/ProC/InverseLimits/Predicates/Source

ProCGroups/ProC/InverseLimits/Predicates.lean

1import ProCGroups.FiniteGroups.StandardClasses
2import ProCGroups.Generation.QuotientCriteria
3import ProCGroups.ProC.InverseLimits.FiniteQuotients
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/ProC/InverseLimits/Predicates.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 groups and open normal quotients
16Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.
17-/
19open Set
20open scoped Topology Pointwise
22namespace ProCGroups.ProC
24universe u v
26open InverseSystems
28section
30variable {G : Type u} [Group G] [TopologicalSpace G]
32/-- Pronilpotent profinite groups, characterized by nilpotent finite quotients. -/
34 (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
35 IsProfiniteGroup G ∧ ∀ U : OpenNormalSubgroup G, Group.IsNilpotent (G ⧸ (U : Subgroup G))
37/-- Prosolvable profinite groups, characterized by solvable finite quotients. -/
39 (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
40 IsProfiniteGroup G ∧ ∀ U : OpenNormalSubgroup G, IsSolvable (G ⧸ (U : Subgroup G))
44/-- The underlying profiniteness of a pronilpotent group. -/
45theorem isProfiniteGroup (hG : IsPronilpotentGroup G) : IsProfiniteGroup G :=
46 hG.1
52/-- The underlying profiniteness of a prosolvable group. -/
53theorem isProfiniteGroup (hG : IsProsolvableGroup G) : IsProfiniteGroup G :=
54 hG.1
56/-- Every quotient by an open normal subgroup of a prosolvable group is solvable. -/
57theorem quotient_isSolvable (hG : IsProsolvableGroup G) (U : OpenNormalSubgroup G) :
58 IsSolvable (G ⧸ (U : Subgroup G)) :=
59 hG.2 U
63/-- Procyclic groups as pro-`C` groups for the cyclic finite-group class. -/
65 (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
66 IsProCGroup FiniteGroupClass.cyclic G
68/-- Proabelian groups as pro-`C` groups for the abelian finite-group class. -/
70 (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
71 IsProCGroup FiniteGroupClass.abelian G
73/-- Pro-`p` groups as pro-`C` groups for the finite `p`-group class. -/
74def IsProPGroup (p : ℕ)
75 (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
76 IsProCGroup (FiniteGroupClass.pGroup p) G
78/-- Pro-`Σ` groups as pro-`C` groups for the finite `Σ`-group class. -/
79def IsProSigmaGroup (sigma : Set ℕ)
80 (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
81 IsProCGroup (FiniteGroupClass.sigmaGroup sigma) G
83/-- A pro-`nilpotent` group is pronilpotent. -/
85 (hG : IsProCGroup FiniteGroupClass.nilpotent G) : IsPronilpotentGroup G := by
86 letI : IsTopologicalGroup G := hG.isTopologicalGroup
87 refine ⟨hG.isProfinite, ?_⟩
88 intro U
89 exact
90 (IsProCGroup.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
91 FiniteGroupClass.nilpotent_isomClosed FiniteGroupClass.nilpotent_quotientClosed hG U).2
93/-- A pro-`solvable` group is prosolvable. -/
95 (hG : IsProCGroup FiniteGroupClass.solvable G) : IsProsolvableGroup G := by
96 letI : IsTopologicalGroup G := hG.isTopologicalGroup
97 refine ⟨hG.isProfinite, ?_⟩
98 intro U
99 exact
100 (IsProCGroup.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
101 FiniteGroupClass.solvable_isomClosed FiniteGroupClass.solvable_quotientClosed hG U).2
105/-- A procyclic group is pronilpotent. -/
106theorem isPronilpotentGroup (hG : IsProcyclicGroup G) : IsPronilpotentGroup G := by
107 letI : IsTopologicalGroup G := hG.isTopologicalGroup
108 refine ⟨hG.isProfinite, ?_⟩
109 intro U
110 exact
111 (FiniteGroupClass.cyclic_to_nilpotent
112 (IsProCGroup.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
113 FiniteGroupClass.cyclic_isomClosed FiniteGroupClass.cyclic_quotientClosed hG U)).2
115/-- A procyclic group is prosolvable. -/
116theorem isProsolvableGroup (hG : IsProcyclicGroup G) : IsProsolvableGroup G := by
117 letI : IsTopologicalGroup G := hG.isTopologicalGroup
118 refine ⟨hG.isProfinite, ?_⟩
119 intro U
120 exact
121 (FiniteGroupClass.cyclic_to_solvable
122 (IsProCGroup.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
123 FiniteGroupClass.cyclic_isomClosed FiniteGroupClass.cyclic_quotientClosed hG U)).2
125/-- A procyclic group is proabelian. -/
127 exact hG.mono (fun {Q} [Group Q] hQ => by
128 rcases hQ with ⟨hfin, hcyc⟩
129 refine ⟨hfin, ?_⟩
130 letI : IsCyclic Q := hcyc
131 letI : CommGroup Q := IsCyclic.commGroup
132 intro a b
133 exact mul_comm a b)
137/-- A profinite group topologically generated by one element is procyclic. -/
139 [IsTopologicalGroup G] (hG : IsProfiniteGroup G) {g : G}
140 (hg : Generation.TopologicallyGenerates (G := G) ({g} : Set G)) :
142 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
143 letI : T2Space G := IsProfiniteGroup.t2Space hG
144 refine IsProCGroup.of_allOpenNormalQuotients (C := FiniteGroupClass.cyclic) hG ?_
145 intro U
146 let qg : G ⧸ (U : Subgroup G) := QuotientGroup.mk' (U : Subgroup G) g
147 have hquot :
148 Generation.TopologicallyGenerates (G := G ⧸ (U : Subgroup G)) ({qg} : Set _) := by
149 have hmap := Generation.topologicallyGenerates_quotient_image
150 (G := G) (N := (U : Subgroup G)) (X := ({g} : Set G)) hg
151 simpa [qg] using hmap
152 have hdense :
153 Dense (((Subgroup.closure ({qg} : Set (G ⧸ (U : Subgroup G))) : Subgroup
154 (G ⧸ (U : Subgroup G))) : Set (G ⧸ (U : Subgroup G)))) :=
155 (Generation.topologicallyGenerates_iff_dense
156 (G := G ⧸ (U : Subgroup G)) (X := ({qg} : Set _))).1 hquot
157 have htop : Subgroup.zpowers qg = ⊤ := by
158 apply SetLike.ext'
159 rw [Subgroup.zpowers_eq_closure]
160 exact dense_discrete.1 hdense
161 have hcyc : IsCyclic (G ⧸ (U : Subgroup G)) :=
162 (isCyclic_iff_exists_zpowers_eq_top).2 ⟨qg, htop⟩
163 letI : Finite (G ⧸ (U : Subgroup G)) := openNormalSubgroup_finiteQuotient (G := G) U
164 exact ⟨inferInstance, hcyc⟩
168/-- Repackage a pronilpotent group as a pro-`nilpotent` group in the working `IsProCGroup`
169interface used for permanence arguments. -/
171 IsProCGroup FiniteGroupClass.nilpotent G := by
172 letI : IsTopologicalGroup G := IsProfiniteGroup.isTopologicalGroup hG.1
173 refine IsProCGroup.of_allOpenNormalQuotients (C := FiniteGroupClass.nilpotent) hG.1 ?_
174 intro U
175 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG.1
176 letI : T2Space G := IsProfiniteGroup.t2Space hG.1
177 exact ⟨openNormalSubgroup_finiteQuotient (G := G) U, hG.2 U⟩
183/-- Repackage a prosolvable group as a pro-`solvable` group in the working `IsProCGroup`
184interface used for permanence arguments. -/
186 IsProCGroup FiniteGroupClass.solvable G := by
187 letI : IsTopologicalGroup G := IsProfiniteGroup.isTopologicalGroup hG.1
188 refine IsProCGroup.of_allOpenNormalQuotients (C := FiniteGroupClass.solvable) hG.1 ?_
189 intro U
190 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG.1
191 letI : T2Space G := IsProfiniteGroup.t2Space hG.1
192 exact ⟨openNormalSubgroup_finiteQuotient (G := G) U, hG.2 U⟩
198/-- The quotient of a procyclic group by an open normal subgroup is procyclic. -/
199theorem quotient_openNormalSubgroup (hG : IsProcyclicGroup G)
200 (U : OpenNormalSubgroup G) :
201 IsProcyclicGroup (G ⧸ (U : Subgroup G)) := by
202 letI : IsTopologicalGroup G := IsProfiniteGroup.isTopologicalGroup hG.isProfinite
203 letI : Finite (G ⧸ (U : Subgroup G)) := hG.finite_quotient U
204 letI : DiscreteTopology (G ⧸ (U : Subgroup G)) :=
205 QuotientGroup.discreteTopology (openNormalSubgroup_isOpen (G := G) U)
206 exact IsProCGroup.of_finite_discrete (C := FiniteGroupClass.cyclic)
207 FiniteGroupClass.cyclic_quotientClosed
208 (IsProCGroup.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
209 FiniteGroupClass.cyclic_isomClosed FiniteGroupClass.cyclic_quotientClosed hG U)
213end
215end ProCGroups.ProC