Subgroups and topological closure

This file records how subgroup constructions interact with topological closure. It provides normality of the closure of a normal closure, the kernel criterion for a closed normal closure, and compatibility of multiplicative and additive subgroup closures. It also records that a dense subgroup meets every open subgroup densely. The closed cyclic subgroup closedZpowers x is topologically generated by its canonical element, without compactness assumptions.

Mathlib's theorem that the topological closure of a subgroup is closed is registered as an instance, so that the quotient of a topological group by the topological closure of a normal subgroup is found to be a Hausdorff topological group by instance search alone.

The closed normal closure of a set s, the topological closure of Subgroup.normalClosure s, is the least closed normal subgroup containing s (Subgroup.topologicalClosure_normalClosure_le_iff), and it is N itself when s is the carrier of a closed normal subgroup N (Subgroup.topologicalClosure_normalClosure_eq_self), for instance the kernel of a continuous homomorphism to a T1 monoid (ContinuousMonoidHom.topologicalClosure_normalClosure_ker). This is the fact behind the universal property of a group presented by generators and relators inside a category of topological groups.

A continuous homomorphism carries the topological closure of a subgroup into the topological closure of its image, and a closed subgroup containing the commutators ⁅A, B⁆ also contains the commutators ⁅A, closure B⁆. These are the two closure facts needed to run commutator calculus on closed subgroups that are given as topological closures, such as the terms of a lower central series of a profinite group.

Main results

• Subgroup.continuous_inclusion: the inclusion of a subgroup into a larger one is continuous.
• Subgroup.continuous_subgroupOf_codRestrict: the inclusion of U ⊓ D into U, presented using U.subgroupOf D, is continuous.
• Dense.denseRange_subgroupOf_codRestrict: a dense subgroup meets an open subgroup densely.
• Subgroup.index_comap_of_denseRange: the preimage of an open subgroup under a homomorphism with dense range has the same index.
• Subgroup.instIsClosedTopologicalClosure: the topological closure of a subgroup is closed.
• Subgroup.dense_iff_topologicalClosure_eq_top: a subgroup is dense exactly when its topological closure is everything; IsClosed.subgroup_topologicalClosure_eq: a closed subgroup is its own topological closure.
• Subgroup.dense_preimage_val_iff_le_topologicalClosure: a subgroup H ≤ K is dense in K exactly when K lies in the topological closure of H.
• TauCeti.instNormal_topologicalClosure_normalClosure: the closure of a normal closure is normal.
• TauCeti.topologicalClosure_normalClosure_le_ker: relators killed by a continuous map have closed normal closure in its kernel.
• Subgroup.topologicalClosure_normalClosure_le_iff: the closed normal closure is the least closed normal subgroup containing the set.
• Subgroup.topologicalClosure_normalClosure_eq_self: the closed normal closure of a closed normal subgroup is that subgroup.
• ContinuousMonoidHom.topologicalClosure_normalClosure_ker: the kernel of a continuous homomorphism to a T1 monoid is its own closed normal closure.
• Subgroup.toAddSubgroup_topologicalClosure: converting to an additive subgroup commutes with topological closure; Subgroup.dense_toAddSubgroup_iff: and preserves density.
• MonoidHom.map_topologicalClosure_le: a continuous homomorphism maps the topological closure of a subgroup into the topological closure of its image; MonoidHom.map_topologicalClosure: with equality when the subgroup's closure is compact and the target Hausdorff. Subgroup.isClosed_map says that images of compact subgroups in Hausdorff groups are closed.
• ContinuousMulEquiv.map_topologicalClosure_normalClosure: a topological group isomorphism carries the closed normal closure of a set onto the closed normal closure of its image.
• Subgroup.commutator_topologicalClosure_right_le: a closed subgroup containing ⁅A, B⁆ contains ⁅A, B.topologicalClosure⁆.
• Subgroup.topologicalClosure_commutator_le_of_forall_commutatorElement_mem: a closed normal subgroup containing the commutators of a topological generating set contains the closure of the commutator subgroup.
• Subgroup.instCompactSpace_of_isClosed: a closed subgroup of a compact group is compact.
• Subgroup.isCompact_sup_of_le_normalizer: the join of two compact subgroups, the first normalizing the second, is compact.
• TauCeti.closedZpowers, TauCeti.mem_closedZpowers, TauCeti.closedZpowers_le, and TauCeti.topologicallyGenerates_closedZpowers: the closed cyclic subgroup generated by an element, its canonical element, minimality among closed subgroups, and topological generation by that element.
• TauCeti.mem_or_inv_mul_mem_of_mem_topologicalClosure_zpowers: if a closed subgroup H contains u ^ 2, the closed subgroup generated by u lies in H ∪ u • H.
• TauCeti.topologicalClosure_iSup_range_mulSingle_eq_top: in a product of topological groups, the subgroup generated by the coordinate embeddings MonoidHom.mulSingle, that is the finitely supported elements, is dense; TauCeti.topologicalClosure_closure_range_mulSingle_eq_top: in a power ι → M of a group topologically generated by g, the elements Pi.mulSingle i g generate a dense subgroup.
• TauCeti.discreteTopology_of_conjAct_smul_eq: a conjugate g H g⁻¹ of a discrete subgroup H is discrete.

