Subgroups of topological groups

Topological group structures on subgroups, topological closures and connected components of subgroups, and properly discontinuous actions by closed normal subgroups.

instance Subgroup.instIsTopologicalGroupSubtypeMem {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (S : Subgroup G) : IsTopologicalGroup ↥S

instance AddSubgroup.instIsTopologicalAddGroupSubtypeMem {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (S : AddSubgroup G) : IsTopologicalAddGroup ↥S

def Subgroup.topologicalClosure {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (s : Subgroup G) : Subgroup G

The (topological-space) closure of a subgroup of a topological group is itself a subgroup.

def AddSubgroup.topologicalClosure {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (s : AddSubgroup G) : AddSubgroup G

The (topological-space) closure of an additive subgroup of an additive topological group is itself an additive subgroup.

@[simp]

theorem Subgroup.topologicalClosure_coe {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s : Subgroup G} : ↑s.topologicalClosure = _root_.closure ↑s

@[simp]

theorem AddSubgroup.topologicalClosure_coe {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s : AddSubgroup G} : ↑s.topologicalClosure = _root_.closure ↑s

theorem Subgroup.le_topologicalClosure {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (s : Subgroup G) : s ≤ s.topologicalClosure

theorem AddSubgroup.le_topologicalClosure {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (s : AddSubgroup G) : s ≤ s.topologicalClosure

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

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

theorem Subgroup.topologicalClosure_minimal {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (s : Subgroup G) {t : Subgroup G} (h : s ≤ t) (ht : IsClosed ↑t) : s.topologicalClosure ≤ t

theorem AddSubgroup.topologicalClosure_minimal {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (s : AddSubgroup G) {t : AddSubgroup G} (h : s ≤ t) (ht : IsClosed ↑t) : s.topologicalClosure ≤ t

theorem Subgroup.topologicalClosure_mono {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {s t : Subgroup G} (h : s ≤ t) : s.topologicalClosure ≤ t.topologicalClosure

theorem AddSubgroup.topologicalClosure_mono {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {s t : AddSubgroup G} (h : s ≤ t) : s.topologicalClosure ≤ t.topologicalClosure

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

theorem DenseRange.topologicalClosure_map_addSubgroup {G : Type u_1} {H : Type u_2} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [AddGroup H] [TopologicalSpace H] [IsTopologicalAddGroup H] {f : G →+ H} (hf : Continuous ⇑f) (hf' : DenseRange ⇑f) {s : AddSubgroup G} (hs : s.topologicalClosure = ⊤) : (AddSubgroup.map f s).topologicalClosure = ⊤

theorem Subgroup.is_normal_topologicalClosure {G : Type u_3} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] : N.topologicalClosure.Normal

The topological closure of a normal subgroup is normal.

theorem AddSubgroup.is_normal_topologicalClosure {G : Type u_3} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (N : AddSubgroup G) [N.Normal] : N.topologicalClosure.Normal

The topological closure of a normal additive subgroup is normal.

theorem mul_mem_connectedComponent_one {G : Type u_3} [TopologicalSpace G] [MulOneClass G] [ContinuousMul G] {g h : G} (hg : g ∈ connectedComponent 1) (hh : h ∈ connectedComponent 1) : g * h ∈ connectedComponent 1

theorem add_mem_connectedComponent_zero {G : Type u_3} [TopologicalSpace G] [AddZeroClass G] [ContinuousAdd G] {g h : G} (hg : g ∈ connectedComponent 0) (hh : h ∈ connectedComponent 0) : g + h ∈ connectedComponent 0

theorem inv_mem_connectedComponent_one {G : Type u_3} [TopologicalSpace G] [DivisionMonoid G] [ContinuousInv G] {g : G} (hg : g ∈ connectedComponent 1) : g⁻¹ ∈ connectedComponent 1

theorem neg_mem_connectedComponent_zero {G : Type u_3} [TopologicalSpace G] [SubtractionMonoid G] [ContinuousNeg G] {g : G} (hg : g ∈ connectedComponent 0) : -g ∈ connectedComponent 0

def Subgroup.connectedComponentOfOne (G : Type u_3) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : Subgroup G

The connected component of 1 is a subgroup of G.

def AddSubgroup.connectedComponentOfZero (G : Type u_3) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : AddSubgroup G

The connected component of 0 is a subgroup of G.

instance Subgroup.isMulCommutative_topologicalClosure {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [T2Space G] (s : Subgroup G) [IsMulCommutative ↥s] : IsMulCommutative ↥s.topologicalClosure

If a subgroup of a topological group is commutative, then so is its topological closure.

instance AddSubgroup.isAddCommutative_topologicalClosure {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [T2Space G] (s : AddSubgroup G) [IsAddCommutative ↥s] : IsAddCommutative ↥s.topologicalClosure

If a subgroup of an additive topological group is commutative, then so is its topological closure.

@[reducible, inline, deprecated Subgroup.isMulCommutative_topologicalClosure (since := "2026-07-29")]

abbrev Subgroup.commGroupTopologicalClosure {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [T2Space G] (s : Subgroup G) (hs : ∀ (x y : ↥s), x * y = y * x) : CommGroup ↥s.topologicalClosure

If a subgroup of a topological group is commutative, then so is its topological closure.

See note [reducible non-instances].

@[reducible, inline, deprecated AddSubgroup.isAddCommutative_topologicalClosure (since := "2026-07-29")]

abbrev AddSubgroup.addCommGroupTopologicalClosure {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [T2Space G] (s : AddSubgroup G) (hs : ∀ (x y : ↥s), x + y = y + x) : AddCommGroup ↥s.topologicalClosure

If a subgroup of an additive topological group is commutative, then so is its topological closure.

See note [reducible non-instances].

theorem Subgroup.coe_topologicalClosure_bot (G : Type u_1) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : ↑⊥.topologicalClosure = _root_.closure {1}

theorem AddSubgroup.coe_topologicalClosure_bot (G : Type u_1) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : ↑⊥.topologicalClosure = _root_.closure {0}

theorem Subgroup.properlyDiscontinuousSMul_of_tendsto_cofinite {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (S : Subgroup G) (hS : Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G)) : ProperlyDiscontinuousSMul (↥S) G

A subgroup S of a topological group G acts on G properly discontinuously on the left, if it is discrete in the sense that S ∩ K is finite for all compact K. (See also DiscreteTopology.)

theorem AddSubgroup.properlyDiscontinuousVAdd_of_tendsto_cofinite {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (S : AddSubgroup G) (hS : Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G)) : ProperlyDiscontinuousVAdd (↥S) G

A subgroup S of an additive topological group G acts on G properly discontinuously on the left, if it is discrete in the sense that S ∩ K is finite for all compact K. (See also DiscreteTopology.)

theorem Subgroup.properlyDiscontinuousSMul_opposite_of_tendsto_cofinite {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (S : Subgroup G) (hS : Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G)) : ProperlyDiscontinuousSMul (↥S.op) G

A subgroup S of a topological group G acts on G properly discontinuously on the right, if it is discrete in the sense that S ∩ K is finite for all compact K. (See also DiscreteTopology.)

If G is Hausdorff, this can be combined with t2Space_of_properlyDiscontinuousSMul_of_t2Space to show that the quotient group G ⧸ S is Hausdorff.

theorem AddSubgroup.properlyDiscontinuousVAdd_opposite_of_tendsto_cofinite {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (S : AddSubgroup G) (hS : Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G)) : ProperlyDiscontinuousVAdd (↥S.op) G

A subgroup S of an additive topological group G acts on G properly discontinuously on the right, if it is discrete in the sense that S ∩ K is finite for all compact K. (See also DiscreteTopology.)

If G is Hausdorff, this can be combined with t2Space_of_properlyDiscontinuousVAdd_of_t2Space to show that the quotient group G ⧸ S is Hausdorff.