ProCGroups/Generation/Basic.lean
1import Mathlib.Topology.Algebra.ClopenNhdofOne
2import Mathlib.Topology.Algebra.ContinuousMonoidHom
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/Generation/Basic.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Topological generation
15Develops topological generation, generating families, convergence-to-one criteria, quotient generation, and profinite generation lemmas.
16-/
18open Set
19open scoped Topology Pointwise
21namespace ProCGroups.Generation
23universe u v
25section
27variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
29/-- `X` topologically generates `G` if the abstract subgroup generated by `X`
30is dense in `G`. -/
31def TopologicallyGenerates (X : Set G) : Prop :=
32 (Subgroup.closure X).topologicalClosure = ⊤
34/-- `X` converges to `1` if every open subgroup contains all but finitely many elements of `X`. -/
35def ConvergesToOne (X : Set G) : Prop :=
36 ∀ U : OpenSubgroup G, (X \ (U : Set G)).Finite
38omit [IsTopologicalGroup G] in
39/-- A finite set converges to `1` in the coarse sense used for profinite generating families. -/
40theorem ConvergesToOne.of_finite {X : Set G} (hX : X.Finite) :
41 ConvergesToOne (G := G) X := by
42 intro U
43 exact hX.subset (by
44 intro x hx
45 exact hx.1)
47/-- A generating set converging to `1`. -/
48def GeneratesAndConvergesToOne (X : Set G) : Prop :=
49 TopologicallyGenerates (G := G) X ∧ ConvergesToOne (G := G) X
51/-- The minimal cardinality of a generating set converging to `1`.
53This is the topological rank usually denoted `d(G)` in the profinite-group
54literature. The declaration name is intentionally descriptive for public API
55use. -/
56noncomputable def topologicalRank
57 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
58 Cardinal :=
59 sInf {κ : Cardinal | ∃ X : Set G, GeneratesAndConvergesToOne (G := G) X ∧ Cardinal.mk X = κ}
61/-- The topological rank is bounded by the cardinality of any generating set converging to `1`. -/
62theorem topologicalRank_le_mk_of_generatesAndConvergesToOne {X : Set G}
63 (hX : GeneratesAndConvergesToOne (G := G) X) :
64 topologicalRank G ≤ Cardinal.mk X := by
65 change sInf {κ : Cardinal |
66 ∃ X : Set G, GeneratesAndConvergesToOne (G := G) X ∧ Cardinal.mk X = κ} ≤
67 Cardinal.mk X
68 exact csInf_le' ⟨X, hX, rfl⟩
70/-- If at least one generating set converging to `1` exists, one may choose such a set whose
71cardinality is exactly the topological rank. -/
73 (h : ∃ X : Set G, GeneratesAndConvergesToOne (G := G) X) :
74 ∃ X : Set G, GeneratesAndConvergesToOne (G := G) X ∧
75 Cardinal.mk X = topologicalRank G := by
76 let C : Set Cardinal := {κ : Cardinal |
77 ∃ X : Set G, GeneratesAndConvergesToOne (G := G) X ∧ Cardinal.mk X = κ}
78 have hC : C.Nonempty := by
79 rcases h with ⟨X, hX⟩
80 exact ⟨Cardinal.mk X, X, hX, rfl⟩
81 simpa [topologicalRank, C] using (csInf_mem hC)
83/-- Iterated products of words in `X`, with `wordProducts X 0 = {1}` and
84`wordProducts X (n + 1) = wordProducts X n * X`. -/
85def wordProducts (X : Set G) : ℕ → Set G
86 | 0 => {1}
87 | n + 1 => wordProducts X n * X
89/-- Topological generation is equivalently density of the abstract subgroup generated by the set. -/
90theorem topologicallyGenerates_iff_dense {X : Set G} :
91 TopologicallyGenerates (G := G) X ↔ Dense ((Subgroup.closure X : Subgroup G) : Set G) := by
92 rw [TopologicallyGenerates, SetLike.ext'_iff, Subgroup.topologicalClosure_coe, Subgroup.coe_top,
93 dense_iff_closure_eq]
95/-- Continuous homomorphisms out of a topologically generated group are determined by their
96values on the generating set. -/
98 {R : Type v} [Group R] [TopologicalSpace R] [T2Space R]
99 {X : Set G} (hX : TopologicallyGenerates (G := G) X)
100 {f g : ContinuousMonoidHom G R} (hfg : ∀ x ∈ X, f x = g x) :
101 f = g := by
102 let K : Subgroup G := {
103 carrier := { x | f x = g x }
105 mul_mem' := by
106 intro a b ha hb
107 change f (a * b) = g (a * b)
109 inv_mem' := by
110 intro a ha
111 simpa using congrArg Inv.inv ha
112 }
113 have hKclosed : IsClosed ((K : Subgroup G) : Set G) := by
114 change IsClosed { x | f x = g x }
115 exact isClosed_eq f.continuous_toFun g.continuous_toFun
116 have hsub : Subgroup.closure X ≤ K := by
117 rw [Subgroup.closure_le]
118 intro x hx
119 exact hfg x hx
120 have htop : (⊤ : Subgroup G) ≤ K := by
121 have hcl : (Subgroup.closure X).topologicalClosure ≤ K :=
122 Subgroup.topologicalClosure_minimal _ hsub hKclosed
123 rw [TopologicallyGenerates] at hX
124 simpa [hX] using hcl
125 ext x
126 simpa [K] using htop (show x ∈ (⊤ : Subgroup G) from by simp only [Subgroup.mem_top])
128/-- The closed subgroup topologically generated by a set. -/
129def closedSubgroupGenerated (X : Set G) : ClosedSubgroup G where
130 toSubgroup := (Subgroup.closure X).topologicalClosure
131 isClosed' := Subgroup.isClosed_topologicalClosure _
133/-- The canonical map from an indexed family into the closed subgroup it topologically
134generates. -/
135def closedSubgroupGeneratedMap {A : Type v} (φ : A → G) :
136 A → (closedSubgroupGenerated (G := G) (Set.range φ) : Subgroup G) :=
137 fun a =>
138 ⟨φ a, Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨a, rfl⟩)⟩
140/-- The canonical indexed family topologically generates its closed generated subgroup. -/
141theorem closedSubgroupGeneratedMap_topologicallyGenerates {A : Type v} (φ : A → G) :
143 (G := (closedSubgroupGenerated (G := G) (Set.range φ) : Subgroup G))
144 (Set.range (closedSubgroupGeneratedMap (G := G) φ)) := by
145 let K : ClosedSubgroup G := closedSubgroupGenerated (G := G) (Set.range φ)
146 let φK : A → (K : Subgroup G) := closedSubgroupGeneratedMap (G := G) φ
147 let L : Subgroup (K : Subgroup G) := Subgroup.closure (Set.range φK)
148 have hmap :
150 refine le_antisymm ?_ ?_
151 · rw [Subgroup.map_le_iff_le_comap, Subgroup.closure_le]
152 rintro y ⟨a, rfl⟩
153 exact Subgroup.subset_closure ⟨a, rfl⟩
154 · rw [Subgroup.closure_le]
155 rintro y ⟨a, rfl⟩
157 exact ⟨φK a, Subgroup.subset_closure ⟨a, rfl⟩, rfl⟩
158 have himage :
159 ((Subtype.val : ↥(K : Subgroup G) → G) ''
160 ((L : Subgroup ↥(K : Subgroup G)) : Set ↥(K : Subgroup G))) =
162 ext y
163 constructor
164 · rintro ⟨z, hz, rfl⟩
165 exact ⟨z, hz, rfl⟩
166 · rintro ⟨z, hz, hzy⟩
167 exact ⟨z, hz, hzy⟩
168 rw [topologicallyGenerates_iff_dense, dense_iff_closure_eq]
169 ext y
170 constructor
171 · intro _
172 simp only [mem_univ]
173 · intro _
174 change y ∈ closure ((L : Subgroup K) : Set K)
175 rw [closure_subtype]
176 change (y : G) ∈
177 closure
178 (((Subtype.val : ↥(K : Subgroup G) → G) ''
179 ((L : Subgroup ↥(K : Subgroup G)) : Set ↥(K : Subgroup G))))
180 rw [himage, hmap]
181 change (y : G) ∈ ((Subgroup.closure (Set.range φ)).topologicalClosure : Set G)
182 exact y.2
184/-- Membership in a closed generated subgroup is preserved by continuous homomorphisms, after
185mapping the generating set. -/
187 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
188 (φ : G →ₜ* H) {X : Set G} {y : G}
189 (hy : y ∈ (closedSubgroupGenerated (G := G) X : Subgroup G)) :
190 φ y ∈ (closedSubgroupGenerated (G := H) (φ '' X) : Subgroup H) := by
191 let K : Subgroup G :=
192 (closedSubgroupGenerated (G := H) (φ '' X) : Subgroup H).comap (φ : G →* H)
193 have hX : X ⊆ K := by
194 intro x hx
195 exact Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨x, hx, rfl⟩)
196 have hKclosed : IsClosed (K : Set G) := by
197 change IsClosed {x : G | φ x ∈
198 (closedSubgroupGenerated (G := H) (φ '' X) : Subgroup H)}
199 exact (closedSubgroupGenerated (G := H) (φ '' X)).isClosed'.preimage φ.continuous
200 exact
201 (Subgroup.topologicalClosure_minimal _
202 ((Subgroup.closure_le (K := K)).2 hX) hKclosed) hy
204/-- Membership in a topologically generated cyclic closed subgroup is preserved by continuous
205homomorphisms. -/
207 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
208 (φ : G →ₜ* H) (x : G) {y : G}
209 (hy : y ∈ (closedSubgroupGenerated (G := G) ({x} : Set G) : Subgroup G)) :
210 φ y ∈ (closedSubgroupGenerated (G := H) ({φ x} : Set H) : Subgroup H) := by
211 simpa using
212 (map_mem_closedSubgroupGenerated_image (G := G) (H := H) φ
213 (X := ({x} : Set G)) hy)
215/-- The distinguished element `g` algebraically generates its subgroup of powers. -/
217 {G₀ : Type*} [Group G₀] (g : G₀) :
218 let cyc : Subgroup G₀ := Subgroup.zpowers g
219 let gcyc : cyc := ⟨g, Subgroup.mem_zpowers_iff.mpr ⟨1, by simp only [zpow_one]⟩⟩
220 ∀ z : cyc, z ∈ Subgroup.zpowers gcyc := by
221 intro cyc gcyc z
222 rcases Subgroup.mem_zpowers_iff.mp z.2 with ⟨k, hk⟩
223 refine Subgroup.mem_zpowers_iff.mpr ⟨k, ?_⟩
224 apply Subtype.ext
225 simpa [gcyc] using hk
227/-- A finite discrete image of a topologically cyclic group is algebraically cyclic. -/
229 {A : Type u} [TopologicalSpace A] [Group A] [IsTopologicalGroup A]
230 {B : Type v} [TopologicalSpace B] [Group B] [IsTopologicalGroup B]
231 [DiscreteTopology B]
232 (f : A →ₜ* B) {x a : A}
233 (hxgen : TopologicallyGenerates (G := A) ({x} : Set A)) :
234 f a ∈ Subgroup.zpowers (f x) := by
235 have ha_closed :
236 a ∈ (closedSubgroupGenerated ({x} : Set A) : Subgroup A) := by
237 have htop :
238 (closedSubgroupGenerated ({x} : Set A) : Subgroup A) = ⊤ := by
239 simpa [closedSubgroupGenerated] using hxgen
240 rw [htop]
241 simp only [Subgroup.mem_top]
242 have hfa_closed :
243 f a ∈ (closedSubgroupGenerated ({f x} : Set B) : Subgroup B) :=
244 map_mem_closedSubgroupGenerated_singleton f x ha_closed
245 have hclosure_eq :
246 (Subgroup.closure ({f x} : Set B)).topologicalClosure =
247 Subgroup.closure ({f x} : Set B) := by
248 ext y
249 change y ∈ closure (((Subgroup.closure ({f x} : Set B) : Subgroup B) : Set B)) ↔
250 y ∈ ((Subgroup.closure ({f x} : Set B) : Subgroup B) : Set B)
251 rw [closure_discrete]
252 have hfa_closure :
253 f a ∈ Subgroup.closure ({f x} : Set B) := by
254 simpa [closedSubgroupGenerated, hclosure_eq] using hfa_closed
255 simpa [Subgroup.zpowers_eq_closure] using hfa_closure
257/-- `MonoidHom` version of `map_mem_zpowers_of_topologicallyGenerates_singleton`. -/
259 {A : Type u} [TopologicalSpace A] [Group A] [IsTopologicalGroup A]
260 {B : Type v} [TopologicalSpace B] [Group B] [IsTopologicalGroup B]
261 [DiscreteTopology B]
262 (f : A →* B) (hf : Continuous f) {x a : A}
263 (hxgen : TopologicallyGenerates (G := A) ({x} : Set A)) :
264 f a ∈ Subgroup.zpowers (f x) := by
265 let fcont : A →ₜ* B :=
266 { toMonoidHom := f
267 continuous_toFun := hf }
268 simpa [fcont] using
270 (A := A) fcont hxgen (a := a)
272/-- Algebraic powers of the image of `x` lie in the image of the closed subgroup generated by
273`x`. -/
275 {Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
276 {B : Type v} [Group B]
277 (q : Q →* B) (x : Q) :
278 Subgroup.zpowers (q x) ≤
279 ((closedSubgroupGenerated ({x} : Set Q) : ClosedSubgroup Q) :
280 Subgroup Q).map q := by
281 intro b hb
282 rcases (Subgroup.mem_zpowers_iff.mp hb) with ⟨k, rfl⟩
283 refine ⟨x ^ k, ?_, by simp only [map_zpow]⟩
284 have hxmem :
285 x ∈ ((closedSubgroupGenerated ({x} : Set Q) : ClosedSubgroup Q) :
286 Subgroup Q) := by
287 change x ∈ (Subgroup.closure ({x} : Set Q)).topologicalClosure
288 exact Subgroup.le_topologicalClosure _
289 (Subgroup.subset_closure (by simp only [Set.mem_singleton_iff]))
290 exact
291 ((closedSubgroupGenerated ({x} : Set Q) : ClosedSubgroup Q) :
292 Subgroup Q).zpow_mem hxmem k
294/-- A dense homomorphic image of the infinite cyclic group is topologically generated by the
295image of `1`. -/
297 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
298 (f : Multiplicative ℤ →* H) (hf : DenseRange f) :
299 TopologicallyGenerates (G := H) ({f (Multiplicative.ofAdd 1)} : Set H) := by
300 let g : H := f (Multiplicative.ofAdd 1)
301 have hsubset :
302 Set.range f ⊆
303 (((Subgroup.closure ({g} : Set H)).topologicalClosure : Subgroup H) : Set H) := by
304 intro y hy
305 rcases hy with ⟨n, rfl⟩
306 have hz : f n ∈ Subgroup.zpowers g := by
307 have hEq : f n = g ^ n.toAdd := by
308 simpa [g] using (MonoidHom.apply_mint (f := f) (n := n))
309 rw [hEq]
310 exact (Subgroup.zpowers g).zpow_mem (Subgroup.mem_zpowers g) n.toAdd
311 exact Subgroup.le_topologicalClosure _
312 (by simpa [g, Subgroup.zpowers_eq_closure] using hz)
313 have hclosure :
314 closure (Set.range f) ⊆
315 (((Subgroup.closure ({g} : Set H)).topologicalClosure : Subgroup H) : Set H) :=
316 closure_minimal hsubset (Subgroup.isClosed_topologicalClosure _)
318 apply top_unique
319 intro x _hx
320 have hx' : x ∈ closure (Set.range f) := by
321 rw [hf.closure_range]
322 simp only [mem_univ]
323 exact hclosure hx'
325/-- Topological generation is unchanged by closing the generating set. -/
326theorem topologicallyGenerates_closure_iff {X : Set G} :
327 TopologicallyGenerates (G := G) X ↔ TopologicallyGenerates (G := G) (closure X) := by
328 constructor
329 · intro hX
330 have hsub :
331 Subgroup.closure X ≤ (Subgroup.closure (closure X)).topologicalClosure := by
332 exact (Subgroup.closure_mono subset_closure).trans (Subgroup.le_topologicalClosure _)
333 have hle :
334 (Subgroup.closure X).topologicalClosure ≤
335 (Subgroup.closure (closure X)).topologicalClosure := by
336 exact Subgroup.topologicalClosure_minimal _ hsub (Subgroup.isClosed_topologicalClosure _)
337 have htop : (⊤ : Subgroup G) ≤ (Subgroup.closure X).topologicalClosure := by
338 rw [hX]
339 exact top_unique (htop.trans hle)
340 · intro hX
341 have hsubset : closure X ⊆ ((Subgroup.closure X).topologicalClosure : Set G) := by
342 refine closure_minimal ?_ (Subgroup.isClosed_topologicalClosure _)
343 intro x hx
344 exact (Subgroup.le_topologicalClosure (Subgroup.closure X)) (Subgroup.subset_closure hx)
345 have hsub : Subgroup.closure (closure X) ≤ (Subgroup.closure X).topologicalClosure := by
346 exact (Subgroup.closure_le (K := (Subgroup.closure X).topologicalClosure)).2 hsubset
347 have hle :
348 (Subgroup.closure (closure X)).topologicalClosure ≤
349 (Subgroup.closure X).topologicalClosure := by
350 exact Subgroup.topologicalClosure_minimal _ hsub (Subgroup.isClosed_topologicalClosure _)
351 have htop : (⊤ : Subgroup G) ≤ (Subgroup.closure (closure X)).topologicalClosure := by
352 rw [hX]
353 exact top_unique (htop.trans hle)
355/-- Adding `1` to a topological generating set does not change generation. -/
356theorem topologicallyGenerates_insert_one_iff {X : Set G} :
357 TopologicallyGenerates (G := G) (insert (1 : G) X) ↔ TopologicallyGenerates (G := G) X := by
358 simp only [TopologicallyGenerates, Subgroup.closure_insert_one]
360/-- Union with `{1}` does not change topological generation. -/
361theorem topologicallyGenerates_union_one_iff {X : Set G} :
362 TopologicallyGenerates (G := G) (X ∪ ({1} : Set G)) ↔ TopologicallyGenerates (G := G) X := by
363 simpa [Set.union_singleton] using topologicallyGenerates_insert_one_iff (G := G) (X := X)
365omit [TopologicalSpace G] [IsTopologicalGroup G] in
366/-- Removing occurrences of `1` from a parametrized generating range does not change its abstract
367subgroup closure. -/
369 {α : Type v} (f : α → G) :
370 Subgroup.closure ({g | ∃ a, g = f a ∧ g ≠ 1} : Set G) =
371 Subgroup.closure (Set.range f) := by
372 apply le_antisymm
373 · exact Subgroup.closure_mono (by
374 rintro g ⟨a, rfl, _⟩
375 exact ⟨a, rfl⟩)
376 · have hrange :
377 Set.range f ⊆ insert (1 : G) ({g | ∃ a, g = f a ∧ g ≠ 1} : Set G) := by
378 rintro g ⟨a, rfl⟩
379 by_cases h : f a = 1
380 · exact Or.inl h
381 · exact Or.inr ⟨a, rfl, h⟩
382 refine (Subgroup.closure_mono hrange).trans ?_
383 exact le_of_eq (Subgroup.closure_insert_one ({g | ∃ a, g = f a ∧ g ≠ 1} : Set G))
385/-- Topological generation is monotone in the generating set. -/
386theorem topologicallyGenerates_mono {X Y : Set G}
387 (hX : TopologicallyGenerates (G := G) X) (hXY : X ⊆ Y) :
388 TopologicallyGenerates (G := G) Y := by
389 have hle :
390 (Subgroup.closure X).topologicalClosure ≤ (Subgroup.closure Y).topologicalClosure := by
391 exact Subgroup.topologicalClosure_minimal _
392 ((Subgroup.closure_mono hXY).trans (Subgroup.le_topologicalClosure _))
393 (Subgroup.isClosed_topologicalClosure _)
394 have htop : (⊤ : Subgroup G) ≤ (Subgroup.closure X).topologicalClosure := by
395 simpa [TopologicallyGenerates] using (show TopologicallyGenerates (G := G) X from hX)
396 exact top_unique (htop.trans hle)
398/-- A topological generating set may be replaced by any set whose abstract closure contains it. -/
399theorem topologicallyGenerates_of_subset_closure {X Y : Set G}
400 (hX : TopologicallyGenerates (G := G) X)
401 (hXY : X ⊆ ((Subgroup.closure Y : Subgroup G) : Set G)) :
402 TopologicallyGenerates (G := G) Y := by
403 have hle : Subgroup.closure X ≤ Subgroup.closure Y :=
404 (Subgroup.closure_le (K := Subgroup.closure Y)).2 hXY
405 have hle' :
406 (Subgroup.closure X).topologicalClosure ≤ (Subgroup.closure Y).topologicalClosure := by
407 exact Subgroup.topologicalClosure_minimal _
408 (hle.trans (Subgroup.le_topologicalClosure _))
409 (Subgroup.isClosed_topologicalClosure _)
410 have htop : (⊤ : Subgroup G) ≤ (Subgroup.closure X).topologicalClosure := by
411 simpa [TopologicallyGenerates] using (show TopologicallyGenerates (G := G) X from hX)
412 exact top_unique (htop.trans hle')
414/-- Topological generation pushes forward along continuous surjective homomorphisms. -/
416 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
417 (f : G →* H) (hf : Continuous f) (hfsurj : Function.Surjective f)
418 {X : Set G} (hX : TopologicallyGenerates (G := G) X) :
419 TopologicallyGenerates (G := H) (f '' X) := by
420 have hmap :
421 (Subgroup.closure X).map f = Subgroup.closure (f '' X) := by
422 simpa using MonoidHom.map_closure f X
423 have htop :
424 ((Subgroup.closure X).map f).topologicalClosure = ⊤ := by
425 exact DenseRange.topologicalClosure_map_subgroup
426 (f := f)
427 (hf := hf)
428 (hf' := hfsurj.denseRange)
429 (by simpa [TopologicallyGenerates] using hX)
430 rw [TopologicallyGenerates, ← hmap]
431 exact htop
433/-- Continuous-homomorphism form of push-forward for topological generation. -/
435 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
436 (f : G →ₜ* H) (hfsurj : Function.Surjective f)
437 {X : Set G} (hX : TopologicallyGenerates (G := G) X) :
438 TopologicallyGenerates (G := H) (f '' X) :=
440 (G := G) (H := H) f.toMonoidHom f.continuous_toFun hfsurj hX
442omit [IsTopologicalGroup G] in
443/-- A continuous homomorphism from a compact group onto a Hausdorff target is surjective as soon
444as its closed range contains a topological generating set of the target. -/
446 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
447 [CompactSpace G] [T2Space H]
448 (f : G →ₜ* H) {X : Set H} (hX : TopologicallyGenerates (G := H) X)
449 (hXrange : X ⊆ ((f.toMonoidHom.range : Subgroup H) : Set H)) :
450 Function.Surjective f := by
451 have hrangeClosed : IsClosed (((f.toMonoidHom.range : Subgroup H) : Set H)) := by
453 isCompact_univ.image f.continuous_toFun
454 have hEq :
455 f '' (Set.univ : Set G) =
456 ((f.toMonoidHom.range : Subgroup H) : Set H) := by
457 ext y
458 constructor
459 · rintro ⟨x, _hx, rfl⟩
460 exact ⟨x, rfl⟩
461 · rintro ⟨x, rfl⟩
462 exact ⟨x, trivial, rfl⟩
463 exact (hEq ▸ himage).isClosed
464 have hclosure_le :
465 (Subgroup.closure X).topologicalClosure ≤ f.toMonoidHom.range :=
466 Subgroup.topologicalClosure_minimal _
467 ((Subgroup.closure_le (K := f.toMonoidHom.range)).2 hXrange) hrangeClosed
468 have htop : (⊤ : Subgroup H) ≤ f.toMonoidHom.range := by
469 rw [← hX]
470 exact hclosure_le
471 intro y
472 exact htop trivial
474/-- Topological generation descends to every quotient by a normal subgroup. -/
476 (N : Subgroup G) [N.Normal]
477 {X : Set G} (hX : TopologicallyGenerates (G := G) X) :
478 TopologicallyGenerates (G := G ⧸ N) ((QuotientGroup.mk' N) '' X) :=
480 (G := G)
481 (H := G ⧸ N)
482 (QuotientGroup.mk' N)
483 continuous_quotient_mk'
484 (QuotientGroup.mk'_surjective N)
485 hX
487/-- Topological generation is preserved by continuous multiplicative equivalences. -/
489 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
490 (e : G ≃ₜ* H) {X : Set G} (hX : TopologicallyGenerates (G := G) X) :
491 TopologicallyGenerates (G := H) (e '' X) :=
493 (G := G) (H := H) e.toMonoidHom e.continuous e.surjective hX
495/-- Topological generation transported across a continuous multiplicative equivalence. -/
497 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
498 (e : G ≃ₜ* H) {X : Set G} :
499 TopologicallyGenerates (G := H) (e '' X) ↔ TopologicallyGenerates (G := G) X := by
500 constructor
501 · intro h
502 have hpre :=
504 (G := H) (H := G) e.symm (X := e '' X) h
505 have hset : e.symm '' (e '' X) = X := by
506 ext x
507 constructor
508 · rintro ⟨y, ⟨z, hz, rfl⟩, rfl⟩
509 simpa using hz
510 · intro hx
511 exact ⟨e x, ⟨x, hx, rfl⟩, by simp only [ContinuousMulEquiv.symm_apply_apply]⟩
512 simpa [hset] using hpre
513 · exact topologicallyGenerates_continuousMulEquiv_image (G := G) (H := H) e
515end
517end ProCGroups.Generation