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.

theorem ClosedSubgroup.ext_iff {G : Type u} :

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

theorem ClosedSubgroup.ext {G : Type u} :

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

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

The type of closed subgroups of a topological group.

carrier : Set G
mul_mem' : ∀ {a b : G}, a ∈ (↑self).carrier → b ∈ (↑self).carrier → a * b ∈ (↑self).carrier
one_mem' : 1 ∈ (↑self).carrier
inv_mem' : ∀ {x : G}, x ∈ (↑self).carrier → x⁻¹ ∈ (↑self).carrier
isClosed' : IsClosed (↑self).carrier

Instances For

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

IsClosed (↑self).carrier

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.ext_iff {G : Type u} :

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

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

The type of closed subgroups of an additive topological group.

carrier : Set G
add_mem' : ∀ {a b : G}, a ∈ (↑self).carrier → b ∈ (↑self).carrier → a + b ∈ (↑self).carrier
zero_mem' : 0 ∈ (↑self).carrier
neg_mem' : ∀ {x : G}, x ∈ (↑self).carrier → -x ∈ (↑self).carrier
isClosed' : IsClosed (↑self).carrier

Instances For

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

IsClosed (↑self).carrier

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

Function.Injective ClosedAddSubgroup.toAddSubgroup

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

Function.Injective ClosedSubgroup.toSubgroup

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.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.instAddSubgroupClass (G : Type u) [AddGroup G] [TopologicalSpace G] :

AddSubgroupClass (ClosedAddSubgroup G) G

Equations

⋯ = ⋯

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

SubgroupClass (ClosedSubgroup G) G

Equations

⋯ = ⋯

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

Coe (ClosedAddSubgroup G) (AddSubgroup G)

Equations

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

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

Coe (ClosedSubgroup G) (Subgroup G)

Equations

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

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.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.instSemilatticeInfClosedAddSubgroup (G : Type u) [AddGroup G] [TopologicalSpace G] :

SemilatticeInf (ClosedAddSubgroup G)

Equations

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

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

SemilatticeInf (ClosedSubgroup G)

Equations

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

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

CompactSpace ↥H

Equations

⋯ = ⋯

instance ClosedSubgroup.instCompactSpaceSubtypeMem (G : Type u) [Group G] [TopologicalSpace G] [CompactSpace G] (H : ClosedSubgroup 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 AddSubgroup.isOpen_of_isClosed_of_finiteIndex {G : Type u} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (H : AddSubgroup G) [H.FiniteIndex] (h : IsClosed ↑H) :

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