ReidemeisterSchreier/Profinite/OpenSubgroups/GeneratingFamilies.lean

1import ProCGroups.Generation.GeneratingFamilies

2import ReidemeisterSchreier.Profinite.OpenSubgroups.BasisCardinalRank

4/-

5PUBLIC_PAGE_SNAPSHOT

6generated_at: 2026-05-27T09:47:29+09:00

7lean_source: lean4/ReidemeisterSchreier/Profinite/OpenSubgroups/GeneratingFamilies.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.Generation

26open ProCGroups.ProC

28universe u

30/-- A free pro-`C` basis on a fixed carrier. -/

31structure FreeProCBasis

32 (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})

33 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] where

34 index : Type u

35 inclusion : index → G

36 isFree : IsFreeProCGroupOnConvergingSet (ProC := ProC) index G inclusion

38namespace FreeProCBasis

40variable {ProC : ProCGroups.ProC.ProCGroupPredicate.{u}}

41variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

43instance instCoeFunFreeProCBasis : CoeFun (FreeProCBasis ProC G) (fun basis => basis.index → G) where

44 coe basis := basis.inclusion

46@[simp] theorem inclusion_eq_coe (basis : FreeProCBasis ProC G) :

47 basis.inclusion = (basis : basis.index → G) := rfl

49/-- The cardinality of the basis index. -/

50def cardinal (basis : FreeProCBasis ProC G) : Cardinal :=

51 Cardinal.mk basis.index

53/-- A free pro-`C` basis forgets to a topological generating family. -/

54def toGeneratingFamily (basis : FreeProCBasis ProC G) :

55 TopologicalGeneratingFamily G where

56 index := basis.index

57 toFun := basis

58 convergesToOne := basis.isFree.convergesToOne

59 generates := basis.isFree.generates_range

61/-- Forget the fixed-carrier basis to the existing carrier-and-basis data structure. -/

62def toData (basis : FreeProCBasis ProC G) :

63 FreeProCGroupOnConvergingSetData (ProC := ProC) where

64 basis := basis.index

65 carrier := G

66 instGroup := inferInstance

67 instTopologicalSpace := inferInstance

68 instIsTopologicalGroup := inferInstance

69 inclusion := basis.inclusion

70 isFree := basis.isFree

72/-- Repackage existing carrier-and-basis data as a fixed-carrier basis. -/

73def ofData (data : FreeProCGroupOnConvergingSetData (ProC := ProC)) :

74 FreeProCBasis ProC data.carrier where

75 index := data.basis

76 inclusion := data.inclusion

77 isFree := data.isFree

79end FreeProCBasis

81/-- A free pro-`C` basis model for a target group, up to continuous multiplicative equivalence. -/

82structure FreeProCBasisModel

83 (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})

84 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] where

85 carrier : Type u

86 instGroup : Group carrier

87 instTopologicalSpace : TopologicalSpace carrier

88 instIsTopologicalGroup : IsTopologicalGroup carrier

89 basis : FreeProCBasis ProC carrier

90 equiv : carrier ≃ₜ* G

92attribute [instance] FreeProCBasisModel.instGroup

93attribute [instance] FreeProCBasisModel.instTopologicalSpace

94attribute [instance] FreeProCBasisModel.instIsTopologicalGroup

96namespace FreeProCBasisModel

98variable {ProC : ProCGroups.ProC.ProCGroupPredicate.{u}}

99variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

100

101/-- The cardinality of the modeled free pro-`C` basis. -/

102def basisCardinal (model : FreeProCBasisModel ProC G) : Cardinal :=

103 model.basis.cardinal

104

105/-- Turn existing carrier-and-basis data plus an equivalence to the target into a basis model. -/

106def ofData (data : FreeProCGroupOnConvergingSetData (ProC := ProC)) (e : data.carrier ≃ₜ* G) :

107 FreeProCBasisModel ProC G where

108 carrier := data.carrier

109 instGroup := data.instGroup

110 instTopologicalSpace := data.instTopologicalSpace

111 instIsTopologicalGroup := data.instIsTopologicalGroup

112 basis := FreeProCBasis.ofData data

113 equiv := e

114

115end FreeProCBasisModel

116

117/-- Correctly named generating-family statement for the finite-rank open-subnormal result. -/

