ReidemeisterSchreier/Profinite/OpenSubgroups/BasisCardinalRank.lean

1import ReidemeisterSchreier.Profinite.OpenSubgroups.BasisFiniteRank

2import ReidemeisterSchreier.Profinite.OpenSubgroups.BasisInfiniteRank

4/-

5PUBLIC_PAGE_SNAPSHOT

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

7lean_source: lean4/ReidemeisterSchreier/Profinite/OpenSubgroups/BasisCardinalRank.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 cardinal-rank Schreier basis theorem.

31The bridge is only needed in the infinite-rank branch, but bundling it here gives a single

32public theorem whose conclusion uses `schreierRankTransformCardinal`. -/

33structure SchreierBasisCardinalRankHypotheses

34 (C : ProCGroups.FiniteGroupClass.{u}) : Prop where

35 bridge : PointedToConvergingSetBasisBridge

36 (ProCGroups.ProC.finiteGroupClassProCPredicate C)

37 variety : ProCGroups.FiniteGroupClass.Variety C

38 isomClosed : ProCGroups.FiniteGroupClass.IsomClosed C

39 extensionClosed : ProCGroups.FiniteGroupClass.ExtensionClosed C

40 hasNontrivialCyclic :

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

42 C A ∧ IsCyclic A ∧ Nontrivial A

44/-- Cardinal-rank Schreier basis theorem for extension-closed varieties.

46This is the public cardinal layer: finite bases give the classical finite Schreier transform,

47and infinite bases stabilize at the ambient basis cardinal. -/

48theorem exists_basis_openSubgroup_of_extensionClosed_cardinalRank

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

50 (hBridge :

51 PointedToConvergingSetBasisBridge (ProCGroups.ProC.finiteGroupClassProCPredicate C))

52 (hVar : ProCGroups.FiniteGroupClass.Variety C)

53 (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)

54 (hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)

55 (hcyc :

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

57 C A ∧ IsCyclic A ∧ Nontrivial A)

58 {X : Type u}

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

60 {ι : X → F}

61 [DiscreteTopology (Set.range ι)]

62 (hF : IsFreeProCGroupOnConvergingSet

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

64 (H : OpenSubgroup F) :

65 ∃ Fdata : FreeProCGroupOnConvergingSetData

66 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),

67 Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧

68 Cardinal.mk Fdata.basis =

69 schreierRankTransformCardinal (Cardinal.mk X)

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

71 classical

72 by_cases hXfin : Finite X

73 · letI : Finite X := hXfin

74 rcases exists_basis_openSubgroup_of_extensionClosed_finiteRank

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

76 ⟨Fdata, hFdataEquiv, hFdataCard⟩

77 refine ⟨Fdata, hFdataEquiv, ?_⟩

78 calc

79 Cardinal.mk Fdata.basis =

80 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X)

81 (Nat.card (F ⧸ (H : Subgroup F))) : Cardinal) := hFdataCard

82 _ = schreierRankTransformCardinal (Cardinal.mk X)

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

84 exact (schreierRankTransformCardinal_mk_finite X

85 (Nat.card (F ⧸ (H : Subgroup F)))).symm

86 · haveI : Infinite X := not_finite_iff_infinite.1 hXfin

87 rcases exists_basis_openSubgroup_of_extensionClosed_infiniteRank

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

89 ⟨Fdata, hFdataEquiv, hFdataCard⟩

90 refine ⟨Fdata, hFdataEquiv, ?_⟩

91 calc

92 Cardinal.mk Fdata.basis = Cardinal.mk X := hFdataCard

93 _ = schreierRankTransformCardinal (Cardinal.mk X)

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

95 exact (schreierRankTransformCardinal_mk_infinite X

96 (Nat.card (F ⧸ (H : Subgroup F)))).symm

98/-- Cardinal-rank Schreier basis theorem using the bundled cardinal-rank hypotheses. -/

99theorem exists_basis_openSubgroup_of_cardinalRank_of_schreierBasisHypotheses

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

101 (hC : SchreierBasisCardinalRankHypotheses C)

102 {X : Type u}

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

104 {ι : X → F}

105 [DiscreteTopology (Set.range ι)]

106 (hF : IsFreeProCGroupOnConvergingSet

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

108 (H : OpenSubgroup F) :

109 ∃ Fdata : FreeProCGroupOnConvergingSetData

110 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),

111 Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧

112 Cardinal.mk Fdata.basis =

113 schreierRankTransformCardinal (Cardinal.mk X)

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

115 exists_basis_openSubgroup_of_extensionClosed_cardinalRank

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

117 hC.hasNontrivialCyclic hF H

118

119/-- Cardinal-rank Melnikov-formation variant with explicit subgroup closure. -/

