ProCGroups/ProC/GroupPredicates/Standard.lean
1import ProCGroups.ProC.Category.Basic
2import ProCGroups.ProC.InverseLimits.Predicates
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/ProC/GroupPredicates/Standard.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Pro-C groups and open normal quotients
15Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.
16-/
18open Set
19open scoped Topology
21namespace ProCGroups.ProC
23universe u
25namespace ProCGroupPredicate
27/-- On finite discrete groups, the finite quotient class induced by
28`finiteGroupClassProCPredicate C` recovers `C`, provided `C` is quotient- and
29isomorphism-closed. -/
31 {C : FiniteGroupClass.{u}}
32 (hquot : FiniteGroupClass.QuotientClosed C)
33 (hiso : FiniteGroupClass.IsomClosed C)
34 {Q : Type u} [Group Q] [Finite Q] :
35 (ProCGroups.ProC.finiteGroupClassProCPredicate C).finiteQuotientClass Q ↔ C Q := by
36 constructor
37 · intro hQ
38 letI : TopologicalSpace Q := ⊥
39 letI : DiscreteTopology Q := ⟨rfl⟩
40 letI : IsTopologicalGroup Q := inferInstance
41 change Finite Q ∧ IsProCGroup C Q at hQ
42 let Ubot : OpenNormalSubgroup Q :=
43 { toOpenSubgroup := ⟨⊥, isOpen_discrete _⟩
44 isNormal' := inferInstance }
45 exact hiso ⟨QuotientGroup.quotientBot (G := Q)⟩
46 (IsProCGroup.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
47 hiso hquot hQ.2 Ubot)
48 · intro hQ
49 letI : TopologicalSpace Q := ⊥
50 letI : DiscreteTopology Q := ⟨rfl⟩
51 letI : IsTopologicalGroup Q := inferInstance
52 exact ⟨FiniteGroupClass.finite hQ,
53 IsProCGroup.of_finite_discrete (C := C) (G := Q) hquot hQ⟩
55/-- Formation data transfers from a finite-group class `C` to the finite quotient class induced
56by `finiteGroupClassProCPredicate C`. -/
58 (C : FiniteGroupClass.{u}) (hForm : FiniteGroupClass.Formation C) :
61 refine ⟨?_, ?_⟩
62 · intro G _ N _ hG
63 have hfiniteG : Finite G := by
64 exact FiniteGroupClass.finite hG
65 letI : Finite G := hfiniteG
66 have hCG : C G :=
68 hForm.quotientClosed hForm.isomClosed).1 hG
69 exact
71 hForm.quotientClosed hForm.isomClosed
72 (Q := G ⧸ N)).2 (hForm.quotientClosed N hCG)
73 · intro ι _ G _ H _ f hf hsurj hH
74 have hfiniteH : ∀ i, Finite (H i) := by
75 intro i
76 exact FiniteGroupClass.finite (hH i)
77 letI : ∀ i, Finite (H i) := hfiniteH
78 have hCH : ∀ i, C (H i) := fun i =>
80 hForm.quotientClosed hForm.isomClosed).1
81 (hH i)
82 have hCG : C G := hForm.finiteSubdirectProductClosed f hf hsurj hCH
83 letI : Finite G := Finite.of_injective f hf
84 exact
86 hForm.quotientClosed hForm.isomClosed).2 hCG
88/-- Full formation data transfers from a finite-group class `C` to the finite quotient class
89induced by `finiteGroupClassProCPredicate C`. -/
91 (C : FiniteGroupClass.{u}) (hFull : FiniteGroupClass.FullFormation C) :
93 fullFormation := by
94 let hForm : FiniteGroupClass.Formation C := hFull.melnikovFormation.formation
95 refine
96 { melnikovFormation :=
99 normalSubgroupClosed := ?_
100 extensionClosed := ?_ }
101 subgroupClosed := ?_ }
102 · intro G _ N _ hG
103 letI : Finite G := FiniteGroupClass.finite hG
104 have hCG : C G :=
106 hForm.quotientClosed hForm.isomClosed).1 hG
107 have hCN : C N := hFull.melnikovFormation.normalSubgroupClosed N hCG
108 letI : Finite N := FiniteGroupClass.finite hCN
109 exact
111 hForm.quotientClosed hForm.isomClosed).2 hCN
112 · intro E _ N _ hN hQ
113 letI : Finite N := FiniteGroupClass.finite hN
114 letI : Finite (E ⧸ N) := FiniteGroupClass.finite hQ
115 have hCN : C N :=
117 hForm.quotientClosed hForm.isomClosed).1 hN
118 have hCQ : C (E ⧸ N) :=
120 hForm.quotientClosed hForm.isomClosed).1 hQ
121 have hCE : C E := hFull.melnikovFormation.extensionClosed N hCN hCQ
122 letI : Finite E := FiniteGroupClass.finite hCE
123 exact
125 hForm.quotientClosed hForm.isomClosed).2 hCE
126 · intro G _ H hG
127 letI : Finite G := FiniteGroupClass.finite hG
128 have hCG : C G :=
130 hForm.quotientClosed hForm.isomClosed).1 hG
131 have hCH : C H := hFull.subgroupClosed H hCG
132 letI : Finite H := FiniteGroupClass.finite hCH
133 exact
135 hForm.quotientClosed hForm.isomClosed).2 hCH
137/-- A finite-class pro-`C` predicate is determined by its finite quotient class whenever `C` is
138a formation. -/
140 (C : FiniteGroupClass.{u}) (hForm : FiniteGroupClass.Formation C) :
142 holds_of_isProCGroup := by
143 intro G _ _ _ hG
144 refine ⟨hG.isProfinite, ?_⟩
145 intro W hW h1W
146 rcases hG.hasOpenNormalBasisInClass W hW h1W with ⟨U, hUW, hCU⟩
147 have hfinite : Finite (G ⧸ (U : Subgroup G)) := FiniteGroupClass.finite hCU
148 letI : Finite (G ⧸ (U : Subgroup G)) := hfinite
149 exact ⟨U, hUW,
151 hForm.quotientClosed hForm.isomClosed).1 hCU⟩
155/-- Procyclic profinite groups. -/
156def procyclicProC : ProCGroupPredicate.{u} :=
157 ProCGroups.ProC.finiteGroupClassProCPredicate FiniteGroupClass.cyclic
159/-- Proabelian profinite groups. -/
160def proabelianProC : ProCGroupPredicate.{u} :=
161 ProCGroups.ProC.finiteGroupClassProCPredicate FiniteGroupClass.abelian
163/-- Pronilpotent profinite groups. -/
164def pronilpotentProC : ProCGroupPredicate.{u} :=
165 ProCGroups.ProC.finiteGroupClassProCPredicate FiniteGroupClass.nilpotent
167/-- Prosolvable profinite groups. -/
168def prosolvableProC : ProCGroupPredicate.{u} :=
169 ProCGroups.ProC.finiteGroupClassProCPredicate FiniteGroupClass.solvable
171/-- Pro-`p` groups. -/
173 ProCGroups.ProC.finiteGroupClassProCPredicate (FiniteGroupClass.pGroup p)
175/-- Pro-`Σ` groups, for a set `Σ` of primes. -/
176def proSigmaProC (sigma : Set ℕ) : ProCGroupPredicate.{u} :=
177 ProCGroups.ProC.finiteGroupClassProCPredicate (FiniteGroupClass.sigmaGroup sigma)
179/-- On finite groups, the finite quotient class of `proSigmaProC` is exactly `sigmaGroup`. -/
181 {sigma : Set ℕ} {Q : Type u} [Group Q] [Finite Q] :
182 (proSigmaProC sigma).finiteQuotientClass Q ↔
183 FiniteGroupClass.sigmaGroup sigma Q := by
184 simpa [proSigmaProC] using
185 (ProCGroupPredicate.finiteQuotientClass_finiteGroupClassProCPredicate_iff
186 (FiniteGroupClass.sigmaGroup_quotientClosed sigma)
187 (FiniteGroupClass.sigmaGroup_isomClosed sigma)
188 (Q := Q))
190/-- Proabelian groups of exponent dividing `n` on every finite quotient. -/
191def abelianExponentProC (n : ℕ) : ProCGroupPredicate.{u} :=
192 ProCGroups.ProC.finiteGroupClassProCPredicate (FiniteGroupClass.abelianExponent n)
194/-- The proabelian predicate is stable under the finite-quotient formation operations. -/
195instance proabelianProC_hasFiniteQuotientFormation :
196 ProCGroupPredicate.HasFiniteQuotientFormation
197 (proabelianProC : ProCGroupPredicate.{u}) :=
198 ProCGroupPredicate.finiteQuotientFormation_finiteGroupClassProCPredicate
199 FiniteGroupClass.abelian FiniteGroupClass.abelian_formation
201/-- The proabelian predicate is determined by its finite quotients. -/
203 ProCGroupPredicate.DeterminedByFiniteQuotients
204 (proabelianProC : ProCGroupPredicate.{u}) :=
205 ProCGroupPredicate.determinedByFiniteQuotients_finiteGroupClassProCPredicate
206 FiniteGroupClass.abelian FiniteGroupClass.abelian_formation
208/-- The pro-p predicate is stable under the finite-quotient formation operations. -/
209instance proPProC_hasFiniteQuotientFormation (p : ℕ) :
210 ProCGroupPredicate.HasFiniteQuotientFormation
212 ProCGroupPredicate.finiteQuotientFormation_finiteGroupClassProCPredicate
213 (FiniteGroupClass.pGroup p) (FiniteGroupClass.pGroup_formation p)
215/-- The pro-p predicate is determined by its finite quotients. -/
216instance proPProC_determinedByFiniteQuotients (p : ℕ) :
217 ProCGroupPredicate.DeterminedByFiniteQuotients
219 ProCGroupPredicate.determinedByFiniteQuotients_finiteGroupClassProCPredicate
220 (FiniteGroupClass.pGroup p) (FiniteGroupClass.pGroup_formation p)
222/-- The pro-Sigma predicate is stable under the finite-quotient formation operations. -/
223instance proSigmaProC_hasFiniteQuotientFormation (sigma : Set ℕ) :
224 ProCGroupPredicate.HasFiniteQuotientFormation
225 (proSigmaProC sigma : ProCGroupPredicate.{u}) :=
226 ProCGroupPredicate.finiteQuotientFormation_finiteGroupClassProCPredicate
227 (FiniteGroupClass.sigmaGroup sigma) (FiniteGroupClass.sigmaGroup_formation sigma)
229/-- The pro-Sigma predicate has the full finite quotient formation structure. -/
230instance proSigmaProC_hasFiniteQuotientFullFormation (sigma : Set ℕ) :
231 ProCGroupPredicate.HasFiniteQuotientFullFormation
232 (proSigmaProC sigma : ProCGroupPredicate.{u}) :=
233 ProCGroupPredicate.finiteQuotientFullFormation_finiteGroupClassProCPredicate
234 (FiniteGroupClass.sigmaGroup sigma) (FiniteGroupClass.sigmaGroup_fullFormation sigma)
236/-- The pro-Sigma predicate is determined by its finite quotients. -/
237instance proSigmaProC_determinedByFiniteQuotients (sigma : Set ℕ) :
238 ProCGroupPredicate.DeterminedByFiniteQuotients
239 (proSigmaProC sigma : ProCGroupPredicate.{u}) :=
240 ProCGroupPredicate.determinedByFiniteQuotients_finiteGroupClassProCPredicate
241 (FiniteGroupClass.sigmaGroup sigma) (FiniteGroupClass.sigmaGroup_formation sigma)
243/-- The bounded-exponent abelian predicate is stable under finite-quotient formation operations. -/
244instance abelianExponentProC_hasFiniteQuotientFormation (n : ℕ) :
245 ProCGroupPredicate.HasFiniteQuotientFormation
246 (abelianExponentProC n : ProCGroupPredicate.{u}) :=
247 ProCGroupPredicate.finiteQuotientFormation_finiteGroupClassProCPredicate
248 (FiniteGroupClass.abelianExponent n) (FiniteGroupClass.abelianExponent_formation n)
250/-- The bounded-exponent abelian predicate is determined by its finite quotients. -/
251instance abelianExponentProC_determinedByFiniteQuotients (n : ℕ) :
252 ProCGroupPredicate.DeterminedByFiniteQuotients
253 (abelianExponentProC n : ProCGroupPredicate.{u}) :=
254 ProCGroupPredicate.determinedByFiniteQuotients_finiteGroupClassProCPredicate
255 (FiniteGroupClass.abelianExponent n) (FiniteGroupClass.abelianExponent_formation n)
257/-- The named procyclic predicate unfolds to `IsProcyclicGroup`. -/
258@[simp]
259theorem procyclicProC_holds_iff
260 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
261 procyclicProC (G := G) ↔ IsProcyclicGroup G :=
262 Iff.rfl
264/-- The named proabelian predicate unfolds to `IsProabelianGroup`. -/
265@[simp]
266theorem proabelianProC_holds_iff
267 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
268 proabelianProC (G := G) ↔ IsProabelianGroup G :=
269 Iff.rfl
271/-- The named pronilpotent predicate is equivalent to `IsPronilpotentGroup`. -/
272@[simp]
273theorem pronilpotentProC_holds_iff
274 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
275 pronilpotentProC (G := G) ↔ IsPronilpotentGroup G := by
276 constructor
278 · exact IsPronilpotentGroup.toIsProC_nilpotent
280/-- The named prosolvable predicate is equivalent to `IsProsolvableGroup`. -/
281@[simp]
282theorem prosolvableProC_holds_iff
283 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
284 prosolvableProC (G := G) ↔ IsProsolvableGroup G := by
285 constructor
287 · exact IsProsolvableGroup.toIsProC_solvable
289/-- The named pro-`p` predicate unfolds to `IsProPGroup`. -/
290@[simp]
291theorem proPProC_holds_iff
292 {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
293 proPProC p (G := G) ↔ IsProPGroup p G :=
294 Iff.rfl
296/-- The named pro-`Σ` predicate unfolds to `IsProSigmaGroup`. -/
297@[simp]
298theorem proSigmaProC_holds_iff
299 {sigma : Set ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
300 proSigmaProC sigma (G := G) ↔ IsProSigmaGroup sigma G :=
301 Iff.rfl
303/-- The named bounded-exponent abelian predicate unfolds to the corresponding concrete pro-`C`
304condition. -/
305@[simp]
306theorem abelianExponentProC_holds_iff
307 {n : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
308 abelianExponentProC n (G := G) ↔
309 IsProCGroup (FiniteGroupClass.abelianExponent n) G :=
310 Iff.rfl
312namespace IsProPGroup
314variable {p : ℕ} [Fact (Nat.Prime p)]
315variable {G : Type u} [Group G] [TopologicalSpace G]
317 /-- A pro-`p` group is pronilpotent. -/
318 theorem isPronilpotentGroup (hG : IsProPGroup p G) : IsPronilpotentGroup G := by
319 letI : IsTopologicalGroup G := hG.isTopologicalGroup
320 refine ⟨hG.isProfinite, ?_⟩
321 intro U
322 exact
323 (FiniteGroupClass.pGroup_to_nilpotent (p := p)
324 (hG.quotient_mem (FiniteGroupClass.pGroup_formation p) U)).2
326 /-- A pro-`p` group is prosolvable. -/
327 theorem isProsolvableGroup (hG : IsProPGroup p G) : IsProsolvableGroup G := by
328 letI : IsTopologicalGroup G := hG.isTopologicalGroup
329 refine ⟨hG.isProfinite, ?_⟩
330 intro U
331 exact
332 (FiniteGroupClass.pGroup_to_solvable (p := p)
333 (hG.quotient_mem (FiniteGroupClass.pGroup_formation p) U)).2
335end IsProPGroup
337section
339variable {G : Type u} [Group G] [TopologicalSpace G] [DiscreteTopology G]
341end
343end ProCGroups.ProC