118theorem exists_generatingFamily_openSubnormalSubgroup_of_melnikovFormation_finiteRank

119 (C : ProCGroups.FiniteGroupClass.{u})

120 {X : Type u} [Finite X]

121 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]

122 {ι : X → F}

123 (hF : IsFreeProCGroupOnConvergingSet

124 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)

125 (H : OpenSubgroup F) :

126 ∃ family : TopologicalGeneratingFamily ↥(H : Subgroup F),

127 family.cardinal ≤

128 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) :

129 Cardinal) := by

130 classical

131 rcases exists_basis_openSubnormalSubgroup_of_melnikovFormation_finiteRank

132 (C := C) hF H with

133 ⟨Y, κ, hκ, hκcard⟩

134 have hYfinite : Finite Y :=

135 (Cardinal.lt_aleph0_iff_finite (α := Y)).mp <|

136 lt_of_le_of_lt hκcard

137 (Cardinal.natCast_lt_aleph0

138 (n := _root_.ReidemeisterSchreier.Schreier.rankTransform

139 (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F)))))

140 letI : Finite Y := hYfinite

141 let family : TopologicalGeneratingFamily ↥(H : Subgroup F) :=

142 { index := Y

143 toFun := κ

144 convergesToOne := FamilyConvergesToOne.of_finite_domain (G := ↥(H : Subgroup F)) κ

145 generates := hκ.1 }

146 exact ⟨family, by simpa [TopologicalGeneratingFamily.cardinal, family] using hκcard⟩

147

148/-- Cardinal-rank extension-closed basis theorem, with the conclusion explicitly packaged as a

149free pro-`C` basis model rather than only a generating family. -/

150theorem exists_freeProCBasisModel_openSubgroup_of_extensionClosed_cardinalRank

151 (C : ProCGroups.FiniteGroupClass.{u})

152 (hBridge :

153 PointedToConvergingSetBasisBridge (ProCGroups.ProC.finiteGroupClassProCPredicate C))

154 (hVar : ProCGroups.FiniteGroupClass.Variety C)

155 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)

156 (hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)

157 (hcyc :

158 ∃ (A : Type u) (_ : Group A) (_ : Finite A),

159 C A ∧ IsCyclic A ∧ Nontrivial A)

160 {X : Type u}

161 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]

162 {ι : X → F}

163 [DiscreteTopology (Set.range ι)]

164 (hF : IsFreeProCGroupOnConvergingSet

165 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)

166 (H : OpenSubgroup F) :

167 ∃ model : FreeProCBasisModel

168 (ProCGroups.ProC.finiteGroupClassProCPredicate C) ↥(H : Subgroup F),

169 model.basisCardinal =

170 schreierRankTransformCardinal (Cardinal.mk X)

171 (Nat.card (F ⧸ (H : Subgroup F))) := by

172 rcases exists_basis_openSubgroup_of_extensionClosed_cardinalRank

173 (C := C) hBridge hVar hIso hExt hcyc hF H with

174 ⟨data, ⟨e⟩, hcard⟩

175 let model : FreeProCBasisModel

176 (ProCGroups.ProC.finiteGroupClassProCPredicate C) ↥(H : Subgroup F) :=

177 FreeProCBasisModel.ofData data e

178 refine ⟨model, ?_⟩

179 simpa [model, FreeProCBasisModel.basisCardinal, FreeProCBasisModel.ofData,

180 FreeProCBasis.cardinal, FreeProCBasis.ofData] using hcard

181

182/-- Bundled-hypothesis cardinal-rank basis theorem, with a basis-model conclusion. -/

183theorem exists_freeProCBasisModel_openSubgroup_of_cardinalRank_of_schreierBasisHypotheses

184 (C : ProCGroups.FiniteGroupClass.{u})

185 (hC : SchreierBasisCardinalRankHypotheses C)

186 {X : Type u}

187 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]

188 {ι : X → F}

189 [DiscreteTopology (Set.range ι)]

190 (hF : IsFreeProCGroupOnConvergingSet

191 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)

192 (H : OpenSubgroup F) :

193 ∃ model : FreeProCBasisModel

194 (ProCGroups.ProC.finiteGroupClassProCPredicate C) ↥(H : Subgroup F),

195 model.basisCardinal =

