Documentation

Mathlib.Topology.Algebra.Group.Quotient

Topology on the quotient group #

In this file we define topology on G ⧸ N, where N is a subgroup of G, and prove basic properties of this topology.

source
@[implicit_reducible]
instance QuotientGroup.instTopologicalSpace {G : Type u_1} [TopologicalSpace G] [Group G] (N : Subgroup G) :
TopologicalSpace (G ⧸ N)
Equations
source
@[implicit_reducible]
instance QuotientAddGroup.instTopologicalSpace {G : Type u_1} [TopologicalSpace G] [AddGroup G] (N : AddSubgroup G) :
TopologicalSpace (G ⧸ N)
Equations
source
instance QuotientGroup.instCompactSpaceQuotientSubgroup {G : Type u_1} [TopologicalSpace G] [Group G] [CompactSpace G] (N : Subgroup G) :
CompactSpace (G ⧸ N)
source
instance QuotientAddGroup.instCompactSpaceQuotientAddSubgroup {G : Type u_1} [TopologicalSpace G] [AddGroup G] [CompactSpace G] (N : AddSubgroup G) :
CompactSpace (G ⧸ N)
source
theorem QuotientGroup.isQuotientMap_mk {G : Type u_1} [TopologicalSpace G] [Group G] (N : Subgroup G) :
Topology.IsQuotientMap mk
source
theorem QuotientAddGroup.isQuotientMap_mk {G : Type u_1} [TopologicalSpace G] [AddGroup G] (N : AddSubgroup G) :
Topology.IsQuotientMap mk
source
theorem QuotientGroup.continuous_mk {G : Type u_1} [TopologicalSpace G] [Group G] {N : Subgroup G} :
Continuous mk
source
theorem QuotientAddGroup.continuous_mk {G : Type u_1} [TopologicalSpace G] [AddGroup G] {N : AddSubgroup G} :
Continuous mk
source
theorem QuotientGroup.isOpenMap_coe {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] {N : Subgroup G} :
IsOpenMap mk
source
theorem QuotientAddGroup.isOpenMap_coe {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] {N : AddSubgroup G} :
IsOpenMap mk
source
theorem QuotientGroup.isOpenQuotientMap_mk {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] {N : Subgroup G} :
IsOpenQuotientMap mk
source
theorem QuotientAddGroup.isOpenQuotientMap_mk {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] {N : AddSubgroup G} :
IsOpenQuotientMap mk
source
@[simp]
theorem QuotientGroup.dense_preimage_mk {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] {N : Subgroup G} {s : Set (G ⧸ N)} :
Dense (mk ⁻¹' s) ↔ Dense s
source
@[simp]
theorem QuotientAddGroup.dense_preimage_mk {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] {N : AddSubgroup G} {s : Set (G ⧸ N)} :
Dense (mk ⁻¹' s) ↔ Dense s
source
theorem QuotientGroup.dense_image_mk {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] {N : Subgroup G} {s : Set G} :
Dense (mk '' s) ↔ Dense (s * ↑N)
source
theorem QuotientAddGroup.dense_image_mk {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] {N : AddSubgroup G} {s : Set G} :
Dense (mk '' s) ↔ Dense (s + ↑N)
source
instance QuotientGroup.instContinuousSMul {G : Type u_2} [Group G] [TopologicalSpace G] [ContinuousMul G] {N : Subgroup G} :
ContinuousSMul G (G ⧸ N)
source
instance QuotientAddGroup.instContinuousVAdd {G : Type u_2} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] {N : AddSubgroup G} :
ContinuousVAdd G (G ⧸ N)
source
instance QuotientGroup.instContinuousConstSMul {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] {N : Subgroup G} :
ContinuousConstSMul G (G ⧸ N)
source
instance QuotientAddGroup.instContinuousConstVAdd {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] {N : AddSubgroup G} :
ContinuousConstVAdd G (G ⧸ N)
source
theorem QuotientGroup.t1Space_iff {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] {N : Subgroup G} :
T1Space (G ⧸ N) ↔ IsClosed ↑N
source
theorem QuotientAddGroup.t1Space_iff {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] {N : AddSubgroup G} :
T1Space (G ⧸ N) ↔ IsClosed ↑N
source
theorem QuotientGroup.discreteTopology_iff {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] {N : Subgroup G} :
DiscreteTopology (G ⧸ N) ↔ IsOpen ↑N
source
theorem QuotientAddGroup.discreteTopology_iff {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] {N : AddSubgroup G} :
DiscreteTopology (G ⧸ N) ↔ IsOpen ↑N
source
instance QuotientGroup.instT1Space {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] {N : Subgroup G} [hN : IsClosed ↑N] :
T1Space (G ⧸ N)

The quotient of a topological group G by a closed subgroup N is T1.

When G is normal, this implies (because G ⧸ N is a topological group) that the quotient is T3 (see QuotientGroup.instT3Space).

Back to the general case, we will show later that the quotient is in fact T2 since N acts on G properly.

source
instance QuotientAddGroup.instT1Space {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] {N : AddSubgroup G} [hN : IsClosed ↑N] :
T1Space (G ⧸ N)

The quotient of a topological additive group G by a closed subgroup N is T1.

When G is normal, this implies (because G ⧸ N is a topological additive group) that the quotient is T3 (see QuotientAddGroup.instT3Space).

Back to the general case, we will show later that the quotient is in fact T2 since N acts on G properly.

source
theorem QuotientGroup.discreteTopology {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] {N : Subgroup G} (hN : IsOpen ↑N) :
DiscreteTopology (G ⧸ N)
source
theorem QuotientAddGroup.discreteTopology {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] {N : AddSubgroup G} (hN : IsOpen ↑N) :
DiscreteTopology (G ⧸ N)
source
instance QuotientGroup.instLocallyCompactSpace {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] [LocallyCompactSpace G] (N : Subgroup G) :
LocallyCompactSpace (G ⧸ N)

A quotient of a locally compact group is locally compact.

source
instance QuotientAddGroup.instLocallyCompactSpace {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] [LocallyCompactSpace G] (N : AddSubgroup G) :
LocallyCompactSpace (G ⧸ N)
source
theorem QuotientGroup.nhds_eq {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (N : Subgroup G) (x : G) :
nhds ↑x = Filter.map mk (nhds x)

Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient.

source
theorem QuotientAddGroup.nhds_eq {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] (N : AddSubgroup G) (x : G) :
nhds ↑x = Filter.map mk (nhds x)

Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient.

source
instance QuotientGroup.instFirstCountableTopology {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (N : Subgroup G) [FirstCountableTopology G] :
FirstCountableTopology (G ⧸ N)
source
instance QuotientAddGroup.instFirstCountableTopology {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] (N : AddSubgroup G) [FirstCountableTopology G] :
FirstCountableTopology (G ⧸ N)
source
instance QuotientGroup.instSecondCountableTopology {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] (N : Subgroup G) [SecondCountableTopology G] :
SecondCountableTopology (G ⧸ N)

The quotient of a second countable topological group by a subgroup is second countable.

source
instance QuotientAddGroup.instSecondCountableTopology {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] (N : AddSubgroup G) [SecondCountableTopology G] :
SecondCountableTopology (G ⧸ N)

The quotient of a second countable additive topological group by a subgroup is second countable.

source
instance QuotientGroup.instIsTopologicalGroup {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] :
IsTopologicalGroup (G ⧸ N)
source
instance QuotientAddGroup.instIsTopologicalAddGroup {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (N : AddSubgroup G) [N.Normal] :
IsTopologicalAddGroup (G ⧸ N)
source
theorem QuotientGroup.isClosedMap_coe {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {H : Subgroup G} (hH : IsCompact ↑H) :
IsClosedMap mk
source
theorem QuotientAddGroup.isClosedMap_coe {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {H : AddSubgroup G} (hH : IsCompact ↑H) :
IsClosedMap mk
source
instance QuotientGroup.instT3Space {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] [hN : IsClosed ↑N] :
T3Space (G ⧸ N)
source
instance QuotientAddGroup.instT3Space {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (N : AddSubgroup G) [N.Normal] [hN : IsClosed ↑N] :
T3Space (G ⧸ N)