Source: ProCGroups.FiniteGeneration.Basic

1import Mathlib.GroupTheory.FreeGroup.Basic

2import ProCGroups.Generation.QuotientGeneratorConvergingPairs

4/-!

5# Basic results on topological finite generation

7This module defines topological finite generation and topologically characteristic subgroups,

8then relates finite generating sets to free-group maps and generator-converging families.

9-/

11open Set

12open scoped Topology Pointwise

14namespace ProCGroups.FiniteGeneration

16universe u v w

18open ProCGroups.Generation

20section Basic

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

24/-- Finitely generated as a topological group. -/

25def TopologicallyFinitelyGenerated

26 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop :=

27 ∃ s : Finset G, TopologicallyGenerates (G := G) (↑s : Set G)

29/-- A subgroup is topologically characteristic if every continuous automorphism preserves it. -/

30def IsTopologicallyCharacteristic

31 (G : Type u) [Group G] [TopologicalSpace G] (H : Subgroup G) : Prop :=

32 ∀ φ : G ≃ₜ* G, ∀ g : G, φ g ∈ H ↔ g ∈ H

34section Characteristic

36omit [IsTopologicalGroup G]

38/--

39Membership in a topologically characteristic subgroup is invariant under applying a continuous

40automorphism.

41-/

42theorem IsTopologicallyCharacteristic.apply_mem_iff {H : Subgroup G}

43 (hH : IsTopologicallyCharacteristic (G := G) H) (φ : G ≃ₜ* G) {g : G} :

44 φ g ∈ H ↔ g ∈ H :=

45 hH φ g

47/-- Intersections of topologically characteristic subgroups are topologically characteristic. -/

48theorem IsTopologicallyCharacteristic.inf {H K : Subgroup G}

49 (hH : IsTopologicallyCharacteristic (G := G) H) (hK : IsTopologicallyCharacteristic (G := G)

50 K) :

51 IsTopologicallyCharacteristic (G := G) (H ⊓ K) := by

52 intro φ g

53 simp only [Subgroup.mem_inf, hH φ g, hK φ g]

55/-- Arbitrary infima of topologically characteristic subgroups are topologically characteristic. -/

56theorem IsTopologicallyCharacteristic.sInf {S : Set (Subgroup G)}

57 (hS : ∀ H ∈ S, IsTopologicallyCharacteristic (G := G) H) :

58 IsTopologicallyCharacteristic (G := G) (sInf S) := by

59 intro φ g

60 simp only [Subgroup.mem_sInf]

61 constructor

62 · intro hg H hH

63 exact (hS H hH φ g).1 (hg H hH)

64 · intro hg H hH

65 exact (hS H hH φ g).2 (hg H hH)

67/-- Indexed infima of topologically characteristic subgroups are topologically characteristic. -/

68theorem IsTopologicallyCharacteristic.iInf {ι : Sort*} {S : ι → Subgroup G}

69 (hS : ∀ i, IsTopologicallyCharacteristic (G := G) (S i)) :

70 IsTopologicallyCharacteristic (G := G) (iInf S) := by

71 intro φ g

72 simp only [Subgroup.mem_iInf]

73 constructor

74 · intro hg i

75 exact (hS i φ g).1 (hg i)

76 · intro hg i

77 exact (hS i φ g).2 (hg i)

79/--

80The top subgroup is topologically characteristic, since every continuous automorphism preserves

81it.

82-/

83@[simp] theorem IsTopologicallyCharacteristic.top :

84 IsTopologicallyCharacteristic (G := G) (⊤ : Subgroup G) := by

85 intro φ g

86 simp only [Subgroup.mem_top]

88end Characteristic

90/-- \(G\) can be topologically generated by at most \(n\) elements. -/

91def TopologicallyGeneratedByAtMost