196 schreierRankTransformCardinal (Cardinal.mk X)

197 (Nat.card (F ⧸ (H : Subgroup F))) :=

198 exists_freeProCBasisModel_openSubgroup_of_extensionClosed_cardinalRank

199 (C := C) hC.bridge hC.variety hC.isomClosed hC.extensionClosed

200 hC.hasNontrivialCyclic hF H

201

202/-- Cardinal-rank Melnikov-formation variant, with a basis-model conclusion. -/

203theorem exists_freeProCBasisModel_openSubgroup_of_melnikovRank

204 (C : ProCGroups.FiniteGroupClass.{u})

205 (hBridge :

206 PointedToConvergingSetBasisBridge (ProCGroups.ProC.finiteGroupClassProCPredicate C))

207 (hC : ProCGroups.FiniteGroupClass.MelnikovFormation C)

208 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)

209 (hcyc :

210 ∃ (A : Type u) (_ : Group A) (_ : Finite A),

211 C A ∧ IsCyclic A ∧ Nontrivial A)

212 {X : Type u}

213 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]

214 {ι : X → F}

215 [DiscreteTopology (Set.range ι)]

216 (hF : IsFreeProCGroupOnConvergingSet

217 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)

218 (H : OpenSubgroup F) :

219 ∃ model : FreeProCBasisModel

220 (ProCGroups.ProC.finiteGroupClassProCPredicate C) ↥(H : Subgroup F),

221 model.basisCardinal =

222 schreierRankTransformCardinal (Cardinal.mk X)

223 (Nat.card (F ⧸ (H : Subgroup F))) := by

224 rcases exists_basis_openSubgroup_of_melnikovFormation_cardinalRank_of_subgroupClosed

225 (C := C) hBridge hC hSub hcyc hF H with

226 ⟨data, ⟨e⟩, hcard⟩

227 let model : FreeProCBasisModel

228 (ProCGroups.ProC.finiteGroupClassProCPredicate C) ↥(H : Subgroup F) :=

229 FreeProCBasisModel.ofData data e

230 refine ⟨model, ?_⟩

231 simpa [model, FreeProCBasisModel.basisCardinal, FreeProCBasisModel.ofData,

232 FreeProCBasis.cardinal, FreeProCBasis.ofData] using hcard

233

234/-- Cardinal-rank Melnikov-formation open-subgroup variant, with a basis-model conclusion. -/

235theorem exists_freeProCBasisModel_openNormalSubgroup_of_melnikovFormation_cardinalRank

236 (C : ProCGroups.FiniteGroupClass.{u})

237 (hBridge :

238 PointedToConvergingSetBasisBridge (ProCGroups.ProC.finiteGroupClassProCPredicate C))

239 (hC : ProCGroups.FiniteGroupClass.MelnikovFormation C)

240 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)

241 (hcyc :

242 ∃ (A : Type u) (_ : Group A) (_ : Finite A),

243 C A ∧ IsCyclic A ∧ Nontrivial A)

244 {X : Type u}

245 {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]

246 {ι : X → F}

247 [DiscreteTopology (Set.range ι)]

248 (hF : IsFreeProCGroupOnConvergingSet

249 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)

250 (H : OpenSubgroup F) :

251 ∃ model : FreeProCBasisModel

252 (ProCGroups.ProC.finiteGroupClassProCPredicate C) ↥(H : Subgroup F),

253 model.basisCardinal =

254 schreierRankTransformCardinal (Cardinal.mk X)

255 (Nat.card (F ⧸ (H : Subgroup F))) := by

256 rcases exists_basis_openNormalSubgroup_of_melnikovFormation_cardinalRank

257 (C := C) hBridge hC hSub hcyc hF H with

258 ⟨data, ⟨e⟩, hcard⟩

259 let model : FreeProCBasisModel

260 (ProCGroups.ProC.finiteGroupClassProCPredicate C) ↥(H : Subgroup F) :=

261 FreeProCBasisModel.ofData data e

262 refine ⟨model, ?_⟩

263 simpa [model, FreeProCBasisModel.basisCardinal, FreeProCBasisModel.ofData,

264 FreeProCBasis.cardinal, FreeProCBasis.ofData] using hcard

265

266end Profinite

267end ReidemeisterSchreier