Source: ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.RankBound

1import ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.FreeBasis

2import ProCGroups.GroupTheory.Subgroups

3import ProCGroups.FiniteGeneration.Basic

5/-!

6# Cardinal and finite-rank Schreier bounds

8This module defines the cardinal Schreier transform, proves its finite and

9infinite simplifications, and bounds the topological rank of an open subgroup

10of a compact Hausdorff totally disconnected group by the classical finite

11rank transform.

12-/

14open Set

15open scoped Topology Pointwise

17namespace ReidemeisterSchreier

18namespace Profinite

20open ProCGroups

21open ProCGroups.FiniteGeneration

22open ReidemeisterSchreier.Discrete.OpenSubgroups

24universe u

26/--

27Cardinal form of the Schreier rank transform for an open subgroup of finite index \(n\). For

28finite rank this is the usual Schreier transform \(1+n(d-1)\). For infinite cardinals the

29finite-index transform stabilizes at the original cardinal.

30-/

31noncomputable def schreierRankTransformCardinal (κ : Cardinal) (n : ℕ) : Cardinal :=

32 if _ : κ < Cardinal.aleph0 then

33 (_root_.ReidemeisterSchreier.Schreier.rankTransform κ.toNat n : Cardinal)

34 else κ

36/-- On a finite cardinal, the cardinal Schreier transform agrees with the usual natural-number formula. -/

37@[simp] theorem schreierRankTransformCardinal_natCast (d n : ℕ) :

38 schreierRankTransformCardinal (d : Cardinal) n =

39 (_root_.ReidemeisterSchreier.Schreier.rankTransform d n : Cardinal) := by

40 simp only [schreierRankTransformCardinal, Cardinal.natCast_lt_aleph0, ↓reduceDIte,

41 Cardinal.toNat_natCast]

43/-- A finite-index Schreier transform fixes every infinite cardinal. -/

44theorem schreierRankTransformCardinal_eq_self_of_aleph0_le

45 {κ : Cardinal} (hκ : Cardinal.aleph0 ≤ κ) (n : ℕ) :

46 schreierRankTransformCardinal κ n = κ := by

47 simp only [schreierRankTransformCardinal, not_lt.mpr hκ, ↓reduceDIte]

49/--

50For a finite input cardinal, the Schreier rank-transform cardinal is the corresponding finite

51Schreier value.

52-/

53@[simp 900] theorem schreierRankTransformCardinal_mk_finite (X : Type u) [Finite X] (n : ℕ) :

54 schreierRankTransformCardinal (Cardinal.mk X) n =

55 (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) n : Cardinal) := by

56 classical

57 letI : Fintype X := Fintype.ofFinite X

58 simp only [Cardinal.mk_fintype, schreierRankTransformCardinal_natCast, Nat.card_eq_fintype_card]

60/--

61For an infinite input cardinal, the finite-index Schreier rank transform is the same infinite

62cardinal.

63-/

64@[simp 900] theorem schreierRankTransformCardinal_mk_infinite (X : Type u) [Infinite X] (n : ℕ) :

65 schreierRankTransformCardinal (Cardinal.mk X) n = Cardinal.mk X :=

66 schreierRankTransformCardinal_eq_self_of_aleph0_le (Cardinal.aleph0_le_mk X) n

69/--

70An open subgroup of a finitely generated profinite group satisfies the usual Schreier bound on

71the minimal number of topological generators.

72-/

73theorem topologicalRank_openSubgroup_le_rankTransform_of_topologicalRank_eq_nat

74 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

75 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

76 {d : ℕ} (hd : Generation.topologicalRank G = d)

77 (U : OpenSubgroup G) :

78 Generation.topologicalRank ↥(U : Subgroup G) ≤

79 (_root_.ReidemeisterSchreier.Schreier.rankTransform d (Nat.card (G ⧸ (U : Subgroup G))) :

80 Cardinal) := by

81 classical

82 cases d with

83 | zero =>