instance TauCeti.instNormal_topologicalClosure_normalClosure {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (s : Set G) : (Subgroup.normalClosure s).topologicalClosure.Normal

The closure of the normal closure of a set is a normal subgroup.

theorem TauCeti.topologicalClosure_normalClosure_le_ker {G : Type u_1} {H : Type u_2} [Group G] [Monoid H] [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace H] [T1Space H] {s : Set G} {f : G →ₜ* H} (hf : ∀ r ∈ s, f r = 1) : (Subgroup.normalClosure s).topologicalClosure ≤ f.ker

The closed normal closure of relators lies in the kernel of a continuous homomorphism that kills them.

theorem Subgroup.continuous_subgroupOf_codRestrict {G : Type u_1} [Group G] [TopologicalSpace G] (D U : Subgroup G) : Continuous ⇑((D.subtype.comp (U.subgroupOf D).subtype).codRestrict U ⋯)

The inclusion of U ⊓ D into U, where U ⊓ D is presented as the subgroup U.subgroupOf D of D, is continuous.

theorem Dense.denseRange_subgroupOf_codRestrict {G : Type u_1} [Group G] [TopologicalSpace G] {D U : Subgroup G} (hD : Dense ↑D) (hU : IsOpen ↑U) : DenseRange ⇑((D.subtype.comp (U.subgroupOf D).subtype).codRestrict U ⋯)

A dense subgroup meets an open subgroup densely. If D is dense and U is open, the inclusion of U ⊓ D, presented as the subgroup U.subgroupOf D of D, into U has dense range.

theorem Subgroup.index_comap_of_denseRange {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] {G' : Type u_2} [Group G'] {f : G' →* G} (hf : DenseRange ⇑f) {U : Subgroup G} (hU : IsOpen ↑U) : (comap f U).index = U.index

An open subgroup has the same index in a dense subgroup. If f : G' →* G has dense range and U is an open subgroup of G, then the preimage of U has the same index in G' as U has in G: the range of f meets every coset of U, since the cosets are open.

The proof is adapted from Mathlib's Subgroup.index_comap_of_surjective.

theorem Subgroup.continuous_inclusion {G : Type u_1} [Group G] [TopologicalSpace G] {H K : Subgroup G} (h : H ≤ K) : Continuous ⇑(inclusion h)

The inclusion of a subgroup into a larger subgroup is continuous.

instance Subgroup.instIsClosedTopologicalClosure {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (s : Subgroup G) : IsClosed ↑s.topologicalClosure

The topological closure of a subgroup is closed.

theorem Subgroup.dense_iff_topologicalClosure_eq_top {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {s : Subgroup G} : Dense ↑s ↔ s.topologicalClosure = ⊤

A subgroup is dense exactly when its topological closure is the whole group.

theorem AddSubgroup.dense_iff_topologicalClosure_eq_top {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {s : AddSubgroup G} : Dense ↑s ↔ s.topologicalClosure = ⊤

An additive subgroup is dense exactly when its topological closure is the whole group.

theorem IsClosed.subgroup_topologicalClosure_eq {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {s : Subgroup G} (hs : IsClosed ↑s) : s.topologicalClosure = s

A closed subgroup is its own topological closure.

theorem IsClosed.addSubgroup_topologicalClosure_eq {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {s : AddSubgroup G} (hs : IsClosed ↑s) : s.topologicalClosure = s

A closed additive subgroup is its own topological closure.

theorem Subgroup.dense_preimage_val_iff_le_topologicalClosure {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H K : Subgroup G} (h : H ≤ K) : Dense (Subtype.val ⁻¹' ↑H) ↔ K ≤ H.topologicalClosure

A subgroup H ≤ K is dense in K exactly when K lies in the topological closure of H.

instance Subgroup.instCompactSpace_of_isClosed {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] (N : Subgroup G) [IsClosed ↑N] : CompactSpace ↥N

A closed subgroup of a compact group is compact.

theorem Subgroup.isCompact_sup_of_le_normalizer {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] {H N : Subgroup G} (hH : IsCompact ↑H) (hN : IsCompact ↑N) (hHN : H ≤ normalizer ↑N) : IsCompact ↑(H ⊔ N)

In a group with continuous multiplication, the join of two compact subgroups H and N with H normalizing N is compact. In a Hausdorff group it is therefore closed.

theorem AddSubgroup.isCompact_sup_of_le_normalizer {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] {H N : AddSubgroup G} (hH : IsCompact ↑H) (hN : IsCompact ↑N) (hHN : H ≤ normalizer ↑N) : IsCompact ↑(H ⊔ N)

In a group with continuous addition, the join of two compact additive subgroups H and N with H normalizing N is compact. In a Hausdorff group it is therefore closed.

@[simp]

theorem Subgroup.topologicalClosure_normalClosure_le_iff {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {s : Set G} {N : Subgroup G} [N.Normal] (hN : IsClosed ↑N) : (normalClosure s).topologicalClosure ≤ N ↔ s ⊆ ↑N

A closed normal subgroup contains the closed normal closure of s exactly when it contains s: the closed normal closure is the least closed normal subgroup containing s.

theorem Subgroup.topologicalClosure_normalClosure_eq_self {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (hN : IsClosed ↑N) : (normalClosure ↑N).topologicalClosure = N

The closed normal closure of the carrier of a closed normal subgroup is that subgroup.

theorem ContinuousMonoidHom.topologicalClosure_normalClosure_ker {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Monoid H] [TopologicalSpace H] [T1Space H] (φ : G →ₜ* H) : (Subgroup.normalClosure ↑(↑φ).ker).topologicalClosure = (↑φ).ker

The kernel of a continuous homomorphism to a T1 monoid is a closed normal subgroup, so it is its own closed normal closure.

@[simp]

theorem Subgroup.toAddSubgroup_topologicalClosure {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (S : Subgroup G) : toAddSubgroup S.topologicalClosure = (toAddSubgroup S).topologicalClosure

Converting a subgroup to an additive subgroup commutes with topological closure.

theorem Subgroup.dense_toAddSubgroup_iff {G : Type u_1} [Group G] [TopologicalSpace G] (S : Subgroup G) : Dense ↑(toAddSubgroup S) ↔ Dense ↑S

Converting a subgroup to an additive subgroup preserves density.

theorem MonoidHom.map_topologicalClosure_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) (S : Subgroup G) : Subgroup.map f S.topologicalClosure ≤ (Subgroup.map f S).topologicalClosure

A continuous homomorphism maps the topological closure of a subgroup into the topological closure of its image.

theorem Subgroup.isClosed_map {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Group H] [TopologicalSpace H] [T2Space H] {S : Subgroup G} (hS : IsCompact ↑S) (f : G →* H) (hf : Continuous ⇑f) : IsClosed ↑(map f S)

A continuous homomorphism to a Hausdorff group maps compact subgroups to closed subgroups.

theorem MonoidHom.map_topologicalClosure {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H] (f : G →* H) (hf : Continuous ⇑f) (S : Subgroup G) (hS : IsCompact ↑S.topologicalClosure) : Subgroup.map f S.topologicalClosure = (Subgroup.map f S).topologicalClosure

A continuous homomorphism to a Hausdorff group maps a subgroup's compact topological closure onto the topological closure of its image.

@[simp]

theorem ContinuousMulEquiv.map_topologicalClosure_normalClosure {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (α : G ≃ₜ* H) (s : Set G) : Subgroup.map (↑↑α) (Subgroup.normalClosure s).topologicalClosure = (Subgroup.normalClosure (⇑α '' s)).topologicalClosure

A topological group isomorphism carries the closed normal closure of a set onto the closed normal closure of its image.

theorem Subgroup.commutator_topologicalClosure_right_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A B N : Subgroup G} (hN : IsClosed ↑N) (h : ⁅A, B⁆ ≤ N) : ⁅A, B.topologicalClosure⁆ ≤ N

A closed subgroup containing the commutators ⁅A, B⁆ contains the commutators ⁅A, B.topologicalClosure⁆.

theorem Subgroup.topologicalClosure_commutator_le_of_forall_commutatorElement_mem {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {s : Set G} (hs : (closure s).topologicalClosure = ⊤) {N : Subgroup G} [N.Normal] (hN : IsClosed ↑N) (h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ ∈ N) : (_root_.commutator G).topologicalClosure ≤ N

Commutators of topological generators generate the commutators. If s topologically generates G and N is a closed normal subgroup containing the commutators of the elements of s, then N contains the closure of the commutator subgroup: the quotient G ⧸ N is topologically generated by pairwise commuting elements, hence commutative.

def TauCeti.closedZpowers {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x : G) : Subgroup G

The closed cyclic subgroup generated by x.

Equations

• TauCeti.closedZpowers x = (Subgroup.zpowers x).topologicalClosure

theorem TauCeti.closedZpowers_def {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x : G) : closedZpowers x = (Subgroup.zpowers x).topologicalClosure

The closed cyclic subgroup is the topological closure of the integer powers. This lemma is not a simp rule, so simplification preserves the closed cyclic subgroup API.

instance TauCeti.isClosed_closedZpowers {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x : G) : IsClosed ↑(closedZpowers x)

The closed cyclic subgroup is closed.

instance TauCeti.instIsMulCommutative_closedZpowers {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] (x : G) : IsMulCommutative ↥(closedZpowers x)

The closed cyclic subgroup of a Hausdorff topological group is commutative.

@[simp]

theorem TauCeti.mem_closedZpowers {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x : G) : x ∈ closedZpowers x

An element belongs to its closed cyclic subgroup.

@[simp]

theorem TauCeti.closedZpowers_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {x : G} {H : Subgroup G} (hH : IsClosed ↑H) : closedZpowers x ≤ H ↔ x ∈ H

The closed cyclic subgroup generated by x lies in a closed subgroup exactly when that subgroup contains x.

theorem TauCeti.topologicallyGenerates_closedZpowers {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x : G) : (Subgroup.zpowers ⟨x, ⋯⟩).topologicalClosure = ⊤

The canonical element topologically generates its closed cyclic subgroup.

theorem TauCeti.mem_or_inv_mul_mem_of_mem_topologicalClosure_zpowers {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (u : G) (H : Subgroup G) (hH : IsClosed ↑H) (hu : u ^ 2 ∈ H) {x : G} (hx : x ∈ (Subgroup.zpowers u).topologicalClosure) : x ∈ H ∨ u⁻¹ * x ∈ H

If a closed subgroup H contains u ^ 2, then the closed subgroup topologically generated by u is contained in H ∪ u • H: the even powers of u lie in H, the odd ones in u • H, and this closed union contains their closure.

Products of topological groups

theorem TauCeti.topologicalClosure_iSup_range_mulSingle_eq_top {ι : Type u_1} [DecidableEq ι] {M : ι → Type u_2} [(i : ι) → Group (M i)] [(i : ι) → TopologicalSpace (M i)] [∀ (i : ι), IsTopologicalGroup (M i)] : (⨆ (i : ι), (MonoidHom.mulSingle M i).range).topologicalClosure = ⊤

The coordinate embeddings generate a dense subgroup of a product of topological groups. The subgroup generated by the images of the embeddings MonoidHom.mulSingle M i, that is the elements of the product supported at finitely many coordinates, is dense.

theorem TauCeti.topologicalClosure_iSup_range_single_eq_top {ι : Type u_1} [DecidableEq ι] {M : ι → Type u_2} [(i : ι) → AddGroup (M i)] [(i : ι) → TopologicalSpace (M i)] [∀ (i : ι), IsTopologicalAddGroup (M i)] : (⨆ (i : ι), (AddMonoidHom.single M i).range).topologicalClosure = ⊤

The coordinate embeddings generate a dense subgroup of a product of topological additive groups. The additive subgroup generated by the images of the embeddings AddMonoidHom.single M i, that is the elements of the product supported at finitely many coordinates, is dense.

theorem TauCeti.topologicalClosure_closure_range_mulSingle_eq_top {ι : Type u_1} [DecidableEq ι] {M : Type u_2} [Group M] [TopologicalSpace M] [IsTopologicalGroup M] {g : M} (hg : (Subgroup.zpowers g).topologicalClosure = ⊤) : (Subgroup.closure (Set.range fun (i : ι) => Pi.mulSingle i g)).topologicalClosure = ⊤

A topological generator of a group topologically generates each of its powers, coordinatewise. If g topologically generates the topological group M, that is the subgroup it generates is dense, the elements Pi.mulSingle i g of the power ι → M, supported at a single coordinate, generate a dense subgroup.

theorem TauCeti.topologicalClosure_closure_range_single_eq_top {ι : Type u_1} [DecidableEq ι] {M : Type u_2} [AddGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] {g : M} (hg : (AddSubgroup.zmultiples g).topologicalClosure = ⊤) : (AddSubgroup.closure (Set.range fun (i : ι) => Pi.single i g)).topologicalClosure = ⊤

A topological generator of an additive group topologically generates each of its powers, coordinatewise. If g topologically generates the topological additive group M, that is the additive subgroup it generates is dense, the elements Pi.single i g of the power ι → M, supported at a single coordinate, generate a dense additive subgroup.

theorem TauCeti.discreteTopology_of_conjAct_smul_eq {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {H H' : Subgroup G} {g : G} [DiscreteTopology ↥H] (h : ConjAct.toConjAct g • H = H') : DiscreteTopology ↥H'

Conjugation preserves discreteness: if H' is the conjugate g H g⁻¹ of a discrete subgroup H of a group with continuous translations, then H' is discrete, since x ↦ g⁻¹ x g embeds it in H.