92 (n : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :

93 Prop :=

94 ∃ s : Finset G, s.card ≤ n ∧ TopologicallyGenerates (G := G) (↑s : Set G)

96/-- Increasing the allowed number of generators preserves bounded topological generation. -/

97theorem TopologicallyGeneratedByAtMost.mono {m n : ℕ}

98 (hmn : m ≤ n)

99 (hG : TopologicallyGeneratedByAtMost (G := G) m) :

100 TopologicallyGeneratedByAtMost (G := G) n := by

101 rcases hG with ⟨s, hs, hgen⟩

102 exact ⟨s, hs.trans hmn, hgen⟩

103

104/--

105A group is topologically finitely generated if and only if it is generated by at most \(n\)

106elements for some natural number \(n\).

107-/

108theorem topologicallyFinitelyGenerated_iff_exists_topologicallyGeneratedByAtMost :

109 TopologicallyFinitelyGenerated G ↔

110 ∃ n, TopologicallyGeneratedByAtMost (G := G) n := by

111 constructor

112 · rintro ⟨s, hs⟩

113 exact ⟨s.card, s, le_rfl, hs⟩

114 · rintro ⟨_n, s, _hs, hgen⟩

115 exact ⟨s, hgen⟩

116

117omit [IsTopologicalGroup G] in

118/-- A finite set of elements converges to \(1\) in the profinite generating-family sense. -/

119theorem finiteSet_convergesToOneAlongOpenSubgroups (s : Finset G) :

120 ConvergesToOneAlongOpenSubgroups (G := G) (↑s : Set G) :=

121 ConvergesToOneAlongOpenSubgroups.of_finite s.finite_toSet

122

123/--

124If \(G\) is topologically generated by at most \(n\) elements, its topological rank is at most

125\(n\).

126-/

127theorem topologicalRank_le_of_topologicallyGeneratedByAtMost {n : ℕ}

128 (h : TopologicallyGeneratedByAtMost (G := G) n) :

129 topologicalRank G ≤ n := by

130 rcases h with ⟨s, hs, hgen⟩

131 have hconv : ConvergesToOneAlongOpenSubgroups (G := G) (↑s : Set G) :=

132 finiteSet_convergesToOneAlongOpenSubgroups (G := G) s

133 calc

134 topologicalRank G ≤ Cardinal.mk (↑s : Set G) :=

135 topologicalRank_le_mk_of_generatesAndConvergesToOneAlongOpenSubgroups (G := G) ⟨hgen, hconv⟩

136 _ = (s.card : Cardinal) := by

137 exact Cardinal.mk_coe_finset (s := s)

138 _ ≤ n := by

139 exact_mod_cast hs

140

141/--

142The image of a topological generating family under a continuous surjective homomorphism

143topologically generates the codomain.

144-/

145theorem topologicallyGenerates_range_comp_of_surjective

146 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

147 (φ : G →ₜ* H) (hφ : Function.Surjective φ)

148 {ι : Sort w} (g : ι → G)

149 (hg : TopologicallyGenerates (G := G) (Set.range g)) :

150 TopologicallyGenerates (G := H) (Set.range (φ ∘ g)) := by

151 simpa [Set.range_comp, Function.comp] using

152 topologicallyGenerates_image_of_continuousMonoidHom_surjective

153 (G := G) (H := H) φ hφ hg

154

155/-- Bounded topological generation descends along continuous surjective homomorphisms. -/

156theorem TopologicallyGeneratedByAtMost.of_surjective

157 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

158 (φ : G →ₜ* H) (hφ : Function.Surjective φ) {n : ℕ}

159 (hG : TopologicallyGeneratedByAtMost (G := G) n) :

160 TopologicallyGeneratedByAtMost (G := H) n := by

161 classical

162 rcases hG with ⟨s, hs, hgen⟩

163 refine ⟨s.image φ, (Finset.card_image_le).trans hs, ?_⟩

164 simpa [Finset.coe_image] using

165 topologicallyGenerates_image_of_continuousMonoidHom_surjective

166 (G := G) (H := H) φ hφ hgen

167

168/-- Topological finite generation descends along continuous surjective homomorphisms. -/

169theorem topologicallyFinitelyGenerated_of_continuousSurjective

170 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

171 (φ : G →ₜ* H) (hφ : Function.Surjective φ)

172 (hG : TopologicallyFinitelyGenerated G) :

173 TopologicallyFinitelyGenerated H := by

174 rw [topologicallyFinitelyGenerated_iff_exists_topologicallyGeneratedByAtMost] at hG ⊢

175 rcases hG with ⟨n, hn⟩

176 exact ⟨n, TopologicallyGeneratedByAtMost.of_surjective (G := G) (H := H) φ hφ hn⟩

177

178/-- In the discrete case, topological generation is abstract subgroup generation. -/

179theorem topologicallyGenerates_iff_subgroupClosure_eq_top_of_discrete

180 [DiscreteTopology G] {X : Set G} :

181 TopologicallyGenerates (G := G) X ↔ Subgroup.closure X = ⊤ := by

182 have htc : (Subgroup.closure X).topologicalClosure = Subgroup.closure X := by

183 apply SetLike.ext'

184 rw [Subgroup.topologicalClosure_coe]

185 exact closure_discrete ((Subgroup.closure X : Subgroup G) : Set G)

186 rw [TopologicallyGenerates, htc]

187

188/--

189A map from a free group to a discrete group is surjective when the images of the chosen

190generators topologically generate the target; in the discrete topology this is exactly abstract

191generation.

192-/

193theorem freeGroup_lift_surjective_of_topologicallyGenerates_discrete

194 {X : Type v} [DiscreteTopology G] (g : X → G)

195 (hg : TopologicallyGenerates (G := G) (Set.range g)) :

196 Function.Surjective (FreeGroup.lift g) := by

197 rw [topologicallyGenerates_iff_subgroupClosure_eq_top_of_discrete] at hg

198 have hclosure_le_range :

199 Subgroup.closure (Set.range g) ≤ (FreeGroup.lift g).range := by

200 refine (Subgroup.closure_le (K := (FreeGroup.lift g).range)).2 ?_

201 rintro y ⟨x, rfl⟩

202 exact ⟨FreeGroup.of x, by simp only [FreeGroup.lift_apply_of]⟩

203 intro y

204 have hy : y ∈ Subgroup.closure (Set.range g) := by

205 rw [hg]

206 trivial

207 exact hclosure_le_range hy

208

209/-- A finite discrete group is topologically finitely generated. -/

210theorem topologicallyFinitelyGenerated_of_finite [Finite G] [DiscreteTopology G] :

211 TopologicallyFinitelyGenerated G := by

212 classical

213 letI : Fintype G := Fintype.ofFinite G

214 refine ⟨Finset.univ, ?_⟩

215 rw [topologicallyGenerates_iff_subgroupClosure_eq_top_of_discrete]

216 simp only [Finset.coe_univ, Subgroup.closure_univ]

217

218/--

219If the topological rank of a profinite group is the natural number \(n\), then the group is

220topologically generated by at most \(n\) elements.

221-/

222theorem topologicallyGeneratedByAtMost_of_topologicalRank_eq_nat

223 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] {n : ℕ}