84 rcases

85 topologicallyGeneratedByAtMost_of_topologicalRank_eq_nat

86 (G := G) hd with ⟨s, hs, hsgen⟩

87 have hs0 : s.card = 0 := Nat.eq_zero_of_le_zero hs

88 have hsempty : s = ∅ := Finset.card_eq_zero.mp hs0

89 have hgenEmpty : Generation.TopologicallyGenerates (G := G) (∅ : Set G) := by

90 simpa [hsempty] using hsgen

91 have hdenseOne : Dense ({1} : Set G) := by

92 have hdenseBot :

93 Dense (((Subgroup.closure (∅ : Set G)) : Subgroup G) : Set G) :=

94 (Generation.topologicallyGenerates_iff_dense (G := G) (X := (∅ : Set G))).1

95 hgenEmpty

96 simpa using hdenseBot

97 have hsingleton :

98 ({1} : Set G) = (Set.univ : Set G) := by

99 exact (closure_eq_iff_isClosed.mpr isClosed_singleton).symm.trans hdenseOne.closure_eq

100 haveI : Subsingleton G := ⟨fun x y => by

101 have hx : x = 1 := by

102 have hxmem : x ∈ ({1} : Set G) := by

103 simp only [hsingleton, mem_univ]

104 simpa using hxmem

105 have hy : y = 1 := by

106 have hymem : y ∈ ({1} : Set G) := by

107 simp only [hsingleton, mem_univ]

108 simpa using hymem

109 rw [hx, hy]⟩

110 have hbot_top : (⊥ : Subgroup ↥(U : Subgroup G)) = ⊤ := by

111 ext x

112 constructor

113 · intro _

114 trivial

115 · intro _

116 exact Subsingleton.elim _ _

117 have hgenEmptyU :

118 Generation.TopologicallyGenerates (G := ↥(U : Subgroup G))

119 (∅ : Set ↥(U : Subgroup G)) := by

120 rw [Generation.TopologicallyGenerates]

121 have htopClosure : (⊤ : Subgroup ↥(U : Subgroup G)).topologicalClosure = ⊤ :=

122 top_unique (Subgroup.le_topologicalClosure _)

123 simpa [hbot_top] using htopClosure

124 have hbound : Generation.topologicalRank ↥(U : Subgroup G) ≤ (0 : Cardinal) := by

125 simpa only [Cardinal.mk_eq_zero] using

126 (Generation.topologicalRank_le_mk_of_topologicallyGenerates

127 (G := ↥(U : Subgroup G)) hgenEmptyU)

128 simpa using hbound

129 | succ n =>

130 have hgenAtMost :

131 TopologicallyGeneratedByAtMost (G := G) (n + 1) :=

132 topologicallyGeneratedByAtMost_of_topologicalRank_eq_nat

133 (G := G) hd

134 have hfg_iff :

135 TopologicallyFinitelyGenerated G ↔

136 ∃ m, TopologicallyGeneratedByAtMost (G := G) m :=

137 by

138 simpa using

139 (topologicallyFinitelyGenerated_iff_exists_topologicallyGeneratedByAtMost

140 (G := G))

141 have hfg : TopologicallyFinitelyGenerated G := by

142 exact hfg_iff.2 ⟨n + 1, hgenAtMost⟩

143 have hdle : Generation.topologicalRank G ≤ ((n + 1 : ℕ) : Cardinal) := by

144 rw [hd]

145 obtain ⟨g, hg⟩ :=

146 exists_generatingTuple_of_topologicalRank_le_of_finite

147 (G := G) (n := n + 1) hfg hdle

148 let φ : FreeGroup (Fin (n + 1)) →* G := FreeGroup.lift g

149 let D : Subgroup G := φ.range

150 have hg_subset : Set.range g ⊆ (D : Set G) := by

151 rintro _ ⟨i, rfl⟩

152 exact ⟨FreeGroup.of i, by simp only [FreeGroup.lift_apply_of, φ]⟩

