Source: ProCGroups.Generation.Basic
1import Mathlib.Topology.Algebra.ClopenNhdofOne
2import Mathlib.Topology.Algebra.ContinuousMonoidHom
3import Mathlib.Topology.Algebra.Nonarchimedean.Basic
5/-!
6# Topological generation and convergent generating sets
8This module defines topological generation, convergence to one, the corresponding cardinal
9ranks, and the finite word-product filtration of a set. It develops extensionality,
10closed-generated-subgroup, image, quotient, and continuous-equivalence lemmas that form the
11basic API for generator arguments in profinite groups.
12-/
14open Set
15open scoped Topology Pointwise
17namespace ProCGroups.Generation
19universe u v
21section
23variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
25/-- X topologically generates G if the abstract subgroup generated by X is dense in G. -/
26def TopologicallyGenerates (X : Set G) : Prop :=
27 (Subgroup.closure X).topologicalClosure = ⊤
29/-- A set converges to `1` when its subtype inclusion tends to `1` along the cofinite filter. -/
30def ConvergesToOne (X : Set G) : Prop :=
31 Filter.Tendsto (fun x : X => (x : G)) Filter.cofinite (𝓝 1)
33/-- The weaker condition obtained by testing convergence only against open subgroups.
35This agrees with `ConvergesToOne` for nonarchimedean groups, but is deliberately kept separate:
36on a general topological group, open subgroups need not form a neighborhood basis at `1`. -/
37def ConvergesToOneAlongOpenSubgroups (X : Set G) : Prop :=
38 ∀ U : OpenSubgroup G, (X \ (U : Set G)).Finite
40omit [IsTopologicalGroup G] in
41/-- A finite set converges to `1`. -/
42theorem ConvergesToOne.of_finite {X : Set G} (hX : X.Finite) :
43 ConvergesToOne (G := G) X := by
44 letI : Finite X := hX.to_subtype
45 simp [ConvergesToOne]
47omit [IsTopologicalGroup G] in
48/-- Every finite set satisfies the open-subgroup convergence condition. -/
49theorem ConvergesToOneAlongOpenSubgroups.of_finite {X : Set G} (hX : X.Finite) :
50 ConvergesToOneAlongOpenSubgroups (G := G) X := by
51 intro U
52 exact hX.subset (by
53 intro x hx
54 exact hx.1)
56omit [IsTopologicalGroup G] in
57/-- Genuine convergence implies convergence when tested only on open subgroups. -/
58theorem ConvergesToOne.to_alongOpenSubgroups {X : Set G}
59 (hX : ConvergesToOne (G := G) X) :
60 ConvergesToOneAlongOpenSubgroups (G := G) X := by
61 intro U
62 have hU : (U : Set G) ∈ 𝓝 (1 : G) :=
63 U.isOpen.mem_nhds U.one_mem
64 have heventually : ∀ᶠ x : X in Filter.cofinite, (x : G) ∈ U :=
65 hX.eventually hU
66 have hbad : {x : X | (x : G) ∉ U}.Finite := by
67 change {x : X | (x : G) ∈ U} ∈ Filter.cofinite at heventually
68 rw [Filter.mem_cofinite] at heventually
69 simpa only [Set.compl_setOf] using heventually
70 have hsubset :
71 X \ (U : Set G) ⊆
72 (fun x : X => (x : G)) '' {x : X | (x : G) ∉ U} := by
73 rintro x ⟨hxX, hxU⟩
74 exact ⟨⟨x, hxX⟩, hxU, rfl⟩
75 exact (hbad.image fun x : X => (x : G)).subset hsubset
77omit [IsTopologicalGroup G] in
78/-- In a nonarchimedean group, testing against open subgroups detects genuine convergence. -/
79theorem ConvergesToOneAlongOpenSubgroups.to_convergesToOne
80 [NonarchimedeanGroup G] {X : Set G}
81 (hX : ConvergesToOneAlongOpenSubgroups (G := G) X) :
82 ConvergesToOne (G := G) X := by
83 rw [ConvergesToOne, Filter.tendsto_def]
84 intro W hW
85 obtain ⟨U, hUW⟩ := NonarchimedeanGroup.is_nonarchimedean W hW
86 rw [Filter.mem_cofinite]
87 change {x : X | (x : G) ∉ W}.Finite
88 have hbadImage :
89 ((fun x : X => (x : G)) '' {x : X | (x : G) ∉ U}).Finite := by
90 exact (hX U).subset (by
91 rintro _ ⟨x, hxU, rfl⟩
92 exact ⟨x.property, hxU⟩)
93 have hbadU : {x : X | (x : G) ∉ U}.Finite := by
94 letI : Finite ((fun x : X => (x : G)) '' {x : X | (x : G) ∉ U}) :=
95 hbadImage.to_subtype
96 exact Finite.Set.finite_of_finite_image _ (by
97 intro a _ b _ hab
98 exact Subtype.ext hab)
99 exact hbadU.subset (by
100 intro x hxW hxU
101 exact hxW (hUW hxU))
103omit [IsTopologicalGroup G] in
104/-- For nonarchimedean groups, the genuine and open-subgroup convergence predicates agree. -/
105theorem convergesToOne_iff_alongOpenSubgroups [NonarchimedeanGroup G] {X : Set G} :
106 ConvergesToOne (G := G) X ↔
107 ConvergesToOneAlongOpenSubgroups (G := G) X :=
108 ⟨ConvergesToOne.to_alongOpenSubgroups,
109 ConvergesToOneAlongOpenSubgroups.to_convergesToOne⟩
111/-- A set which topologically generates and converges to `1` in the filter sense. -/
112def GeneratesAndConvergesToOne (X : Set G) : Prop :=
113 TopologicallyGenerates (G := G) X ∧ ConvergesToOne (G := G) X
115/-- A generating set satisfying only the weaker open-subgroup convergence condition. -/
116def GeneratesAndConvergesToOneAlongOpenSubgroups (X : Set G) : Prop :=
117 TopologicallyGenerates (G := G) X ∧
118 ConvergesToOneAlongOpenSubgroups (G := G) X
120/-- The least cardinality of a topological generating set.
122The candidate set is always nonempty: `Set.univ` topologically generates every group. Thus this
123definition never uses the accidental value `Cardinal.sInf ∅ = 0`. -/
124noncomputable def topologicalRank
125 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
126 Cardinal :=
127 sInf {κ : Cardinal |
128 ∃ X : Set G, TopologicallyGenerates (G := G) X ∧ Cardinal.mk X = κ}
130/-- The optional least size of a generating set which also converges to `1`.
132Unlike `topologicalRank`, the relevant family of cardinals can be empty, so absence is represented
133by `none` instead of being silently identified with cardinal zero. -/
134noncomputable def convergentGeneratorRank
135 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
136 Option Cardinal := by
137 classical
138 exact
139 if h : ∃ X : Set G, GeneratesAndConvergesToOne (G := G) X then
140 some (sInf {κ : Cardinal |
141 ∃ X : Set G, GeneratesAndConvergesToOne (G := G) X ∧ Cardinal.mk X = κ})
142 else
143 none
145/-- The topological rank is bounded by the cardinality of any topological generating set. -/
146theorem topologicalRank_le_mk_of_topologicallyGenerates {X : Set G}
147 (hX : TopologicallyGenerates (G := G) X) :
148 topologicalRank G ≤ Cardinal.mk X := by
149 change sInf {κ : Cardinal |
150 ∃ X : Set G, TopologicallyGenerates (G := G) X ∧ Cardinal.mk X = κ} ≤ Cardinal.mk X
151 exact csInf_le' ⟨X, hX, rfl⟩
153/-- In particular, an open-subgroup-convergent generating set bounds the topological rank. -/
154theorem topologicalRank_le_mk_of_generatesAndConvergesToOneAlongOpenSubgroups {X : Set G}
155 (hX : GeneratesAndConvergesToOneAlongOpenSubgroups (G := G) X) :
156 topologicalRank G ≤ Cardinal.mk X :=
157 topologicalRank_le_mk_of_topologicallyGenerates hX.1
159/-- There is a topological generating set whose cardinality is exactly the topological rank. -/
160theorem exists_topologicallyGenerates_card_eq_topologicalRank :
161 ∃ X : Set G, TopologicallyGenerates (G := G) X ∧
162 Cardinal.mk X = topologicalRank G := by
163 let C : Set Cardinal := {κ : Cardinal |
164 ∃ X : Set G, TopologicallyGenerates (G := G) X ∧ Cardinal.mk X = κ}
165 have hC : C.Nonempty := by
166 refine ⟨Cardinal.mk (Set.univ : Set G), Set.univ, ?_, rfl⟩
167 have hclosure : Subgroup.closure (Set.univ : Set G) = ⊤ := by
168 rw [eq_top_iff]
169 intro x _
170 exact Subgroup.subset_closure (Set.mem_univ x)
171 rw [TopologicallyGenerates, hclosure]
172 exact le_antisymm le_top (Subgroup.le_topologicalClosure _)
173 simpa [topologicalRank, C] using (csInf_mem hC)
175/-- A nontrivial T1 topological group has nonzero topological rank. -/
176theorem topologicalRank_ne_zero [T1Space G] [Nontrivial G] :
177 topologicalRank G ≠ 0 := by
178 intro hzero
179 obtain ⟨X, hX, hcard⟩ :=
180 exists_topologicallyGenerates_card_eq_topologicalRank (G := G)
181 letI : IsEmpty X := Cardinal.mk_eq_zero_iff.mp (hcard.trans hzero)
182 have hXempty : X = ∅ := by
183 ext x
184 constructor
185 · intro hx
186 exact isEmptyElim (⟨x, hx⟩ : X)
187 · simp
188 have hbotClosed : IsClosed (((⊥ : Subgroup G) : Set G)) := by
189 change IsClosed ({1} : Set G)
190 exact isClosed_singleton
191 have hclosureBot : (⊥ : Subgroup G).topologicalClosure = ⊥ :=
192 le_antisymm
193 (Subgroup.topologicalClosure_minimal _ le_rfl hbotClosed)
194 (Subgroup.le_topologicalClosure _)
195 have hclosureEmpty : Subgroup.closure (∅ : Set G) = ⊥ := by
196 apply le_antisymm
197 · exact (Subgroup.closure_le (K := ⊥)).2 (Set.empty_subset _)
198 · exact bot_le
199 have hbotTop : (⊥ : Subgroup G) = ⊤ := by
200 rw [TopologicallyGenerates, hXempty, hclosureEmpty, hclosureBot] at hX
201 exact hX
202 exact not_subsingleton_iff_nontrivial.mpr inferInstance
203 (subsingleton_iff_bot_eq_top.mp hbotTop)
205/--
206Iterated products of words in \(X\), with \(\mathrm{wordProducts}(X,0)=\{1\}\) and
207\(\mathrm{wordProducts}(X,n+1)=\mathrm{wordProducts}(X,n)\cdot X\).
208-/
209def wordProducts (X : Set G) : ℕ → Set G
210 | 0 => {1}
211 | n + 1 => wordProducts X n * X
213/-- Topological generation is equivalently density of the abstract subgroup generated by the set. -/
214theorem topologicallyGenerates_iff_dense {X : Set G} :
215 TopologicallyGenerates (G := G) X ↔ Dense ((Subgroup.closure X : Subgroup G) : Set G) := by
216 rw [TopologicallyGenerates, SetLike.ext'_iff, Subgroup.topologicalClosure_coe, Subgroup.coe_top,
217 dense_iff_closure_eq]
219/--
220Continuous homomorphisms out of a topologically generated group are determined by their values
221on the generating set.
222-/
223theorem continuousMonoidHom_ext_of_topologicallyGenerates
224 {R : Type v} [Group R] [TopologicalSpace R] [T2Space R]
225 {X : Set G} (hX : TopologicallyGenerates (G := G) X)
226 {f g : ContinuousMonoidHom G R} (hfg : ∀ x ∈ X, f x = g x) :
227 f = g := by
228 let K : Subgroup G := {
229 carrier := { x | f x = g x }
230 one_mem' := by simp only [mem_setOf_eq, map_one]
231 mul_mem' := by
232 intro a b ha hb
233 change f (a * b) = g (a * b)
234 rw [map_mul, map_mul, ha, hb]
235 inv_mem' := by
236 intro a ha
237 simpa using congrArg Inv.inv ha
238 }
239 have hKclosed : IsClosed ((K : Subgroup G) : Set G) := by
240 change IsClosed { x | f x = g x }
241 exact isClosed_eq f.continuous_toFun g.continuous_toFun
242 have hsub : Subgroup.closure X ≤ K := by
243 rw [Subgroup.closure_le]
244 intro x hx
245 exact hfg x hx
246 have htop : (⊤ : Subgroup G) ≤ K := by
247 have hcl : (Subgroup.closure X).topologicalClosure ≤ K :=
248 Subgroup.topologicalClosure_minimal _ hsub hKclosed
249 rw [TopologicallyGenerates] at hX
250 simpa [hX] using hcl
251 ext x
252 simpa [K] using htop (show x ∈ (⊤ : Subgroup G) from by simp only [Subgroup.mem_top])
254/-- The closed subgroup topologically generated by a set. -/
255def closedSubgroupGenerated (X : Set G) : ClosedSubgroup G where
256 toSubgroup := (Subgroup.closure X).topologicalClosure
257 isClosed' := Subgroup.isClosed_topologicalClosure _
259/-- The canonical map from an indexed family into the closed subgroup it topologically generates. -/
260def closedSubgroupGeneratedMap {A : Type v} (φ : A → G) :
261 A → (closedSubgroupGenerated (G := G) (Set.range φ) : Subgroup G) :=
262 fun a =>
263 ⟨φ a, Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨a, rfl⟩)⟩
265/-- The canonical indexed family topologically generates its closed generated subgroup. -/
266theorem closedSubgroupGeneratedMap_topologicallyGenerates {A : Type v} (φ : A → G) :
267 TopologicallyGenerates
268 (G := (closedSubgroupGenerated (G := G) (Set.range φ) : Subgroup G))
269 (Set.range (closedSubgroupGeneratedMap (G := G) φ)) := by
270 let K : ClosedSubgroup G := closedSubgroupGenerated (G := G) (Set.range φ)
271 let φK : A → (K : Subgroup G) := closedSubgroupGeneratedMap (G := G) φ
272 let L : Subgroup (K : Subgroup G) := Subgroup.closure (Set.range φK)
273 have hmap :
274 Subgroup.map (K : Subgroup G).subtype L = Subgroup.closure (Set.range φ) := by
275 refine le_antisymm ?_ ?_
276 · rw [Subgroup.map_le_iff_le_comap, Subgroup.closure_le]
277 rintro y ⟨a, rfl⟩
278 exact Subgroup.subset_closure ⟨a, rfl⟩
279 · rw [Subgroup.closure_le]
280 rintro y ⟨a, rfl⟩
281 change φ a ∈ Subgroup.map (K : Subgroup G).subtype L
282 exact ⟨φK a, Subgroup.subset_closure ⟨a, rfl⟩, rfl⟩
283 have himage :
284 ((Subtype.val : ↥(K : Subgroup G) → G) ''
285 ((L : Subgroup ↥(K : Subgroup G)) : Set ↥(K : Subgroup G))) =
286 ((Subgroup.map (K : Subgroup G).subtype L : Subgroup G) : Set G) := by
287 ext y
288 constructor
289 · rintro ⟨z, hz, rfl⟩
290 exact ⟨z, hz, rfl⟩
291 · rintro ⟨z, hz, hzy⟩
292 exact ⟨z, hz, hzy⟩
293 rw [topologicallyGenerates_iff_dense, dense_iff_closure_eq]
294 ext y
295 constructor
296 · intro _
297 simp only [mem_univ]
298 · intro _
299 change y ∈ closure ((L : Subgroup K) : Set K)
300 rw [closure_subtype]
301 change (y : G) ∈
302 closure
303 (((Subtype.val : ↥(K : Subgroup G) → G) ''
304 ((L : Subgroup ↥(K : Subgroup G)) : Set ↥(K : Subgroup G))))
305 rw [himage, hmap]
306 change (y : G) ∈ ((Subgroup.closure (Set.range φ)).topologicalClosure : Set G)
307 exact y.2
309/--
310Membership in a closed generated subgroup is preserved by continuous homomorphisms, after
311mapping the generating set.
312-/
313theorem map_mem_closedSubgroupGenerated_image
314 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
315 (φ : G →ₜ* H) {X : Set G} {y : G}
316 (hy : y ∈ (closedSubgroupGenerated (G := G) X : Subgroup G)) :
317 φ y ∈ (closedSubgroupGenerated (G := H) (φ '' X) : Subgroup H) := by
318 let K : Subgroup G :=
319 (closedSubgroupGenerated (G := H) (φ '' X) : Subgroup H).comap (φ : G →* H)
320 have hX : X ⊆ K := by
321 intro x hx
322 exact Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨x, hx, rfl⟩)
323 have hKclosed : IsClosed (K : Set G) := by
324 change IsClosed {x : G | φ x ∈
325 (closedSubgroupGenerated (G := H) (φ '' X) : Subgroup H)}
326 exact (closedSubgroupGenerated (G := H) (φ '' X)).isClosed'.preimage φ.continuous
327 exact
328 (Subgroup.topologicalClosure_minimal _
329 ((Subgroup.closure_le (K := K)).2 hX) hKclosed) hy
331/--
332Membership in a topologically generated cyclic closed subgroup is preserved by continuous
333homomorphisms.
334-/
335theorem map_mem_closedSubgroupGenerated_singleton
336 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
337 (φ : G →ₜ* H) (x : G) {y : G}
338 (hy : y ∈ (closedSubgroupGenerated (G := G) ({x} : Set G) : Subgroup G)) :
339 φ y ∈ (closedSubgroupGenerated (G := H) ({φ x} : Set H) : Subgroup H) := by
340 simpa using
341 (map_mem_closedSubgroupGenerated_image (G := G) (H := H) φ
342 (X := ({x} : Set G)) hy)
344/-- The distinguished element g algebraically generates its subgroup of powers. -/
345theorem zpowers_subtype_topologically_generated_by_generator
346 {G₀ : Type*} [Group G₀] (g : G₀) :
347 let cyc : Subgroup G₀ := Subgroup.zpowers g
348 let gcyc : cyc := ⟨g, Subgroup.mem_zpowers_iff.mpr ⟨1, by simp only [zpow_one]⟩⟩
349 ∀ z : cyc, z ∈ Subgroup.zpowers gcyc := by
350 intro cyc gcyc z
351 rcases Subgroup.mem_zpowers_iff.mp z.2 with ⟨k, hk⟩
352 refine Subgroup.mem_zpowers_iff.mpr ⟨k, ?_⟩
353 apply Subtype.ext
354 simpa [gcyc] using hk
356/-- A finite discrete image of a topologically cyclic group is algebraically cyclic. -/
357theorem map_mem_zpowers_of_topologicallyGenerates_singleton
358 {A : Type u} [TopologicalSpace A] [Group A] [IsTopologicalGroup A]
359 {B : Type v} [TopologicalSpace B] [Group B] [IsTopologicalGroup B]
360 [DiscreteTopology B]
361 (f : A →ₜ* B) {x a : A}
362 (hxgen : TopologicallyGenerates (G := A) ({x} : Set A)) :
363 f a ∈ Subgroup.zpowers (f x) := by
364 have ha_closed :
365 a ∈ (closedSubgroupGenerated ({x} : Set A) : Subgroup A) := by
366 have htop :
367 (closedSubgroupGenerated ({x} : Set A) : Subgroup A) = ⊤ := by
368 change (Subgroup.closure ({x} : Set A)).topologicalClosure = ⊤
369 exact hxgen
370 rw [htop]
371 simp only [Subgroup.mem_top]
372 have hfa_closed :
373 f a ∈ (closedSubgroupGenerated ({f x} : Set B) : Subgroup B) :=
374 map_mem_closedSubgroupGenerated_singleton f x ha_closed
375 have hclosure_eq :
376 (Subgroup.closure ({f x} : Set B)).topologicalClosure =
377 Subgroup.closure ({f x} : Set B) := by
378 ext y
379 change y ∈ closure (((Subgroup.closure ({f x} : Set B) : Subgroup B) : Set B)) ↔
380 y ∈ ((Subgroup.closure ({f x} : Set B) : Subgroup B) : Set B)
381 rw [closure_discrete]
382 have hfa_closure :
383 f a ∈ Subgroup.closure ({f x} : Set B) := by
384 simpa [closedSubgroupGenerated, hclosure_eq] using hfa_closed
385 simpa [Subgroup.zpowers_eq_closure] using hfa_closure
387/-- MonoidHom version of map_mem_zpowers_of_topologicallyGenerates_singleton. -/
388theorem monoidHom_map_mem_zpowers_of_topologicallyGenerates_singleton
389 {A : Type u} [TopologicalSpace A] [Group A] [IsTopologicalGroup A]
390 {B : Type v} [TopologicalSpace B] [Group B] [IsTopologicalGroup B]
391 [DiscreteTopology B]
392 (f : A →* B) (hf : Continuous f) {x a : A}
393 (hxgen : TopologicallyGenerates (G := A) ({x} : Set A)) :
394 f a ∈ Subgroup.zpowers (f x) := by
395 let fcont : A →ₜ* B :=
396 { toMonoidHom := f
397 continuous_toFun := hf }
398 have hfa :
399 fcont a ∈ Subgroup.zpowers (fcont x) :=
400 map_mem_zpowers_of_topologicallyGenerates_singleton
401 (A := A) fcont hxgen (a := a)
402 change f a ∈ Subgroup.zpowers (f x)
403 exact hfa
405/--
406Algebraic powers of the image of \(x\) lie in the image of the closed subgroup generated by
407\(x\).
408-/
409theorem zpowers_image_le_closedSubgroupGenerated_map
410 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
411 {B : Type v} [Group B]
412 (q : Q →* B) (x : Q) :
413 Subgroup.zpowers (q x) ≤
414 ((closedSubgroupGenerated ({x} : Set Q) : ClosedSubgroup Q) :
415 Subgroup Q).map q := by
416 intro b hb
417 rcases (Subgroup.mem_zpowers_iff.mp hb) with ⟨k, rfl⟩
418 refine ⟨x ^ k, ?_, by simp only [map_zpow]⟩
419 have hxmem :
420 x ∈ ((closedSubgroupGenerated ({x} : Set Q) : ClosedSubgroup Q) :
421 Subgroup Q) := by
422 change x ∈ (Subgroup.closure ({x} : Set Q)).topologicalClosure
423 exact Subgroup.le_topologicalClosure _
424 (Subgroup.subset_closure (by simp only [Set.mem_singleton_iff]))
425 exact
426 ((closedSubgroupGenerated ({x} : Set Q) : ClosedSubgroup Q) :
427 Subgroup Q).zpow_mem hxmem k
429/--
430A dense homomorphic image of the infinite cyclic group is topologically generated by the image
431of \(1\).
432-/
433theorem topologicallyGenerates_singleton_of_denseRange_mint
434 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
435 (f : Multiplicative ℤ →* H) (hf : DenseRange f) :
436 TopologicallyGenerates (G := H) ({f (Multiplicative.ofAdd 1)} : Set H) := by
437 let g : H := f (Multiplicative.ofAdd 1)
438 have hsubset :
439 Set.range f ⊆
440 (((Subgroup.closure ({g} : Set H)).topologicalClosure : Subgroup H) : Set H) := by
441 intro y hy
442 rcases hy with ⟨n, rfl⟩
443 have hz : f n ∈ Subgroup.zpowers g := by
444 have hEq : f n = g ^ n.toAdd := by
445 simpa [g] using (MonoidHom.apply_mint (f := f) (n := n))
446 rw [hEq]
447 exact (Subgroup.zpowers g).zpow_mem (Subgroup.mem_zpowers g) n.toAdd
448 exact Subgroup.le_topologicalClosure _
449 (by simpa [g, Subgroup.zpowers_eq_closure] using hz)
450 have hclosure :
451 closure (Set.range f) ⊆
452 (((Subgroup.closure ({g} : Set H)).topologicalClosure : Subgroup H) : Set H) :=
453 closure_minimal hsubset (Subgroup.isClosed_topologicalClosure _)
454 rw [TopologicallyGenerates]
455 apply top_unique
456 intro x _hx
457 have hx' : x ∈ closure (Set.range f) := by
458 rw [hf.closure_range]
459 simp only [mem_univ]
460 exact hclosure hx'
462/-- Topological generation is unchanged by closing the generating set. -/
463theorem topologicallyGenerates_closure_iff {X : Set G} :
464 TopologicallyGenerates (G := G) X ↔ TopologicallyGenerates (G := G) (closure X) := by
465 constructor
466 · intro hX
467 have hsub :
468 Subgroup.closure X ≤ (Subgroup.closure (closure X)).topologicalClosure := by
469 exact (Subgroup.closure_mono subset_closure).trans (Subgroup.le_topologicalClosure _)
470 have hle :
471 (Subgroup.closure X).topologicalClosure ≤
472 (Subgroup.closure (closure X)).topologicalClosure := by
473 exact Subgroup.topologicalClosure_minimal _ hsub (Subgroup.isClosed_topologicalClosure _)
474 have htop : (⊤ : Subgroup G) ≤ (Subgroup.closure X).topologicalClosure := by
475 rw [hX]
476 exact top_unique (htop.trans hle)
477 · intro hX
478 have hsubset : closure X ⊆ ((Subgroup.closure X).topologicalClosure : Set G) := by
479 refine closure_minimal ?_ (Subgroup.isClosed_topologicalClosure _)
480 intro x hx
481 exact (Subgroup.le_topologicalClosure (Subgroup.closure X)) (Subgroup.subset_closure hx)
482 have hsub : Subgroup.closure (closure X) ≤ (Subgroup.closure X).topologicalClosure := by
483 exact (Subgroup.closure_le (K := (Subgroup.closure X).topologicalClosure)).2 hsubset
484 have hle :
485 (Subgroup.closure (closure X)).topologicalClosure ≤
486 (Subgroup.closure X).topologicalClosure := by
487 exact Subgroup.topologicalClosure_minimal _ hsub (Subgroup.isClosed_topologicalClosure _)
488 have htop : (⊤ : Subgroup G) ≤ (Subgroup.closure (closure X)).topologicalClosure := by
489 rw [hX]
490 exact top_unique (htop.trans hle)
492/-- Adding \(1\) to a topological generating set does not change generation. -/
493theorem topologicallyGenerates_insert_one_iff {X : Set G} :
494 TopologicallyGenerates (G := G) (insert (1 : G) X) ↔ TopologicallyGenerates (G := G) X := by
495 simp only [TopologicallyGenerates, Subgroup.closure_insert_one]
497/-- Union with \(\{1\}\) does not change topological generation. -/
498theorem topologicallyGenerates_union_one_iff {X : Set G} :
499 TopologicallyGenerates (G := G) (X ∪ ({1} : Set G)) ↔ TopologicallyGenerates (G := G) X := by
500 simpa [Set.union_singleton] using topologicallyGenerates_insert_one_iff (G := G) (X := X)
502omit [TopologicalSpace G] [IsTopologicalGroup G] in
503/--
504Removing occurrences of 1 from a parametrized generating range does not change its abstract
505subgroup closure.
506-/
507theorem closure_nontrivial_range_eq_closure_range
508 {α : Type v} (f : α → G) :
509 Subgroup.closure ({g | ∃ a, g = f a ∧ g ≠ 1} : Set G) =
510 Subgroup.closure (Set.range f) := by
511 apply le_antisymm
512 · exact Subgroup.closure_mono (by
513 rintro g ⟨a, rfl, _⟩
514 exact ⟨a, rfl⟩)
515 · have hrange :
516 Set.range f ⊆ insert (1 : G) ({g | ∃ a, g = f a ∧ g ≠ 1} : Set G) := by
517 rintro g ⟨a, rfl⟩
518 by_cases h : f a = 1
519 · exact Or.inl h
520 · exact Or.inr ⟨a, rfl, h⟩
521 refine (Subgroup.closure_mono hrange).trans ?_
522 exact le_of_eq (Subgroup.closure_insert_one ({g | ∃ a, g = f a ∧ g ≠ 1} : Set G))
524/-- Topological generation is monotone in the generating set. -/
525theorem topologicallyGenerates_mono {X Y : Set G}
526 (hX : TopologicallyGenerates (G := G) X) (hXY : X ⊆ Y) :
527 TopologicallyGenerates (G := G) Y := by
528 have hle :
529 (Subgroup.closure X).topologicalClosure ≤ (Subgroup.closure Y).topologicalClosure := by
530 exact Subgroup.topologicalClosure_minimal _
531 ((Subgroup.closure_mono hXY).trans (Subgroup.le_topologicalClosure _))
532 (Subgroup.isClosed_topologicalClosure _)
533 have htop : (⊤ : Subgroup G) ≤ (Subgroup.closure X).topologicalClosure := by
534 simpa [TopologicallyGenerates] using (show TopologicallyGenerates (G := G) X from hX)
535 exact top_unique (htop.trans hle)
537/-- A topological generating set may be replaced by any set whose abstract closure contains it. -/
538theorem topologicallyGenerates_of_subset_closure {X Y : Set G}
539 (hX : TopologicallyGenerates (G := G) X)
540 (hXY : X ⊆ ((Subgroup.closure Y : Subgroup G) : Set G)) :
541 TopologicallyGenerates (G := G) Y := by
542 have hle : Subgroup.closure X ≤ Subgroup.closure Y :=
543 (Subgroup.closure_le (K := Subgroup.closure Y)).2 hXY
544 have hle' :
545 (Subgroup.closure X).topologicalClosure ≤ (Subgroup.closure Y).topologicalClosure := by
546 exact Subgroup.topologicalClosure_minimal _
547 (hle.trans (Subgroup.le_topologicalClosure _))
548 (Subgroup.isClosed_topologicalClosure _)
549 have htop : (⊤ : Subgroup G) ≤ (Subgroup.closure X).topologicalClosure := by
550 simpa [TopologicallyGenerates] using (show TopologicallyGenerates (G := G) X from hX)
551 exact top_unique (htop.trans hle')
553/-- Topological generation pushes forward along continuous surjective homomorphisms. -/
554theorem topologicallyGenerates_image_of_continuousSurjective
555 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
556 (f : G →* H) (hf : Continuous f) (hfsurj : Function.Surjective f)
557 {X : Set G} (hX : TopologicallyGenerates (G := G) X) :
558 TopologicallyGenerates (G := H) (f '' X) := by
559 have hmap :
560 (Subgroup.closure X).map f = Subgroup.closure (f '' X) := by
561 simpa using MonoidHom.map_closure f X
562 have htop :
563 ((Subgroup.closure X).map f).topologicalClosure = ⊤ := by
564 exact DenseRange.topologicalClosure_map_subgroup
565 (f := f)
566 (hf := hf)
567 (hf' := hfsurj.denseRange)
568 (by simpa [TopologicallyGenerates] using hX)
569 rw [TopologicallyGenerates, ← hmap]
570 exact htop
572/-- Continuous-homomorphism form of push-forward for topological generation. -/
573theorem topologicallyGenerates_image_of_continuousMonoidHom_surjective
574 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
575 (f : G →ₜ* H) (hfsurj : Function.Surjective f)
576 {X : Set G} (hX : TopologicallyGenerates (G := G) X) :
577 TopologicallyGenerates (G := H) (f '' X) :=
578 topologicallyGenerates_image_of_continuousSurjective
579 (G := G) (H := H) f.toMonoidHom f.continuous_toFun hfsurj hX
581omit [IsTopologicalGroup G] in
582/--
583A continuous homomorphism from a compact group onto a Hausdorff target is surjective as soon as
584its closed range contains a topological generating set of the target.
585-/
586theorem continuousMonoidHom_surjective_of_topologicallyGenerates_subset_range
587 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
588 [CompactSpace G] [T2Space H]
589 (f : G →ₜ* H) {X : Set H} (hX : TopologicallyGenerates (G := H) X)
590 (hXrange : X ⊆ ((f.toMonoidHom.range : Subgroup H) : Set H)) :
591 Function.Surjective f := by
592 have hrangeClosed : IsClosed (((f.toMonoidHom.range : Subgroup H) : Set H)) := by
593 have himage : IsCompact (f '' (Set.univ : Set G)) :=
594 isCompact_univ.image f.continuous_toFun
595 have hEq :
596 f '' (Set.univ : Set G) =
597 ((f.toMonoidHom.range : Subgroup H) : Set H) := by
598 ext y
599 constructor
600 · rintro ⟨x, _hx, rfl⟩
601 exact ⟨x, rfl⟩
602 · rintro ⟨x, rfl⟩
603 exact ⟨x, trivial, rfl⟩
604 exact (hEq ▸ himage).isClosed
605 have hclosure_le :
606 (Subgroup.closure X).topologicalClosure ≤ f.toMonoidHom.range :=
607 Subgroup.topologicalClosure_minimal _
608 ((Subgroup.closure_le (K := f.toMonoidHom.range)).2 hXrange) hrangeClosed
609 have htop : (⊤ : Subgroup H) ≤ f.toMonoidHom.range := by
610 rw [← hX]
611 exact hclosure_le
612 intro y
613 exact htop trivial
615/-- Topological generation descends to every quotient by a normal subgroup. -/
616theorem topologicallyGenerates_quotient_image
617 (N : Subgroup G) [N.Normal]
618 {X : Set G} (hX : TopologicallyGenerates (G := G) X) :
619 TopologicallyGenerates (G := G ⧸ N) ((QuotientGroup.mk' N) '' X) :=
620 topologicallyGenerates_image_of_continuousSurjective
621 (G := G)
622 (H := G ⧸ N)
623 (QuotientGroup.mk' N)
624 continuous_quotient_mk'
625 (QuotientGroup.mk'_surjective N)
626 hX
628/-- Topological generation is preserved by continuous multiplicative equivalences. -/
629theorem topologicallyGenerates_continuousMulEquiv_image
630 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
631 (e : G ≃ₜ* H) {X : Set G} (hX : TopologicallyGenerates (G := G) X) :
632 TopologicallyGenerates (G := H) (e '' X) :=
633 topologicallyGenerates_image_of_continuousSurjective
634 (G := G) (H := H) e.toMonoidHom e.continuous e.surjective hX
636/-- Topological generation is transported across a continuous multiplicative equivalence. -/
637theorem topologicallyGenerates_continuousMulEquiv_image_iff
638 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
639 (e : G ≃ₜ* H) {X : Set G} :
640 TopologicallyGenerates (G := H) (e '' X) ↔ TopologicallyGenerates (G := G) X := by
641 constructor
642 · intro h
643 have hpre :=
644 topologicallyGenerates_continuousMulEquiv_image
645 (G := H) (H := G) e.symm (X := e '' X) h
646 have hset : e.symm '' (e '' X) = X := by
647 ext x
648 constructor
649 · rintro ⟨y, ⟨z, hz, rfl⟩, rfl⟩
650 simpa using hz
651 · intro hx
652 exact ⟨e x, ⟨x, hx, rfl⟩, by simp only [ContinuousMulEquiv.symm_apply_apply]⟩
653 simpa [hset] using hpre
654 · exact topologicallyGenerates_continuousMulEquiv_image (G := G) (H := H) e
656end
658end ProCGroups.Generation