224 (hd : topologicalRank G = n) :

225 TopologicallyGeneratedByAtMost (G := G) n := by

226 classical

227 rcases exists_topologicallyGenerates_card_eq_topologicalRank (G := G) with

228 ⟨X, hX, hXcard⟩

229 have hXlt : Cardinal.mk X < Cardinal.aleph0 := by

230 calc

231 Cardinal.mk X = topologicalRank G := hXcard

232 _ = n := hd

233 _ < Cardinal.aleph0 := Cardinal.natCast_lt_aleph0 (n := n)

234 letI : Finite X := (Cardinal.lt_aleph0_iff_finite (α := X)).mp hXlt

235 have hXfin : X.Finite := Set.toFinite X

236 let s : Finset G := hXfin.toFinset

237 have hs_card : s.card = n := by

238 have hs_mk : (s.card : Cardinal) = Cardinal.mk X := by

239 simpa [s] using (Cardinal.mk_coe_finset (s := hXfin.toFinset)).symm

240 exact_mod_cast (hs_mk.trans (hXcard.trans hd))

241 refine ⟨s, hs_card.le, ?_⟩

242 simpa [s] using hX

243

244/--

245A finite upper bound on the topological rank gives an explicit generating tuple of that length.

246-/

247theorem exists_generatingTuple_of_topologicalRank_le_of_finite

248 (hG : TopologicallyFinitelyGenerated G) {n : ℕ} (hd : topologicalRank G ≤ n) :

249 ∃ g : Fin n → G, TopologicallyGenerates (G := G) (Set.range g) := by