120theorem exists_basis_openSubgroup_of_melnikovFormation_cardinalRank_of_subgroupClosed

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

122 (hBridge :

123 PointedToConvergingSetBasisBridge (ProCGroups.ProC.finiteGroupClassProCPredicate C))

124 (hC : ProCGroups.FiniteGroupClass.MelnikovFormation C)

125 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)

126 (hcyc :

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

128 C A ∧ IsCyclic A ∧ Nontrivial A)

129 {X : Type u}

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

131 {ι : X → F}

132 [DiscreteTopology (Set.range ι)]

133 (hF : IsFreeProCGroupOnConvergingSet

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

135 (H : OpenSubgroup F) :

136 ∃ Fdata : FreeProCGroupOnConvergingSetData

137 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),

138 Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧

139 Cardinal.mk Fdata.basis =

140 schreierRankTransformCardinal (Cardinal.mk X)

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

142 classical

143 by_cases hXfin : Finite X

144 · letI : Finite X := hXfin

145 rcases exists_basis_openSubgroup_of_melnikovFormation_finiteRank_of_subgroupClosed

146 (C := C) hC hSub hcyc hF H with

147 ⟨Fdata, hFdataEquiv, hFdataCard⟩

148 refine ⟨Fdata, hFdataEquiv, ?_⟩

149 calc

150 Cardinal.mk Fdata.basis =

151 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X)

152 (Nat.card (F ⧸ (H : Subgroup F))) : Cardinal) := hFdataCard

153 _ = schreierRankTransformCardinal (Cardinal.mk X)

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

155 exact (schreierRankTransformCardinal_mk_finite X

156 (Nat.card (F ⧸ (H : Subgroup F)))).symm

157 · haveI : Infinite X := not_finite_iff_infinite.1 hXfin

158 rcases exists_basis_openSubgroup_of_melnikovFormation_infiniteRank_of_subgroupClosed

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

160 ⟨Fdata, hFdataEquiv, hFdataCard⟩

161 refine ⟨Fdata, hFdataEquiv, ?_⟩

162 calc

163 Cardinal.mk Fdata.basis = Cardinal.mk X := hFdataCard

164 _ = schreierRankTransformCardinal (Cardinal.mk X)

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

166 exact (schreierRankTransformCardinal_mk_infinite X

167 (Nat.card (F ⧸ (H : Subgroup F)))).symm

168

169/-- Cardinal-rank Melnikov-formation open-subgroup variant. -/

170theorem exists_basis_openNormalSubgroup_of_melnikovFormation_cardinalRank

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

172 (hBridge :

173 PointedToConvergingSetBasisBridge (ProCGroups.ProC.finiteGroupClassProCPredicate C))

174 (hC : ProCGroups.FiniteGroupClass.MelnikovFormation C)

175 (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)

176 (hcyc :

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

178 C A ∧ IsCyclic A ∧ Nontrivial A)

179 {X : Type u}

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

181 {ι : X → F}

182 [DiscreteTopology (Set.range ι)]

183 (hF : IsFreeProCGroupOnConvergingSet

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

185 (H : OpenSubgroup F) :

186 ∃ Fdata : FreeProCGroupOnConvergingSetData

187 (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),

188 Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧

189 Cardinal.mk Fdata.basis =

190 schreierRankTransformCardinal (Cardinal.mk X)

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

192 classical

193 by_cases hXfin : Finite X

194 · letI : Finite X := hXfin

195 rcases exists_basis_openNormalSubgroup_of_melnikovFormation_finiteRank

196 (C := C) hC hSub hcyc hF H with

197 ⟨Fdata, hFdataEquiv, hFdataCard⟩

198 refine ⟨Fdata, hFdataEquiv, ?_⟩

199 calc

200 Cardinal.mk Fdata.basis =

201 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X)

202 (Nat.card (F ⧸ (H : Subgroup F))) : Cardinal) := hFdataCard

203 _ = schreierRankTransformCardinal (Cardinal.mk X)

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

205 exact (schreierRankTransformCardinal_mk_finite X

206 (Nat.card (F ⧸ (H : Subgroup F)))).symm

207 · haveI : Infinite X := not_finite_iff_infinite.1 hXfin

208 rcases exists_basis_openNormalSubgroup_of_melnikovFormation_infiniteRank

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

210 ⟨Fdata, hFdataEquiv, hFdataCard⟩

211 refine ⟨Fdata, hFdataEquiv, ?_⟩

212 calc

213 Cardinal.mk Fdata.basis = Cardinal.mk X := hFdataCard

214 _ = schreierRankTransformCardinal (Cardinal.mk X)

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

216 exact (schreierRankTransformCardinal_mk_infinite X

217 (Nat.card (F ⧸ (H : Subgroup F)))).symm

218

219end Profinite

220end ReidemeisterSchreier