Topological generation of a topological group

A subset of a topological group generates it topologically when the subgroup it generates is dense, that is when (Subgroup.closure s).topologicalClosure = ⊤. This file introduces the predicate IsTopologicallyFinitelyGenerated, asking for a finite topological generating set, and its basic API.

The predicate is covariant: a topological generating set is carried to a topological generating set by any continuous homomorphism with dense range, hence in particular by a continuous surjection and so to every quotient. It is invariant under a topological group isomorphism, and it has the uniqueness half one expects of a notion of generation — a continuous homomorphism into a Hausdorff monoid is determined by its values on a topological generating set, as is a homomorphism with open kernel into an arbitrary group. Counting the latter over a finite target is what bounds the supply of open subgroups of a compact group.

For a profinite group topological finite generation is detected by the finite quotients; that criterion is in TauCeti/Topology/Algebra/Group/Profinite/Generation.lean.

Main results

• TauCeti.IsTopologicallyFinitelyGenerated: some finite subset generates a dense subgroup.
• TauCeti.topologicalClosure_closure_image_eq_top: the image of a topological generating set under a continuous homomorphism with dense range is a topological generating set.
• TauCeti.IsTopologicallyFinitelyGenerated.of_denseRange, TauCeti.IsTopologicallyFinitelyGenerated.of_surjective, TauCeti.IsTopologicallyFinitelyGenerated.quotient: topological finite generation passes along continuous homomorphisms with dense range, along continuous surjections, and to quotients.
• TauCeti.topologicalClosure_closure_sup_eq_top_iff: a subset together with a normal subgroup K topologically generates G exactly when its image topologically generates G ⧸ K.
• MonoidHom.ker_eq_topologicalClosure_normalClosure_insert_pow_of_orderOf_eq: if a character kills all but one topological generator, whose image has finite order m > 0, its kernel is the closed normal closure of the killed generators and the m-th power of the remaining one.
• TauCeti.IsTopologicallyFinitelyGenerated.of_openSubgroup_of_finiteIndex, TauCeti.IsTopologicallyFinitelyGenerated.of_openSubgroup: topological finite generation passes to open finite-index subgroups, in particular to open subgroups of compact groups.
• MonoidHom.eqOn_topologicalClosure_closure and MonoidHom.eq_of_eqOn_of_topologicalClosure_closure_eq_top: continuous homomorphisms into a Hausdorff monoid agreeing on a set agree on the closed subgroup it generates, so such a homomorphism is determined by its values on a topological generating set.
• MonoidHom.eq_of_eqOn_of_isOpen_ker: the same uniqueness statement for a homomorphism with open kernel, for which the target carries no topology.
• TauCeti.IsTopologicallyFinitelyGenerated.finite_monoidHom_isOpen_ker: only finitely many homomorphisms with open kernel go from a topologically finitely generated group to a fixed finite group.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Corollary 3.6.3.
• Mathlib's Subgroup.fg_of_index_ne_zero and DenseRange.subset_closure_image_preimage_of_isOpen.