250 classical

251 have hdfin : topologicalRank G < Cardinal.aleph0 := by

252 rcases hG with ⟨s, hs⟩

253 have hconv : ConvergesToOneAlongOpenSubgroups (G := G) (↑s : Set G) :=

254 finiteSet_convergesToOneAlongOpenSubgroups (G := G) s

255 have hdle : topologicalRank G ≤ Cardinal.mk (↑s : Set G) :=

256 topologicalRank_le_mk_of_generatesAndConvergesToOneAlongOpenSubgroups (G := G) ⟨hs, hconv⟩

257 exact hdle.trans_lt <| by

258 have hsMk : Cardinal.mk (↑s : Set G) = (s.card : Cardinal) :=

259 Cardinal.mk_coe_finset (s := s)

260 rw [hsMk]

261 exact Cardinal.natCast_lt_aleph0 (n := s.card)

262 let m := Cardinal.toNat (topologicalRank G)

263 have hm : topologicalRank G = m := by

264 symm

265 exact Cardinal.cast_toNat_of_lt_aleph0 hdfin

266 rcases exists_topologicallyGenerates_card_eq_topologicalRank (G := G) with

267 ⟨X, hX, hXcard⟩

268 have hXfin : X.Finite := by

269 have hXlt : Cardinal.mk X < Cardinal.aleph0 := by

270 calc

271 Cardinal.mk X = topologicalRank G := hXcard

272 _ = m := hm

273 _ < Cardinal.aleph0 := Cardinal.natCast_lt_aleph0 (n := m)

274 letI : Finite X := (Cardinal.lt_aleph0_iff_finite (α := X)).mp <| by

275 simpa using hXlt

276 exact Set.toFinite X

277 let s : Finset G := hXfin.toFinset

278 have hs_gen : TopologicallyGenerates (G := G) (↑s : Set G) := by

279 simpa [s] using hX

280 have hs_card : s.card = m := by

281 have hs_mk : (s.card : Cardinal) = Cardinal.mk X := by

282 simpa [s] using (Cardinal.mk_coe_finset (s := hXfin.toFinset)).symm

283 exact_mod_cast (hs_mk.trans (hXcard.trans hm))

284 have hmle : m ≤ n := by

285 simpa [m] using

286 (Cardinal.toNat_le_toNat hd (Cardinal.natCast_lt_aleph0 (n := n)))

287 have hs_le : s.card ≤ n := by

288 simpa [hs_card] using hmle

289 let e : Fin s.card ≃ s := by

290 simpa using (Fintype.equivFin s).symm

291 let g0 : Fin s.card → G := fun i => (e i : G)

292 have hs_subset_range : (↑s : Set G) ⊆ Set.range g0 := by

293 intro x hx

294 refine ⟨e.symm ⟨x, hx⟩, ?_⟩

295 simp only [Equiv.apply_symm_apply, g0]

296 have hg0 : TopologicallyGenerates (G := G) (Set.range g0) :=

297 topologicallyGenerates_mono hs_gen hs_subset_range

298 let g : Fin n → G := fun i =>

299 if hi : i.1 < s.card then g0 ⟨i.1, hi⟩ else 1

300 have hg0_subset : Set.range g0 ⊆ Set.range g := by

301 intro x hx

302 rcases hx with ⟨i, rfl⟩

303 refine ⟨Fin.castLE hs_le i, ?_⟩

304 have hi : (Fin.castLE hs_le i).1 < s.card := i.2

305 simp only [Fin.val_castLE, Fin.is_lt, ↓reduceDIte, Fin.eta, g]

306 exact ⟨g, topologicallyGenerates_mono hg0 hg0_subset⟩

307

308end Basic

309

310

311/--

312If every finite stage of a surjective inverse system has topological rank at most \(n\), then so

313does the inverse limit.

314-/

315theorem topologicalRank_inverseLimit_le_of_componentBound

316 {I : Type v} [Preorder I]

317 (S : ProCGroups.InverseSystems.InverseSystem (I := I))

318 [Nonempty I] [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]

319 [∀ i, IsTopologicalGroup (S.X i)] [∀ i, Finite (S.X i)]

320 [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]

321 (hdir : Directed (· ≤ ·) (id : I → I))