153 have hDgen : Generation.TopologicallyGenerates (G := G) (D : Set G) :=

154 ProCGroups.Generation.topologicallyGenerates_mono (G := G) hg hg_subset

155 have hDdenseClosure :

156 Dense (((Subgroup.closure (D : Set G)) : Subgroup G) : Set G) :=

157 (Generation.topologicallyGenerates_iff_dense (G := G) (X := (D : Set G))).1 hDgen

158 have hD_dense : Dense ((D : Set G)) := by

159 simpa [Subgroup.closure_eq D] using hDdenseClosure

160 let I : Subgroup G := (U : Subgroup G) ⊓ D

161 have hIU_dense : Dense ((I.subgroupOf (U : Subgroup G)) : Set ↥(U : Subgroup G)) := by

162 rw [Subtype.dense_iff]

163 have himage :

164 ((↑) : ↥(U : Subgroup G) → G) '' ((I.subgroupOf (U : Subgroup G)) :

165 Set ↥(U : Subgroup G)) =

166 ((U : Set G) ∩ (D : Set G)) := by

167 have hmap :

168 (((I.subgroupOf (U : Subgroup G)).map (U : Subgroup G).subtype : Subgroup G) :

169 Set G) =

170 ((U : Set G) ∩ (D : Set G)) := by

171 rw [Subgroup.map_subgroupOf_eq_of_le]

172 · rfl

173 · exact inf_le_left

174 exact

175 (Subgroup.coe_map (U : Subgroup G).subtype (I.subgroupOf (U : Subgroup G))).symm.trans

176 hmap

177 change (U : Set G) ⊆

178 closure (((↑) : ↥(U : Subgroup G) → G) '' ((I.subgroupOf (U : Subgroup G)) :

179 Set ↥(U : Subgroup G)))

180 rw [himage]

181 change ((U : Subgroup G) : Set G) ⊆

182 closure (((U : Subgroup G) : Set G) ∩ (D : Set G))

183 exact hD_dense.open_subset_closure_inter U.isOpen'

184 let L : Subgroup (FreeGroup (Fin (n + 1))) := Subgroup.comap φ (U : Subgroup G)

185 letI : Finite (G ⧸ (U : Subgroup G)) := ProCGroups.openSubgroup_finiteQuotient (G := G) U

186 have hDindex :

187 (U : Subgroup G).relIndex D = (U : Subgroup G).index := by

188 change ((U : Subgroup G).subgroupOf D).index = (U : Subgroup G).index

189 have key :

190 ∀ x y : D,

191 QuotientGroup.leftRel ((U : Subgroup G).subgroupOf D) x y ↔

192 QuotientGroup.leftRel (U : Subgroup G) x y := by

193 intro x y

194 simp only [QuotientGroup.leftRel_apply, Subgroup.mem_subgroupOf, Subgroup.coe_mul,

195 InvMemClass.coe_inv,

196 OpenSubgroup.mem_toSubgroup]

197 refine Nat.card_congr <|

198 Equiv.ofBijective