def TauCeti.IsTopologicallyFinitelyGenerated (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop

Topological finite generation: some finite subset of G generates a dense subgroup. For a profinite group this is the notion of finite generation that all of the pro-p theory uses; abstract finite generation is strictly stronger and is never meant.

Equations

• TauCeti.IsTopologicallyFinitelyGenerated G = ∃ (s : Finset G), (Subgroup.closure ↑s).topologicalClosure = ⊤

@[simp]

theorem TauCeti.isTopologicallyFinitelyGenerated_iff {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : IsTopologicallyFinitelyGenerated G ↔ ∃ (s : Finset G), (Subgroup.closure ↑s).topologicalClosure = ⊤

The defining property of IsTopologicallyFinitelyGenerated, available to modules that only see the declaration and not its body.

theorem Set.Finite.isTopologicallyFinitelyGenerated {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {s : Set G} (hs : s.Finite) (hgen : (Subgroup.closure s).topologicalClosure = ⊤) : TauCeti.IsTopologicallyFinitelyGenerated G

A finite topological generating set, presented as a set rather than as a Finset, witnesses topological finite generation.

theorem TauCeti.isTopologicallyFinitelyGenerated_of_fg {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group.FG G] : IsTopologicallyFinitelyGenerated G

A finitely generated group, in any group topology, is topologically finitely generated: an algebraic generating set is a topological one. Via Group.fg_of_finite this covers the finite groups, and so all the finite quotients of a profinite group.

theorem TauCeti.topologicalClosure_closure_image_eq_top {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {s : Set G} (hs : (Subgroup.closure s).topologicalClosure = ⊤) {f : G →* H} (hf : Continuous ⇑f) (hf' : DenseRange ⇑f) : (Subgroup.closure (⇑f '' s)).topologicalClosure = ⊤

The image of a topological generating set under a continuous homomorphism with dense range is again a topological generating set.

theorem MonoidHom.ker_eq_topologicalClosure_normalClosure_insert_pow_of_orderOf_eq {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type u_3} [Group A] (χ : G →* A) (hker : IsClosed ↑χ.ker) {S : Set G} {a : G} {m : ℕ} (hgen : (Subgroup.closure (insert a S)).topologicalClosure = ⊤) (hS : ∀ s ∈ S, χ s = 1) (hm : 0 < m) (ha : orderOf (χ a) = m) : χ.ker = (Subgroup.normalClosure (insert (a ^ m) S)).topologicalClosure

The kernel of a character whose marked value has finite order. If the topological group G is topologically generated by insert a S, χ has closed kernel, kills S, and χ a has order m > 0, then ker χ is the closed normal closure of S together with a ^ m.

theorem MonoidHom.eqOn_topologicalClosure_closure {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M : Type u_3} [Monoid M] [TopologicalSpace M] [T2Space M] {s : Set G} {f g : G →* M} (hf : Continuous ⇑f) (hg : Continuous ⇑g) (hfg : Set.EqOn (⇑f) (⇑g) s) : Set.EqOn ⇑f ⇑g ↑(Subgroup.closure s).topologicalClosure

Two continuous homomorphisms into a Hausdorff monoid that agree on a set agree on the closed subgroup it generates.

theorem MonoidHom.eq_of_eqOn_of_topologicalClosure_closure_eq_top {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M : Type u_3} [Monoid M] [TopologicalSpace M] [T2Space M] {s : Set G} (hs : (Subgroup.closure s).topologicalClosure = ⊤) {f g : G →* M} (hf : Continuous ⇑f) (hg : Continuous ⇑g) (hfg : Set.EqOn (⇑f) (⇑g) s) : f = g

A continuous homomorphism out of a topological group is determined by its values on a topological generating set, provided the target is a Hausdorff monoid. This is the uniqueness half of every construction that defines a map on generators.

theorem MonoidHom.range_le_iff_of_topologicalClosure_closure_eq_top {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {s : Set G} (hs : (Subgroup.closure s).topologicalClosure = ⊤) {f : G →* H} (hf : Continuous ⇑f) {T : Subgroup H} (hT : IsClosed ↑T) : f.range ≤ T ↔ ∀ x ∈ s, f x ∈ T

The range of a continuous homomorphism lies in a closed subgroup exactly when a topological generating set of the source maps into it.

theorem MonoidHom.range_eq_topologicalClosure_of_topologicalClosure_closure_eq_top {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {s : Set G} (hs : (Subgroup.closure s).topologicalClosure = ⊤) {f : G →* H} (hf : Continuous ⇑f) (hf' : IsClosed ↑f.range) {T : Subgroup H} (h₁ : ∀ x ∈ s, f x ∈ T.topologicalClosure) (h₂ : T ≤ f.range) : f.range = T.topologicalClosure

The closed range of a continuous homomorphism is the closure of a subgroup T as soon as a topological generating set of the source maps into that closure and T lies in the range. Out of a compact group into a Hausdorff group the range is closed by MonoidHom.isClosed_range_of_continuous.

theorem TauCeti.IsTopologicallyFinitelyGenerated.of_denseRange {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (hG : IsTopologicallyFinitelyGenerated G) {f : G →* H} (hf : Continuous ⇑f) (hf' : DenseRange ⇑f) : IsTopologicallyFinitelyGenerated H

Topological finite generation passes along a continuous homomorphism with dense range.

theorem TauCeti.IsTopologicallyFinitelyGenerated.of_surjective {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (hG : IsTopologicallyFinitelyGenerated G) {f : G →* H} (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : IsTopologicallyFinitelyGenerated H

Topological finite generation passes to continuous surjective images.

theorem TauCeti.IsTopologicallyFinitelyGenerated.quotient {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hG : IsTopologicallyFinitelyGenerated G) (N : Subgroup G) [N.Normal] : IsTopologicallyFinitelyGenerated (G ⧸ N)

Topological finite generation passes to quotients by normal subgroups, closed or not.

theorem TauCeti.topologicalClosure_closure_sup_eq_top_iff {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {s : Set G} {K : Subgroup G} [K.Normal] : (Subgroup.closure s ⊔ K).topologicalClosure = ⊤ ↔ (Subgroup.closure (⇑(QuotientGroup.mk' K) '' s)).topologicalClosure = ⊤

Generation modulo a normal subgroup. A subset s together with a normal subgroup K topologically generates G exactly when the image of s topologically generates the quotient G ⧸ K. Neither compactness of G nor closedness of K is needed: the quotient map is open, so it exchanges preimages and closures.

theorem TauCeti.IsTopologicallyFinitelyGenerated.of_openSubgroup_of_finiteIndex {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hG : IsTopologicallyFinitelyGenerated G) (U : OpenSubgroup G) [(↑U).FiniteIndex] : IsTopologicallyFinitelyGenerated ↥↑U

An open finite-index subgroup of a topologically finitely generated group is topologically finitely generated.

theorem TauCeti.IsTopologicallyFinitelyGenerated.of_openSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsTopologicallyFinitelyGenerated G) (U : OpenSubgroup G) : IsTopologicallyFinitelyGenerated ↥↑U

An open subgroup of a topologically finitely generated compact topological group is topologically finitely generated.

theorem TauCeti.isTopologicallyFinitelyGenerated_congr {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) : IsTopologicallyFinitelyGenerated G ↔ IsTopologicallyFinitelyGenerated H

Topological finite generation is invariant under topological group isomorphism.

theorem MonoidHom.continuous_iff_isOpen_ker {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_3} [MulOneClass F] [TopologicalSpace F] [DiscreteTopology F] (f : G →* F) : Continuous ⇑f ↔ IsOpen ↑f.ker

A homomorphism from a topological group into a monoid carrying the discrete topology is continuous exactly when its kernel is open.

theorem MonoidHom.eq_of_eqOn_of_isOpen_ker {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {F : Type u_3} [Group F] {s : Set G} (hs : (Subgroup.closure s).topologicalClosure = ⊤) {f g : G →* F} (hf : IsOpen ↑f.ker) (hg : IsOpen ↑g.ker) (hfg : Set.EqOn (⇑f) (⇑g) s) : f = g

A homomorphism whose kernel is open is determined by its values on a topological generating set: the equalizer of two such homomorphisms contains the (open) intersection of their kernels, hence is open, hence closed, hence contains the whole group. The target carries no topology at all, which is what makes the statement usable for a target such as a permutation group that has no topology to hand; compare MonoidHom.eq_of_eqOn_of_topologicalClosure_closure_eq_top, which asks instead for continuity into a Hausdorff target.

theorem TauCeti.IsTopologicallyFinitelyGenerated.finite_monoidHom_isOpen_ker {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hG : IsTopologicallyFinitelyGenerated G) (F : Type u_3) [Group F] [Finite F] : Finite { f : G →* F // IsOpen ↑f.ker }

A topologically finitely generated group has few homomorphisms to a finite group. There are only finitely many homomorphisms with open kernel from a topologically finitely generated topological group to a fixed finite group, because such a homomorphism is determined by its values on a finite topological generating set.