322 (hsurj : ∀ {i j : I} (hij : i ≤ j), Function.Surjective (S.map hij))

323 {n : ℕ} (hbound : ∀ i, topologicalRank (S.X i) ≤ n) :

324 topologicalRank S.inverseLimit ≤ n := by

325 classical

326 letI : ∀ i, DiscreteTopology (S.X i) := fun _ => by infer_instance

327 let T : ProCGroups.InverseSystems.InverseSystem (I := I) := {

328 X := fun i => { g : Fin n → S.X i // TopologicallyGenerates (G := S.X i) (Set.range g) }

329 topologicalSpace := fun _ => inferInstance

330 map := fun {i j} hij g =>

331 ⟨fun a => S.map hij (g.1 a), by

332 let φij : ContinuousMonoidHom (S.X j) (S.X i) :=

333 { toMonoidHom :=

334 { toFun := S.map hij

335 map_one' := ProCGroups.InverseSystems.IsGroupSystem.map_one (S := S) hij

336 map_mul' := ProCGroups.InverseSystems.IsGroupSystem.map_mul (S := S) hij }

337 continuous_toFun := S.continuous_map hij }

338 have hgen :=

339 topologicallyGenerates_range_comp_of_surjective

340 (G := S.X j) (H := S.X i) φij (hsurj hij) g.1 g.2

341 change TopologicallyGenerates (G := S.X i)

342 (Set.range (fun a => S.map hij (g.1 a))) at hgen

343 exact hgen⟩

344 continuous_map := fun {_i _j} _hij => by

345 exact continuous_of_discreteTopology

346 map_id := fun i => by

347 ext g a

348 simp only [InverseSystems.InverseSystem.map_id_apply, id_eq]

349 map_comp := fun hij hjk => by

350 ext g a

351 simp only [Function.comp_apply, InverseSystems.InverseSystem.map_comp_apply]}

352 have hTnonempty : ∀ i, Nonempty (T.X i) := by

353 intro i

354 have hfg : TopologicallyFinitelyGenerated (S.X i) :=

355 topologicallyFinitelyGenerated_of_finite (G := S.X i)

356 rcases exists_generatingTuple_of_topologicalRank_le_of_finite

357 (G := S.X i) hfg (hbound i) with ⟨g, hg⟩

358 exact ⟨⟨g, hg⟩⟩

359 letI : ∀ i, Nonempty (T.X i) := hTnonempty

360 letI : ∀ i, Finite (T.X i) := fun _ => inferInstance

361 rcases ProCGroups.InverseSystems.InverseSystem.nonempty_inverseLimit_of_finite

362 (S := T) hdir with ⟨x⟩

363 let g : Fin n → S.inverseLimit := fun a =>

364 ⟨fun i => (x.1 i).1 a, by

365 intro i j hij

366 have hcompat := congrArg Subtype.val (x.2 i j hij)

367 exact congrArg (fun f => f a) hcompat⟩

368 have hgproj : ∀ i, TopologicallyGenerates (G := S.X i) (S.projection i '' Set.range g) := by

369 intro i

370 rw [← Set.range_comp (S.projection i) g]

371 have hfun : S.projection i ∘ g = (x.1 i).1 := by

372 funext a

373 rfl

374 rw [hfun]

375 exact (x.1 i).2

376 have hggen : TopologicallyGenerates (G := S.inverseLimit) (Set.range g) := by

377 exact

378 (topologicallyGenerates_iff_forall_projection_inverseLimit

379 (S := S) hdir hsurj (X := Set.range g)).2 hgproj

380 let s : Finset S.inverseLimit := Finset.univ.image g

381 have hs_card : s.card ≤ n := by

382 simpa [s] using (Finset.card_image_le (f := g) (s := (Finset.univ : Finset (Fin n))))

383 have hsgen : TopologicallyGenerates (G := S.inverseLimit) (↑s : Set S.inverseLimit) := by

384 simpa [s, Finset.coe_image] using hggen

385 exact topologicalRank_le_of_topologicallyGeneratedByAtMost (G := S.inverseLimit)

386 ⟨s, hs_card, hsgen⟩

387

388

389end ProCGroups.FiniteGeneration