ReidemeisterSchreier/Profinite/OpenSubgroups/BasisInfiniteRank.lean
1import ReidemeisterSchreier.Profinite.OpenSubgroups.BasisTheorems
2import ProCGroups.LocalWeight.LocalWeightTheorems
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ReidemeisterSchreier/Profinite/OpenSubgroups/BasisInfiniteRank.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 infinite-rank Schreier basis theorem. This mirrors
30`SchreierBasisFiniteRankHypotheses`, with the additional bridge needed in the infinite-rank
31argument. -/
32structure SchreierBasisInfiniteRankHypotheses
33 (C : ProCGroups.FiniteGroupClass.{u}) : Prop where
36 isomClosed : ProCGroups.FiniteGroupClass.IsomClosed C
38 hasNontrivialCyclic :
39 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
40 C A ∧ IsCyclic A ∧ Nontrivial A
43/-- Infinite-rank extension-closed variety case. The basis of every open subgroup has the same
44cardinality as the ambient converging-set basis. -/
46 (C : ProCGroups.FiniteGroupClass.{u})
47 (hBridge :
49 (hVar : ProCGroups.FiniteGroupClass.Variety C)
50 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
51 (hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
52 (hcyc :
53 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
54 C A ∧ IsCyclic A ∧ Nontrivial A)
55 {X : Type u} [Infinite X]
56 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
57 {ι : X → F}
58 [DiscreteTopology (Set.range ι)]
60 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
61 (H : OpenSubgroup F) :
62 ∃ Fdata : FreeProCGroupOnConvergingSetData
63 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
64 Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧
65 Cardinal.mk Fdata.basis = Cardinal.mk X := by
66 classical
67 let hFprof : ProCGroups.IsProfiniteGroup F := hF.isProC.1
68 letI : CompactSpace F := ProCGroups.IsProfiniteGroup.compactSpace hFprof
69 letI : T2Space F := ProCGroups.IsProfiniteGroup.t2Space hFprof
70 letI : TotallyDisconnectedSpace F := ProCGroups.IsProfiniteGroup.totallyDisconnectedSpace hFprof
71 let hHprof : ProCGroups.IsProfiniteGroup ↥(H : Subgroup F) :=
72 ProCGroups.IsProfiniteGroup.of_isClosed_subgroup
73 (G := F) hFprof (H : Subgroup F)
74 (Subgroup.isClosed_of_isOpen (H : Subgroup F) H.isOpen')
76 C hVar.quotientClosed hcyc with
77 ⟨A, _instGroupA, _instTopA, _instTopGroupA, hA, a, ha1, hgena⟩
78 have hnontrivial :
79 ∃ (A : Type u) (_ : Group A) (_ : TopologicalSpace A) (_ : IsTopologicalGroup A),
80 (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := A) ∧
81 ∃ a : A, a ≠ 1 ∧ Generation.TopologicallyGenerates (G := A) ({a} : Set A) :=
82 ⟨A, inferInstance, inferInstance, inferInstance, hA, a, ha1, hgena⟩
83 have hιinj : Function.Injective ι :=
84 freeProCGroupOnConvergingSet_injective (hι := hF) hnontrivial
85 have hRangeInf : Set.Infinite (Set.range ι) :=
86 ProCGroups.LocalWeight.setInfinite_of_cardinal_ge_aleph0 (X := Set.range ι) <| by
87 calc
88 Cardinal.aleph0 ≤ Cardinal.mk X := Cardinal.aleph0_le_mk X
89 _ = Cardinal.mk (Set.range ι) := by
90 simpa using (Cardinal.mk_range_eq ι hιinj).symm
91 have hXlw : Cardinal.mk X = ProCGroups.LocalWeight.localWeight F := by
92 calc
93 Cardinal.mk X = Cardinal.mk (Set.range ι) := by
94 simpa using (Cardinal.mk_range_eq ι hιinj).symm
95 _ = ProCGroups.LocalWeight.localWeight F := by
97 (G := F) (Set.range ι) hFprof
98 ⟨hF.generates_range, hF.convergesToOne.range⟩ hRangeInf
99 letI : TopologicalSpace X := ⊥
100 letI : DiscreteTopology X := ⟨rfl⟩
102 (C := C) hBridge hVar hIso hExt hF H with
103 ⟨Fdata, ⟨e⟩⟩
104 have hBasisInf : Infinite Fdata.basis := by
105 by_contra hFin
106 have hBasisFin : Finite Fdata.basis := not_infinite_iff_finite.mp hFin
107 letI : Finite Fdata.basis := hBasisFin
108 letI : Fintype Fdata.basis := Fintype.ofFinite Fdata.basis
109 have hCarrierFg :
110 ProCGroups.FiniteGeneration.TopologicallyFinitelyGenerated Fdata.carrier := by
111 refine ⟨Finset.univ.image Fdata.inclusion, ?_⟩
112 simpa [Finset.coe_image] using Fdata.isFree.generates_range
113 let φ : ContinuousMonoidHom Fdata.carrier ↥(H : Subgroup F) := {
114 toMonoidHom := e.toMonoidHom
115 continuous_toFun := e.continuous_toFun
116 }
117 have hHfg :
118 ProCGroups.FiniteGeneration.TopologicallyFinitelyGenerated ↥(H : Subgroup F) :=
119 ProCGroups.FiniteGeneration.topologicallyFinitelyGenerated_of_continuousSurjective
120 φ e.surjective hCarrierFg
121 have hFfg :
124 have hXfin : Finite X :=
126 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
127 (F := F) (ι := ι) hFprof hFfg hF hnontrivial
128 exact (not_infinite_iff_finite.mpr hXfin) inferInstance
129 have hFdataInj : Function.Injective Fdata.inclusion :=
130 freeProCGroupOnConvergingSet_injective (hι := Fdata.isFree) hnontrivial
131 let μ : Fdata.basis → ↥(H : Subgroup F) := fun x => e (Fdata.inclusion x)
132 have hμinj : Function.Injective μ := e.injective.comp hFdataInj
133 have hμrangeInf : Set.Infinite (Set.range μ) :=
134 ProCGroups.LocalWeight.setInfinite_of_cardinal_ge_aleph0 (X := Set.range μ) <| by
135 calc
136 Cardinal.aleph0 ≤ Cardinal.mk Fdata.basis := Cardinal.aleph0_le_mk Fdata.basis
137 _ = Cardinal.mk (Set.range μ) := by
138 simpa using (Cardinal.mk_range_eq μ hμinj).symm
139 have hFdataProf : ProCGroups.IsProfiniteGroup Fdata.carrier := Fdata.isFree.isProC.1
140 have hμgc :
141 Generation.GeneratesAndConvergesToOne (G := ↥(H : Subgroup F)) (Set.range μ) := by
142 let X0 : Set Fdata.carrier := Set.range Fdata.inclusion
143 have hX0 :
144 Generation.GeneratesAndConvergesToOne (G := Fdata.carrier) X0 := by
145 exact ⟨Fdata.isFree.generates_range, Fdata.isFree.convergesToOne.range⟩
146 have hImg :
147 Generation.GeneratesAndConvergesToOne (G := ↥(H : Subgroup F)) (e '' X0) :=
148 Generation.GeneratesAndConvergesToOne.image_of_continuousMulEquiv
149 (G := Fdata.carrier) hFdataProf e hX0
150 have hRange : e '' X0 = Set.range μ := by
151 ext y
152 constructor
153 · rintro ⟨x, ⟨b, rfl⟩, rfl⟩
154 exact ⟨b, rfl⟩
155 · rintro ⟨b, rfl⟩
156 exact ⟨Fdata.inclusion b, ⟨b, rfl⟩, rfl⟩
157 simpa [X0, μ, hRange] using hImg
158 have hμlw :
159 Cardinal.mk Fdata.basis = ProCGroups.LocalWeight.localWeight ↥(H : Subgroup F) := by
160 calc
161 Cardinal.mk Fdata.basis = Cardinal.mk (Set.range μ) := by
162 simpa using (Cardinal.mk_range_eq μ hμinj).symm
163 _ = ProCGroups.LocalWeight.localWeight ↥(H : Subgroup F) := by
165 (G := ↥(H : Subgroup F)) (Set.range μ) hHprof hμgc hμrangeInf
166 exact
167 ⟨Fdata, ⟨e⟩,
168 hμlw.trans ((ProCGroups.LocalWeight.localWeight_openSubgroup_eq F H).trans
169 hXlw.symm)⟩
171/-- Infinite-rank Schreier basis theorem using a bundled hypothesis record. -/
173 (C : ProCGroups.FiniteGroupClass.{u})
174 (hC : SchreierBasisInfiniteRankHypotheses C)
175 {X : Type u} [Infinite X]
176 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
177 {ι : X → F}
178 [DiscreteTopology (Set.range ι)]
180 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
181 (H : OpenSubgroup F) :
182 ∃ Fdata : FreeProCGroupOnConvergingSetData
183 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
184 Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧
185 Cardinal.mk Fdata.basis = Cardinal.mk X :=
187 (C := C) hC.bridge hC.variety hC.isomClosed hC.extensionClosed hC.hasNontrivialCyclic hF H
189/-- Infinite-rank Melnikov-formation variant with explicit subgroup closure. -/
191 (C : ProCGroups.FiniteGroupClass.{u})
192 (hBridge :
195 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
196 (hcyc :
197 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
198 C A ∧ IsCyclic A ∧ Nontrivial A)
199 {X : Type u} [Infinite X]
200 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
201 {ι : X → F}
202 [DiscreteTopology (Set.range ι)]
204 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
205 (H : OpenSubgroup F) :
206 ∃ Fdata : FreeProCGroupOnConvergingSetData
207 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
208 Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧
209 Cardinal.mk Fdata.basis = Cardinal.mk X := by
210 let hVar : ProCGroups.FiniteGroupClass.Variety C :=
211 { subgroupClosed := hSub
212 quotientClosed := hC.quotientClosed
213 finiteProductClosed := hC.formation.finiteProductClosed }
214 exact
216 (C := C) hBridge hVar hC.isomClosed hC.extensionClosed hcyc hF H
218/-- Infinite-rank Melnikov-formation open-subgroup variant. -/
220 (C : ProCGroups.FiniteGroupClass.{u})
221 (hBridge :
224 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
225 (hcyc :
226 ∃ (A : Type u) (_ : Group A) (_ : Finite A),
227 C A ∧ IsCyclic A ∧ Nontrivial A)
228 {X : Type u} [Infinite X]
229 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
230 {ι : X → F}
231 [DiscreteTopology (Set.range ι)]
233 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
234 (H : OpenSubgroup F) :
235 ∃ Fdata : FreeProCGroupOnConvergingSetData
236 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
237 Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧
238 Cardinal.mk Fdata.basis = Cardinal.mk X :=
240 (C := C) hBridge hC hSub hcyc hF H
244end Profinite
245end ReidemeisterSchreier