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
: ThenormalCore
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
The type of closed subgroups of a topological group.
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
:
Type u
The type of closed subgroups of an additive topological group.
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' := ⋯ }
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]
:
Equations
instance
ClosedSubgroup.instSemilatticeInfClosedSubgroup
(G : Type u)
[Group G]
[TopologicalSpace G]
:
Equations
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)
:
IsOpen ↑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)
:
IsOpen ↑H