Documentation

Mathlib.Topology.Algebra.ClosedSubgroup

Closed subgroups of a topological group #

This files builds the SemilatticeInf ClosedSubgroup G of closed subgroups in a topological group G, and its additive version ClosedAddSubgroup.

Main definitions and results #

normalCore_isClosed : The normalCore of a closed subgroup is closed.
finindex_closedSubgroup_isOpen : A closed subgroup with finite index is open.

structure ClosedSubgroup (G : Type u) [Group G] [TopologicalSpace G] extends Subgroup , Submonoid , Subsemigroup :

The type of closed subgroups of a topological group.

Instances For

theorem ClosedSubgroup.ext {G : Type u} :

∀ {inst : Group G} {inst_1 : TopologicalSpace G} {x y : ClosedSubgroup G}, (↑x).carrier = (↑y).carrier → x = y

theorem ClosedSubgroup.isClosed' {G : Type u} [Group G] [TopologicalSpace G] (self : ClosedSubgroup G) :

IsClosed (↑self).carrier

structure ClosedAddSubgroup (G : Type u) [AddGroup G] [TopologicalSpace G] extends AddSubgroup , AddSubmonoid , AddSubsemigroup :

The type of closed subgroups of an additive topological group.

Instances For

theorem ClosedAddSubgroup.ext {G : Type u} :

∀ {inst : AddGroup G} {inst_1 : TopologicalSpace G} {x y : ClosedAddSubgroup G}, (↑x).carrier = (↑y).carrier → x = y

theorem ClosedAddSubgroup.isClosed' {G : Type u} [AddGroup G] [TopologicalSpace G] (self : ClosedAddSubgroup G) :

IsClosed (↑self).carrier

theorem ClosedSubgroup.toSubgroup_injective {G : Type u} [Group G] [TopologicalSpace G] :

Function.Injective ClosedSubgroup.toSubgroup

theorem ClosedAddSubgroup.toAddSubgroup_injective {G : Type u} [AddGroup G] [TopologicalSpace G] :

Function.Injective ClosedAddSubgroup.toAddSubgroup

instance ClosedSubgroup.instSetLike (G : Type u) [Group G] [TopologicalSpace G] :

SetLike (ClosedSubgroup G) G

Equations

ClosedSubgroup.instSetLike G = { coe := fun (U : ClosedSubgroup G) => ↑↑U, coe_injective' := ⋯ }

instance ClosedAddSubgroup.instSetLike (G : Type u) [AddGroup G] [TopologicalSpace G] :

SetLike (ClosedAddSubgroup G) G

Equations

ClosedAddSubgroup.instSetLike G = { coe := fun (U : ClosedAddSubgroup G) => ↑↑U, coe_injective' := ⋯ }

instance ClosedSubgroup.instSubgroupClass (G : Type u) [Group G] [TopologicalSpace G] :

SubgroupClass (ClosedSubgroup G) G

Equations

⋯ = ⋯

instance ClosedAddSubgroup.instAddSubgroupClass (G : Type u) [AddGroup G] [TopologicalSpace G] :

AddSubgroupClass (ClosedAddSubgroup G) G

Equations

⋯ = ⋯

instance ClosedSubgroup.instCoeSubgroup (G : Type u) [Group G] [TopologicalSpace G] :

Coe (ClosedSubgroup G) (Subgroup G)

Equations

ClosedSubgroup.instCoeSubgroup G = { coe := ClosedSubgroup.toSubgroup }

instance ClosedAddSubgroup.instCoeAddSubgroup (G : Type u) [AddGroup G] [TopologicalSpace G] :

Coe (ClosedAddSubgroup G) (AddSubgroup G)

Equations

ClosedAddSubgroup.instCoeAddSubgroup G = { coe := ClosedAddSubgroup.toAddSubgroup }

instance ClosedSubgroup.instInfClosedSubgroup (G : Type u) [Group G] [TopologicalSpace G] :

Inf (ClosedSubgroup G)

Equations

ClosedSubgroup.instInfClosedSubgroup G = { inf := fun (U V : ClosedSubgroup G) => { toSubgroup := ↑U ⊓ ↑V, isClosed' := ⋯ } }

instance ClosedAddSubgroup.instInfClosedAddSubgroup (G : Type u) [AddGroup G] [TopologicalSpace G] :

Inf (ClosedAddSubgroup G)

Equations

ClosedAddSubgroup.instInfClosedAddSubgroup G = { inf := fun (U V : ClosedAddSubgroup G) => { toAddSubgroup := ↑U ⊓ ↑V, isClosed' := ⋯ } }

instance ClosedSubgroup.instSemilatticeInfClosedSubgroup (G : Type u) [Group G] [TopologicalSpace G] :

SemilatticeInf (ClosedSubgroup G)

Equations

ClosedSubgroup.instSemilatticeInfClosedSubgroup G = Function.Injective.semilatticeInf SetLike.coe ⋯ ⋯

instance ClosedAddSubgroup.instSemilatticeInfClosedAddSubgroup (G : Type u) [AddGroup G] [TopologicalSpace G] :

SemilatticeInf (ClosedAddSubgroup G)

Equations

ClosedAddSubgroup.instSemilatticeInfClosedAddSubgroup G = Function.Injective.semilatticeInf SetLike.coe ⋯ ⋯

instance ClosedSubgroup.instCompactSpaceSubtypeMem (G : Type u) [Group G] [TopologicalSpace G] [CompactSpace G] (H : ClosedSubgroup G) :

CompactSpace ↥H

Equations

⋯ = ⋯

instance ClosedAddSubgroup.instCompactSpaceSubtypeMem (G : Type u) [AddGroup G] [TopologicalSpace G] [CompactSpace G] (H : ClosedAddSubgroup G) :

CompactSpace ↥H

Equations

⋯ = ⋯

theorem Subgroup.normalCore_isClosed {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (H : Subgroup G) (h : IsClosed ↑H) :

IsClosed ↑H.normalCore

theorem Subgroup.isOpen_of_isClosed_of_finiteIndex {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (H : Subgroup G) [H.FiniteIndex] (h : IsClosed ↑H) :

theorem AddSubgroup.isOpen_of_isClosed_of_finiteIndex {G : Type u} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (H : AddSubgroup G) [H.FiniteIndex] (h : IsClosed ↑H) :