199 (Quotient.map' ((↑) : D → G) fun x y => (key x y).mp) ⟨?_, ?_⟩

200 · intro a b hab

201 revert hab

202 refine Quotient.inductionOn₂' a b ?_

203 intro x y hab

204 have hxy : QuotientGroup.leftRel (U : Subgroup G) x y := by

205 rw [Quotient.map'_mk'', Quotient.map'_mk''] at hab

206 exact Quotient.exact' hab

207 exact Quotient.sound' ((key x y).mpr hxy)

208 · refine Quotient.ind' fun x => ?_

209 let V : Set G := x • ((U : Subgroup G) : Set G)

210 have hVopen : IsOpen V := by

211 change IsOpen (x • ((U : Subgroup G) : Set G))

212 exact U.isOpen'.smul x

213 have hVnonempty : V.Nonempty := by

214 refine ⟨x, ?_⟩

215 simpa [V] using mem_leftCoset x (show (1 : G) ∈ (U : Subgroup G) from U.one_mem)

216 rcases hD_dense.exists_mem_open hVopen hVnonempty with ⟨y, hyD, hyV⟩

217 refine ⟨(⟨y, hyD⟩ : D), ?_⟩

218 change QuotientGroup.mk y = QuotientGroup.mk x

219 apply QuotientGroup.eq.2

220 simpa [mul_inv_rev, inv_inv] using

221 (U : Subgroup G).inv_mem ((mem_leftCoset_iff x).1 (by simpa [V] using hyV))

222 have hLindex : L.index = (U : Subgroup G).index := by

223 calc

224 L.index = (U : Subgroup G).relIndex D := by

225 simpa [L, D] using (Subgroup.index_comap (H := (U : Subgroup G)) (f := φ))

226 _ = (U : Subgroup G).index := hDindex

227 have hLindex_ne_zero : L.index ≠ 0 := by

228 rw [hLindex]

229 exact Subgroup.index_ne_zero_of_finite (H := (U : Subgroup G))

230 haveI : Finite (FreeGroup (Fin (n + 1)) ⧸ L) :=

231 (Subgroup.index_ne_zero_iff_finite (H := L)).1 hLindex_ne_zero

232 obtain ⟨Y, ⟨eL⟩, hYcard⟩ :=

233 exists_freeBasis_subgroupOfFreeGroup_of_rankTransform

234 (X := Fin (n + 1)) (L := L)

235 have hquotCard :

236 Nat.card (FreeGroup (Fin (n + 1)) ⧸ L) = Nat.card (G ⧸ (U : Subgroup G)) := by

237 rw [← Subgroup.index_eq_card (H := L), hLindex, Subgroup.index_eq_card]

238 have hYcard' :

239 Nat.card Y = _root_.ReidemeisterSchreier.Schreier.rankTransform (n + 1) (Nat.card (G ⧸

240 (U : Subgroup G))) := by

241 simpa [hquotCard] using hYcard

242 have hYnonzero : Nat.card Y ≠ 0 := by

243 rw [hYcard', _root_.ReidemeisterSchreier.Schreier.rankTransform_succ]

244 simp only [Nat.add_comm, ne_eq, Nat.add_eq_zero_iff, mul_eq_zero, one_ne_zero,

245 and_false, not_false_eq_true]

246 haveI : Finite Y := Nat.finite_of_card_ne_zero hYnonzero

247 letI : Fintype Y := Fintype.ofFinite Y

248 let φU : L →* ↥(U : Subgroup G) := {

249 toFun := fun x => ⟨φ x.1, x.2⟩

250 map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one, φ]

251 map_mul' := by

252 intro a b

253 ext

254 simp only [Subgroup.coe_mul, map_mul, φ]}

255 let κ : Y → ↥(U : Subgroup G) := fun y => φU (eL y)

256 have hLtop :

257 Subgroup.closure (Set.range fun y : Y => eL y) = ⊤ := by

258 have hset :

259 Set.range (fun y : Y => eL y) =

260 eL.repr.symm.toMonoidHom '' Set.range (FreeGroup.of : Y → FreeGroup Y) := by

261 ext z

262 constructor

263 · rintro ⟨y, rfl⟩

264 exact ⟨FreeGroup.of y, ⟨y, rfl⟩, by rfl⟩

265 · rintro ⟨x, hx, rfl⟩

266 rcases hx with ⟨y, rfl⟩

267 exact ⟨y, rfl⟩

268 calc

269 Subgroup.closure (Set.range fun y : Y => eL y)

270 =

271 Subgroup.closure

272 (eL.repr.symm.toMonoidHom '' Set.range (FreeGroup.of : Y → FreeGroup Y)) := by

273 rw [hset]

274 _ = ⊤ := by

275 rw [← MonoidHom.map_closure, FreeGroup.closure_range_of]

276 exact Subgroup.map_top_of_surjective

277 eL.repr.symm.toMonoidHom eL.repr.symm.surjective

278 have hφU_range : φU.range = I.subgroupOf (U : Subgroup G) := by

279 ext u

280 constructor

281 · rintro ⟨x, rfl⟩

282 change φ x.1 ∈ I

283 exact ⟨x.2, ⟨x.1, rfl⟩⟩

284 · intro hu

285 change (u : G) ∈ I at hu

286 rcases hu with ⟨huU, huD⟩

287 rcases huD with ⟨x, hx⟩

288 refine ⟨⟨x, ?_⟩, ?_⟩

289 · change φ x ∈ (U : Subgroup G)

290 exact hx.symm ▸ huU

291 · apply Subtype.ext

292 simp only [MonoidHom.coe_mk, OneHom.coe_mk, hx, Subtype.coe_eta, φU]

293 have hφU_dense :

294 Dense ((φU.range : Subgroup ↥(U : Subgroup G)) : Set ↥(U : Subgroup G)) := by

295 rw [hφU_range]

296 exact hIU_dense

297 have hκclosure :

298 Subgroup.closure (Set.range κ) = φU.range := by

299 have hmap :

300 (Subgroup.closure (Set.range fun y : Y => eL y)).map φU =

301 Subgroup.closure (φU '' Set.range (fun y : Y => eL y)) := by

302 simpa using

303 (MonoidHom.map_closure φU (Set.range fun y : Y => eL y))

304 have himage :

305 φU '' Set.range (fun y : Y => eL y) = Set.range κ := by

306 ext u

307 constructor

308 · rintro ⟨x, ⟨y, rfl⟩, rfl⟩

309 exact ⟨y, rfl⟩

310 · rintro ⟨y, rfl⟩

311 exact ⟨eL y, ⟨y, rfl⟩, rfl⟩

312 calc

313 Subgroup.closure (Set.range κ)

314 = Subgroup.closure (φU '' Set.range (fun y : Y => eL y)) := by

315 rw [← himage]

316 _ = (Subgroup.closure (Set.range fun y : Y => eL y)).map φU := by

317 symm

318 exact hmap

319 _ = (⊤ : Subgroup L).map φU := by rw [hLtop]

320 _ = φU.range := by rw [← MonoidHom.range_eq_map]

321 have hκgen :

322 Generation.TopologicallyGenerates (G := ↥(U : Subgroup G)) (Set.range κ) := by

323 exact (Generation.topologicallyGenerates_iff_dense

324 (G := ↥(U : Subgroup G)) (X := Set.range κ)).2 <|

325 by simpa [hκclosure] using hφU_dense

326 let s : Finset ↥(U : Subgroup G) := Finset.univ.image κ

327 have hs_card : s.card ≤ Nat.card Y := by

328 simpa [s, Nat.card_eq_fintype_card] using

329 (Finset.card_image_le (s := (Finset.univ : Finset Y)) (f := κ))

330 have hs_gen :

331 Generation.TopologicallyGenerates (G := ↥(U : Subgroup G))

332 (↑s : Set ↥(U : Subgroup G)) := by

333 simpa [s, Finset.coe_image] using hκgen

334 have hdU_nat : Generation.topologicalRank ↥(U : Subgroup G) ≤ Nat.card Y := by

335 exact topologicalRank_le_of_topologicallyGeneratedByAtMost

336 (G := ↥(U : Subgroup G)) ⟨s, hs_card, hs_gen⟩

337 calc

338 Generation.topologicalRank ↥(U : Subgroup G) ≤ (Nat.card Y : Cardinal) := by

339 exact hdU_nat

340 _ = (_root_.ReidemeisterSchreier.Schreier.rankTransform (n + 1) (Nat.card (G ⧸ (U :

341 Subgroup G))) : Cardinal) := by

342 exact_mod_cast hYcard'

343

344end Profinite

345end ReidemeisterSchreier