ReidemeisterSchreier/Profinite/OpenSubgroups/BasisFiniteRank.lean
1import ReidemeisterSchreier.Profinite.OpenSubgroups.BasisTheorems
2import ReidemeisterSchreier.Profinite.OpenSubgroups.RankBound
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ReidemeisterSchreier/Profinite/OpenSubgroups/BasisFiniteRank.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Profinite open-subgroup Schreier theory
15Profinite open subgroup quotients, finite permutation targets, dense free models, exact right Schreier generation, and topological rank bounds.
16-/
18open scoped Topology Pointwise
20namespace ReidemeisterSchreier
21namespace Profinite
23open ProCGroups
24open ProCGroups.FreeProC
25open ProCGroups.ProC
27universe u
29/-- Hypotheses used by the finite-rank Schreier basis theorem. The bundle keeps the theorem
31structure SchreierBasisFiniteRankHypotheses
32 (C : ProCGroups.FiniteGroupClass.{u}) : Prop where
34 isomClosed : ProCGroups.FiniteGroupClass.IsomClosed C
36 hasNontrivialCyclic :
37 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
38 C A ∧ IsCyclic A ∧ Nontrivial A
41/-- Finite converging-set basis data for an open subgroup of a free pro-`C` group on a finite
42converging set. The carrier is the open subgroup itself. -/
44 (C : ProCGroups.FiniteGroupClass.{u})
45 (hForm : ProCGroups.FiniteGroupClass.Formation C)
46 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
47 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
48 (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
49 (hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
50 {X : Type u} [Finite X]
51 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
52 {ι : X → F}
53 [DiscreteTopology (Set.range ι)]
55 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
56 (H : OpenSubgroup F) :
57 ∃ (B : Type u), Finite B ∧
58 ∃ μ : B → ↥(H : Subgroup F),
60 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
61 B ↥(H : Subgroup F) μ := by
62 classical
63 letI : CompactSpace F := IsProCGroup.compactSpace hF.isProC
64 letI : T2Space F := IsProCGroup.t2Space hF.isProC
65 letI : TopologicalSpace X := ⊥
66 letI : DiscreteTopology X := ⟨rfl⟩
67 letI : Fintype X := Fintype.ofFinite X
68 rcases
70 C hForm hSub hIso hQuot hExt hF H with
71 ⟨κ, _hκcont, _hκallBase, _hκbase, _hκcompact, _hκclosed, hκfree⟩
72 letI : Finite (OpenSubgroupRightQuotient H) :=
73 finite_openSubgroupRightQuotient (F := F) H
74 have hRangeFin : (Set.range ι).Finite := Set.finite_range ι
75 letI : Finite (Set.range ι) := hRangeFin.to_subtype
76 letI : Fintype (Set.range ι) := Fintype.ofFinite (Set.range ι)
77 letI : Finite (OnePoint X) := Finite.of_fintype (OnePoint X)
78 letI : Finite (Set.range κ) := (Set.finite_range κ).to_subtype
79 let x0 : Set.range κ :=
80 ⟨κ (openSubgroupRightCoset H (1 : F), OnePoint.infty),
81 ⟨(openSubgroupRightCoset H (1 : F), OnePoint.infty), rfl⟩⟩
82 letI : DiscreteTopology (Set.range κ) :=
83 DiscreteTopology.of_finite_of_isClosed_singleton fun _ => isClosed_singleton
84 let B : Type u := {y : Set.range κ // y ≠ x0}
85 let μ : B → ↥(H : Subgroup F) := fun y => y.1.1
86 have hμfree :
88 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) B ↥(H : Subgroup F) μ := by
89 simpa [B, μ, x0] using
91 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) hκfree
92 exact ⟨B, inferInstance, μ, hμfree⟩
94/-- Finite converging-set basis model for an open subgroup of a finite-rank free pro-`C` group on
95a converging set. -/
97 (C : ProCGroups.FiniteGroupClass.{u})
98 (hForm : ProCGroups.FiniteGroupClass.Formation C)
99 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
100 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
101 (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
102 (hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
103 {X : Type u} [Finite X]
104 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
105 {ι : X → F}
106 [DiscreteTopology (Set.range ι)]
108 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
109 (H : OpenSubgroup F) :
110 ∃ Fdata : FreeProCGroupOnConvergingSetData
111 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
112 Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧ Finite Fdata.basis := by
114 C hForm hSub hIso hQuot hExt hF H with
115 ⟨B, hBfin, μ, hμfree⟩
116 letI : Finite B := hBfin
117 let Fdata : FreeProCGroupOnConvergingSetData
118 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) :=
119 { basis := B
120 carrier := ↥(H : Subgroup F)
122 instTopologicalSpace := inferInstance
123 instIsTopologicalGroup := inferInstance
124 inclusion := μ
125 isFree := hμfree }
126 exact ⟨Fdata, ⟨ContinuousMulEquiv.refl _⟩, inferInstance⟩
128/-- An exact-size finite generating family for the open subgroup, indexed by the Schreier
129rank-transform cardinal. This is a generating family, not a basis: the padding step may repeat
130the distinguished padding element `1`. -/
132 (C : ProCGroups.FiniteGroupClass.{u})
133 (hForm : ProCGroups.FiniteGroupClass.Formation C)
134 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
135 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
136 (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
137 (hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
138 (hcyc :
139 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
140 C A ∧ IsCyclic A ∧ Nontrivial A)
141 {X : Type u} [Finite X]
142 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
143 {ι : X → F}
144 [DiscreteTopology (Set.range ι)]
146 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
147 (H : OpenSubgroup F) :
148 ∃ κ :
149 ULift (Fin (_root_.ReidemeisterSchreier.Schreier.rankTransform
150 (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))))) →
151 ↥(H : Subgroup F),
152 Generation.GeneratesAndConvergesToOne
153 (G := ↥(H : Subgroup F)) (Set.range κ) := by
154 classical
155 let n : ℕ := _root_.ReidemeisterSchreier.Schreier.rankTransform
156 (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F)))
158 C hForm hSub hIso hQuot hExt hF H with
159 ⟨B, hBfin, μ, hμfree⟩
160 letI : Finite B := hBfin
161 letI : Fintype B := Fintype.ofFinite B
162 let Fdata : FreeProCGroupOnConvergingSetData
163 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) :=
164 { basis := B
165 carrier := ↥(H : Subgroup F)
167 instTopologicalSpace := inferInstance
168 instIsTopologicalGroup := inferInstance
169 inclusion := μ
170 isFree := hμfree }
171 letI : Fintype X := Fintype.ofFinite X
172 let Fambient : FreeProCGroupOnConvergingSetData
173 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) :=
174 { basis := X
175 carrier := F
177 instTopologicalSpace := inferInstance
178 instIsTopologicalGroup := inferInstance
179 inclusion := ι
180 isFree := hF }
181 have hAmbientRank :
182 Cardinal.mk X = Generation.topologicalRank F :=
183 basisCard_eq_topologicalRank_of_finiteBasis C hQuot hcyc Fambient
184 have hdF : Generation.topologicalRank F = Nat.card X := by
185 calc
186 Generation.topologicalRank F = Cardinal.mk X := hAmbientRank.symm
187 _ = (Nat.card X : Cardinal) := by simp only [Cardinal.mk_fintype, Nat.card_eq_fintype_card]
188 have hdHle :
189 Generation.topologicalRank ↥(H : Subgroup F) ≤ (n : Cardinal) := by
190 simpa [n] using
192 (G := F) hF.isProC.1 hdF H
193 have hBasisRank :
194 Cardinal.mk B = Generation.topologicalRank ↥(H : Subgroup F) := by
195 simpa [Fdata] using
196 basisCard_eq_topologicalRank_of_finiteBasis C hQuot hcyc Fdata
197 have hBcardLe : Cardinal.mk B ≤ (n : Cardinal) := hBasisRank.trans_le hdHle
198 have hBcardNat : Fintype.card B ≤ Fintype.card (ULift (Fin n)) := by
199 have hleNat : Fintype.card B ≤ n := by
200 simpa [Nat.card_eq_fintype_card] using
201 Cardinal.toNat_le_toNat hBcardLe (Cardinal.natCast_lt_aleph0 (n := n))
202 simpa using hleNat
203 have hEmb : Nonempty (B ↪ ULift (Fin n)) :=
204 Function.Embedding.nonempty_of_card_le hBcardNat
205 let e : B ↪ ULift (Fin n) := Classical.choice hEmb
206 let κ : ULift (Fin n) → ↥(H : Subgroup F) :=
207 Function.extend e μ (fun _ => 1)
208 have hext : κ ∘ e = μ := by
209 simpa [κ] using
210 (Function.extend_comp e.injective μ (fun _ => (1 : ↥(H : Subgroup F))))
211 have hrange :
212 Set.range μ ⊆ Set.range κ := by
213 rintro z ⟨b, rfl⟩
214 refine ⟨e b, ?_⟩
215 exact congrArg (fun f => f b) hext
216 have hκgen :
217 Generation.TopologicallyGenerates (G := ↥(H : Subgroup F)) (Set.range κ) :=
218 Generation.topologicallyGenerates_mono (G := ↥(H : Subgroup F)) hμfree.generates_range hrange
219 have hκconv : Generation.ConvergesToOne (G := ↥(H : Subgroup F)) (Set.range κ) :=
220 Generation.ConvergesToOne.of_finite (G := ↥(H : Subgroup F)) (Set.finite_range κ)
221 exact ⟨κ, ⟨hκgen, hκconv⟩⟩
223/-- Finite-rank extension-closed variety case with the exact Schreier rank-transform cardinality. -/
225 (C : ProCGroups.FiniteGroupClass.{u})
226 (hVar : ProCGroups.FiniteGroupClass.Variety C)
227 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
228 (hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
229 (hcyc :
230 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
231 C A ∧ IsCyclic A ∧ Nontrivial A)
232 {X : Type u} [Finite X]
233 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
234 {ι : X → F}
235 [DiscreteTopology (Set.range ι)]
237 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
238 (H : OpenSubgroup F) :
239 ∃ Fdata : FreeProCGroupOnConvergingSetData
240 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
241 Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧
242 Cardinal.mk Fdata.basis =
243 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) :
244 Cardinal) := by
245 classical
246 rcases hVar.closureBundle_of_isomClosed_extensionClosed hIso hExt with
247 ⟨hForm, hSub, hIso', hQuot, hExt'⟩
248 let n : ℕ := _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F)))
250 C hForm hSub hIso' hQuot hExt' hF H with
251 ⟨B, hBfin, μ, hμfree⟩
252 letI : Finite B := hBfin
253 letI : Fintype B := Fintype.ofFinite B
254 let Fdata : FreeProCGroupOnConvergingSetData
255 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) :=
256 { basis := B
257 carrier := ↥(H : Subgroup F)
259 instTopologicalSpace := inferInstance
260 instIsTopologicalGroup := inferInstance
261 inclusion := μ
262 isFree := hμfree }
263 letI : Fintype X := Fintype.ofFinite X
264 let Fambient : FreeProCGroupOnConvergingSetData
265 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) :=
266 { basis := X
267 carrier := F
269 instTopologicalSpace := inferInstance
270 instIsTopologicalGroup := inferInstance
271 inclusion := ι
272 isFree := hF }
273 have hAmbientRank :
274 Cardinal.mk X = Generation.topologicalRank F :=
275 basisCard_eq_topologicalRank_of_finiteBasis C hQuot hcyc Fambient
276 have hdF : Generation.topologicalRank F = Nat.card X := by
277 calc
278 Generation.topologicalRank F = Cardinal.mk X := hAmbientRank.symm
279 _ = (Nat.card X : Cardinal) := by simp only [Cardinal.mk_fintype, Nat.card_eq_fintype_card]
280 have hdHle :
281 Generation.topologicalRank ↥(H : Subgroup F) ≤ (n : Cardinal) := by
282 simpa [n] using
284 (G := F) hF.isProC.1 hdF H
285 have hDataBasis :
286 Cardinal.mk Fdata.basis = Generation.topologicalRank Fdata.carrier :=
287 basisCard_eq_topologicalRank_of_finiteBasis C hQuot hcyc Fdata
288 have hle : Cardinal.mk Fdata.basis ≤ (n : Cardinal) := by
289 simpa [Fdata] using hDataBasis.trans_le hdHle
291 C hForm hSub hIso' hQuot hExt' hcyc hF H with
292 ⟨κ, hκ⟩
293 letI : TopologicalSpace (FreeGroup (ULift.{u} (Fin n))) := ⊥
294 letI : DiscreteTopology (FreeGroup (ULift.{u} (Fin n))) := ⟨rfl⟩
295 letI : IsTopologicalGroup (FreeGroup (ULift.{u} (Fin n))) := by infer_instance
296 let φ : FreeGroup (ULift.{u} (Fin n)) →ₜ* ↥(H : Subgroup F) :=
297 { toMonoidHom := FreeGroup.lift κ
298 continuous_toFun := continuous_of_discreteTopology }
299 have hComp :
302 (FreeGroup (ULift.{u} (Fin n))) ↥(H : Subgroup F) φ := by
303 letI : CompactSpace F := IsProCGroup.compactSpace hF.isProC
304 obtain ⟨Y, hYfree, hYcard⟩ :=
306 (F := F) (X := X) hF.generates_range H
307 let βF : FreeGroup X →* F := FreeGroup.lift ι
308 let L : Subgroup (FreeGroup X) := Subgroup.comap βF (H : Subgroup F)
309 let ψ : L →* ↥(H : Subgroup F) :=
310 { toFun := fun g => ⟨βF g.1, g.2⟩
312 map_mul' := by
313 intro a b
314 ext
316 letI : TopologicalSpace (FreeGroup X) := ⊥
317 letI : DiscreteTopology (FreeGroup X) := ⟨rfl⟩
318 letI : IsTopologicalGroup (FreeGroup X) := by infer_instance
319 have hβFdense : DenseRange βF :=
321 (F := F) (X := X) hF.generates_range
322 have hψdense : DenseRange ψ := by
323 exact denseRange_comapMap_of_openSubgroup (φ := βF) hβFdense H.isOpen'
324 letI : TopologicalSpace (FreeGroup Y) := ⊥
325 letI : DiscreteTopology (FreeGroup Y) := ⟨rfl⟩
326 letI : IsTopologicalGroup (FreeGroup Y) := by infer_instance
327 let bY : FreeGroupBasis Y L := Classical.choice hYfree
328 let eY : FreeGroup Y ≃* L := bY.repr.symm
329 let φY : FreeGroup Y →ₜ* ↥(H : Subgroup F) :=
330 { toMonoidHom := ψ.comp eY.toMonoidHom
331 continuous_toFun := continuous_of_discreteTopology }
332 have hψcont : Continuous ψ := by
333 simpa using (continuous_of_discreteTopology : Continuous ψ)
334 have hφYdense : DenseRange φY := by
335 simpa [φY] using
336 hψdense.comp (Function.Surjective.denseRange eY.surjective) hψcont
337 have hψfinite :
338 ∀ {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
339 [Finite Q] [DiscreteTopology Q],
340 C Q →
341 ∀ χL : L →* Q,
342 ∃! φbar : ↥(H : Subgroup F) →* Q,
343 Continuous φbar ∧ φbar.comp ψ = χL := by
344 intro Q _ _ _ _ _ hQ χL
345 rcases
347 (C := C)
348 (hForm := hForm) (hSub := hSub) (hIso := hIso')
349 (hQuot := hQuot) (hExt := hExt')
350 (X := X) (F := F) (ι := ι) hF H hQ χL with
351 ⟨φbar, hφbarCont, hφbarFac⟩
352 refine ⟨φbar, ⟨hφbarCont, hφbarFac⟩, ?_⟩
353 intro φbar' hφbar'
354 have hEq : (fun h : ↥(H : Subgroup F) => φbar h) = fun h => φbar' h := by
355 apply DenseRange.equalizer (f := ψ) hψdense
356 · exact hφbarCont
357 · exact hφbar'.1
358 · funext l
359 exact congrArg (fun f : L →* Q => f l) (hφbarFac.trans hφbar'.2.symm)
360 apply MonoidHom.ext
361 intro h
362 simpa using (congrArg (fun f : ↥(H : Subgroup F) → Q => f h) hEq).symm
363 have hfinite :
365 (C := C) H φY.toMonoidHom := by
367 (C := C) (H := H) (eY := eY) (ψ := ψ) hψfinite
368 have hCompY :
371 (FreeGroup Y) ↥(H : Subgroup F) φY := by
373 (C := C)
374 (hForm := hForm) (hSub := hSub) (hIso := hIso') (hQuot := hQuot)
375 (X := X) (F := F) (ι := ι) hF H hφYdense hfinite
376 exact
378 (C := C) hSub hIso' hQuot hcyc
379 (n := n) (Y := Y) (by simpa [n] using hYcard) hCompY hκ
380 let Fexact : FreeProCGroupOnConvergingSetData
381 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) :=
382 { basis := ULift.{u} (Fin n)
383 carrier := ↥(H : Subgroup F)
385 instTopologicalSpace := inferInstance
386 instIsTopologicalGroup := inferInstance
387 inclusion := κ
388 isFree := by
389 have hfree :=
391 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
392 (X := ULift.{u} (Fin n)) (Fhat := ↥(H : Subgroup F)) (ι := φ) hComp
393 convert hfree using 1
394 ext x
395 change ((κ x : ↥(H : Subgroup F)) : F) =
396 ((FreeGroup.lift κ (FreeGroup.of x) : ↥(H : Subgroup F)) : F)
397 simp only [FreeGroup.lift_apply_of]}
398 have hExactBasis :
399 Cardinal.mk Fexact.basis = Generation.topologicalRank Fexact.carrier :=
400 basisCard_eq_topologicalRank_of_finiteBasis C hQuot hcyc Fexact
401 have hExactCard : Cardinal.mk Fexact.basis = (n : Cardinal) := by
402 simp only [Cardinal.mk_fintype, Fintype.card_ulift, Fintype.card_fin, Fexact]
403 have hge : (n : Cardinal) ≤ Cardinal.mk Fdata.basis := by
404 exact le_of_eq <| by
405 calc
406 (n : Cardinal) = Cardinal.mk Fexact.basis := hExactCard.symm
407 _ = Generation.topologicalRank Fexact.carrier := hExactBasis
408 _ = Generation.topologicalRank Fdata.carrier := by rfl
409 _ = Cardinal.mk Fdata.basis := hDataBasis.symm
410 refine ⟨Fdata, ⟨ContinuousMulEquiv.refl _⟩, ?_⟩
411 have hCard : Cardinal.mk Fdata.basis = (n : Cardinal) := le_antisymm hle hge
412 simpa [n] using hCard
414/-- Finite-rank Schreier basis theorem using a bundled hypothesis record. -/
416 (C : ProCGroups.FiniteGroupClass.{u})
417 (hC : SchreierBasisFiniteRankHypotheses C)
418 {X : Type u} [Finite X]
419 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
420 {ι : X → F}
421 [DiscreteTopology (Set.range ι)]
423 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
424 (H : OpenSubgroup F) :
425 ∃ Fdata : FreeProCGroupOnConvergingSetData
426 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
427 Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧
428 Cardinal.mk Fdata.basis =
429 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) :
430 Cardinal) :=
432 (C := C) hC.variety hC.isomClosed hC.extensionClosed hC.hasNontrivialCyclic hF H
434/-- Finite-rank Melnikov-formation variant with explicit subgroup closure and exact Schreier
435rank-transform cardinality. -/
437 (C : ProCGroups.FiniteGroupClass.{u})
439 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
440 (hcyc :
441 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
442 C A ∧ IsCyclic A ∧ Nontrivial A)
443 {X : Type u} [Finite X]
444 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
445 {ι : X → F}
446 [DiscreteTopology (Set.range ι)]
448 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
449 (H : OpenSubgroup F) :
450 ∃ Fdata : FreeProCGroupOnConvergingSetData
451 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
452 Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧
453 Cardinal.mk Fdata.basis =
454 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) :
455 Cardinal) := by
456 let hVar : ProCGroups.FiniteGroupClass.Variety C :=
457 { subgroupClosed := hSub
458 quotientClosed := hC.quotientClosed
459 finiteProductClosed := hC.formation.finiteProductClosed }
460 exact
462 (C := C) hVar hC.isomClosed hC.extensionClosed hcyc hF H
464/-- Finite-rank Melnikov-formation open-subgroup variant. -/
466 (C : ProCGroups.FiniteGroupClass.{u})
468 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
469 (hcyc :
470 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
471 C A ∧ IsCyclic A ∧ Nontrivial A)
472 {X : Type u} [Finite X]
473 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
474 {ι : X → F}
475 [DiscreteTopology (Set.range ι)]
477 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
478 (H : OpenSubgroup F) :
479 ∃ Fdata : FreeProCGroupOnConvergingSetData
480 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
481 Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧
482 Cardinal.mk Fdata.basis =
483 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) :
484 Cardinal) :=
486 (C := C) hC hSub hcyc hF H
488/-- Finite-rank open-subnormal Melnikov statement. The current Schreier package records the
489expected bounded generating family converging to `1`; it does not claim that this family is already
490identified as a free pro-`C` basis. -/
492 (C : ProCGroups.FiniteGroupClass.{u})
493 {X : Type u} [Finite X]
494 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
495 {ι : X → F}
497 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
498 (H : OpenSubgroup F) :
499 ∃ (Y : Type u) (κ : Y → ↥(H : Subgroup F)),
500 Generation.GeneratesAndConvergesToOne (G := ↥(H : Subgroup F)) (Set.range κ) ∧
501 Cardinal.mk Y ≤
502 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) :
503 Cardinal) := by
504 classical
505 let hFprof : ProCGroups.IsProfiniteGroup F := hF.isProC.1
506 letI : CompactSpace F := ProCGroups.IsProfiniteGroup.compactSpace hFprof
507 letI : T2Space F := ProCGroups.IsProfiniteGroup.t2Space hFprof
508 letI : TotallyDisconnectedSpace F := ProCGroups.IsProfiniteGroup.totallyDisconnectedSpace hFprof
509 let hHprof : ProCGroups.IsProfiniteGroup ↥(H : Subgroup F) :=
510 ProCGroups.IsProfiniteGroup.of_isClosed_subgroup
511 (G := F) hFprof (H : Subgroup F)
512 (Subgroup.isClosed_of_isOpen (H : Subgroup F) H.isOpen')
513 have hdFleX : Generation.topologicalRank F ≤ (Nat.card X : Cardinal) := by
514 letI : Fintype X := Fintype.ofFinite X
515 calc
516 Generation.topologicalRank F ≤ Cardinal.mk (Set.range ι) := by
517 exact Generation.topologicalRank_le_mk_of_generatesAndConvergesToOne
518 (G := F)
519 ⟨hF.generates_range, hF.convergesToOne.range⟩
520 _ ≤ Cardinal.mk X := Cardinal.mk_range_le
521 _ = (Nat.card X : Cardinal) := by simp only [Cardinal.mk_fintype, Nat.card_eq_fintype_card]
522 have hdFlt : Generation.topologicalRank F < Cardinal.aleph0 :=
523 lt_of_le_of_lt hdFleX (Cardinal.natCast_lt_aleph0 (n := Nat.card X))
524 let d : ℕ := Cardinal.toNat (Generation.topologicalRank F)
525 have hdF : Generation.topologicalRank F = d := by
526 symm
527 exact Cardinal.cast_toNat_of_lt_aleph0 hdFlt
528 have hdle : d ≤ Nat.card X := by
529 simpa [d, Cardinal.toNat_natCast] using
530 Cardinal.toNat_le_toNat hdFleX (Cardinal.natCast_lt_aleph0 (n := Nat.card X))
531 have hdHle :
532 Generation.topologicalRank ↥(H : Subgroup F) ≤
533 (_root_.ReidemeisterSchreier.Schreier.rankTransform d (Nat.card (F ⧸ (H : Subgroup F))) : Cardinal) :=
535 (G := F) hFprof hdF H
536 have hRankMono :
537 _root_.ReidemeisterSchreier.Schreier.rankTransform d (Nat.card (F ⧸ (H : Subgroup F))) ≤
538 _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) :=
539 _root_.ReidemeisterSchreier.Schreier.rankTransform_mono_left hdle
540 rcases Generation.exists_generatorsConvergingToOne (G := ↥(H : Subgroup F)) hHprof with
541 ⟨S0, hS0⟩
542 rcases Generation.exists_generatesAndConvergesToOne_card_eq_topologicalRank
543 (G := ↥(H : Subgroup F)) ⟨S0, hS0⟩ with
544 ⟨S, hS, hScard⟩
545 let κ : S → ↥(H : Subgroup F) := Subtype.val
546 have hκrange : Set.range κ = S := by
547 ext z
548 constructor
549 · rintro ⟨s, rfl⟩
550 exact s.2
551 · intro hz
552 exact ⟨⟨z, hz⟩, rfl⟩
553 refine ⟨S, κ, ?_, ?_⟩
554 · simpa [κ, hκrange] using hS
555 · calc
556 Cardinal.mk S = Generation.topologicalRank ↥(H : Subgroup F) := hScard
557 _ ≤ (_root_.ReidemeisterSchreier.Schreier.rankTransform d (Nat.card (F ⧸ (H : Subgroup F))) : Cardinal) := hdHle
558 _ ≤ (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) :
559 Cardinal) := by
560 exact_mod_cast hRankMono
562/-- Finite discrete pointed input gives a finite converging-set basis model for every open
563subgroup, without an external pointed-to-converging-set bridge. -/
565 {C : ProCGroups.FiniteGroupClass.{u}}
566 (hForm : ProCGroups.FiniteGroupClass.Formation C)
567 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
568 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
569 (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
570 (hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
571 {X : Type u} [TopologicalSpace X] [CompactSpace X] [Finite X]
572 {x0 : X}
573 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
574 {ι : X → F}
575 (hF : IsPointedFreeProCGroupOn
576 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X x0 F ι)
577 (H : OpenSubgroup F) :
578 ∃ Fdata : FreeProCGroupOnConvergingSetData
579 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
580 Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧ Finite Fdata.basis := by
581 classical
582 letI : CompactSpace F := IsProCGroup.compactSpace hF.isProC
583 letI : T2Space F := IsProCGroup.t2Space hF.isProC
584 rcases
586 (C := C) hForm hSub hIso hQuot hExt hF H with
587 ⟨κ, _hκcont, _hκbase, _hκone, _hκcompact, _hκclosed, hκfree⟩
588 letI : Finite (OpenSubgroupRightQuotient H) :=
589 finite_openSubgroupRightQuotient (F := F) H
590 letI : Finite (Set.range κ) := (Set.finite_range κ).to_subtype
591 letI : DiscreteTopology (Set.range κ) :=
592 DiscreteTopology.of_finite_of_isClosed_singleton fun _ => isClosed_singleton
593 exact
595 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) hκfree
599end Profinite
600end ReidemeisterSchreier