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.

instance QuotientGroup.instTopologicalSpace {G : Type u_1} [TopologicalSpace G] [Group G] (N : Subgroup G) : TopologicalSpace (G ⧸ N)

instance QuotientAddGroup.instTopologicalSpace {G : Type u_1} [TopologicalSpace G] [AddGroup G] (N : AddSubgroup G) : TopologicalSpace (G ⧸ N)

instance QuotientGroup.instCompactSpaceQuotientSubgroup {G : Type u_1} [TopologicalSpace G] [Group G] [CompactSpace G] (N : Subgroup G) : CompactSpace (G ⧸ N)

instance QuotientAddGroup.instCompactSpaceQuotientAddSubgroup {G : Type u_1} [TopologicalSpace G] [AddGroup G] [CompactSpace G] (N : AddSubgroup G) : CompactSpace (G ⧸ N)

theorem QuotientGroup.isQuotientMap_mk {G : Type u_1} [TopologicalSpace G] [Group G] (N : Subgroup G) : Topology.IsQuotientMap mk

theorem QuotientAddGroup.isQuotientMap_mk {G : Type u_1} [TopologicalSpace G] [AddGroup G] (N : AddSubgroup G) : Topology.IsQuotientMap mk

theorem QuotientGroup.continuous_mk {G : Type u_1} [TopologicalSpace G] [Group G] {N : Subgroup G} : Continuous mk

theorem QuotientAddGroup.continuous_mk {G : Type u_1} [TopologicalSpace G] [AddGroup G] {N : AddSubgroup G} : Continuous mk

theorem QuotientGroup.isOpenMap_coe {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul G] {N : Subgroup G} : IsOpenMap mk

theorem QuotientAddGroup.isOpenMap_coe {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {N : AddSubgroup G} : IsOpenMap mk

theorem QuotientGroup.isOpenQuotientMap_mk {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul G] {N : Subgroup G} : IsOpenQuotientMap mk

theorem QuotientAddGroup.isOpenQuotientMap_mk {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {N : AddSubgroup G} : IsOpenQuotientMap mk

@[simp]

theorem QuotientGroup.dense_preimage_mk {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul G] {N : Subgroup G} {s : Set (G ⧸ N)} : Dense (mk ⁻¹' s) ↔ Dense s

@[simp]

theorem QuotientAddGroup.dense_preimage_mk {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {N : AddSubgroup G} {s : Set (G ⧸ N)} : Dense (mk ⁻¹' s) ↔ Dense s

theorem QuotientGroup.dense_image_mk {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul G] {N : Subgroup G} {s : Set G} : Dense (mk '' s) ↔ Dense (s * ↑N)

theorem QuotientAddGroup.dense_image_mk {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {N : AddSubgroup G} {s : Set G} : Dense (mk '' s) ↔ Dense (s + ↑N)

instance QuotientGroup.instContinuousSMul {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul G] {N : Subgroup G} : ContinuousSMul G (G ⧸ N)

instance QuotientAddGroup.instContinuousVAdd {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {N : AddSubgroup G} : ContinuousVAdd G (G ⧸ N)

instance QuotientGroup.instContinuousConstSMul {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul G] {N : Subgroup G} : ContinuousConstSMul G (G ⧸ N)

instance QuotientAddGroup.instContinuousConstVAdd {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {N : AddSubgroup G} : ContinuousConstVAdd G (G ⧸ N)

theorem QuotientGroup.t1Space_iff {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul G] {N : Subgroup G} : T1Space (G ⧸ N) ↔ IsClosed ↑N

theorem QuotientAddGroup.t1Space_iff {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {N : AddSubgroup G} : T1Space (G ⧸ N) ↔ IsClosed ↑N

theorem QuotientGroup.discreteTopology_iff {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul G] {N : Subgroup G} : DiscreteTopology (G ⧸ N) ↔ IsOpen ↑N

theorem QuotientAddGroup.discreteTopology_iff {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {N : AddSubgroup G} : DiscreteTopology (G ⧸ N) ↔ IsOpen ↑N

instance QuotientGroup.instT1Space {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul 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.

instance QuotientAddGroup.instT1Space {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd 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.

theorem QuotientGroup.discreteTopology {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul G] {N : Subgroup G} (hN : IsOpen ↑N) : DiscreteTopology (G ⧸ N)

theorem QuotientAddGroup.discreteTopology {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {N : AddSubgroup G} (hN : IsOpen ↑N) : DiscreteTopology (G ⧸ N)

instance QuotientGroup.instLocallyCompactSpace {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul G] [LocallyCompactSpace G] (N : Subgroup G) : LocallyCompactSpace (G ⧸ N)

A quotient of a locally compact group is locally compact.

instance QuotientAddGroup.instLocallyCompactSpace {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] [LocallyCompactSpace G] (N : AddSubgroup G) : LocallyCompactSpace (G ⧸ N)

theorem QuotientGroup.nhds_eq {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul 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.

theorem QuotientAddGroup.nhds_eq {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd 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.

instance QuotientGroup.instFirstCountableTopology {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul G] (N : Subgroup G) [FirstCountableTopology G] : FirstCountableTopology (G ⧸ N)

instance QuotientAddGroup.instFirstCountableTopology {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (N : AddSubgroup G) [FirstCountableTopology G] : FirstCountableTopology (G ⧸ N)

instance QuotientGroup.instSecondCountableTopology {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul G] (N : Subgroup G) [SecondCountableTopology G] : SecondCountableTopology (G ⧸ N)

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

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

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

instance QuotientGroup.instIsTopologicalGroup {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] : IsTopologicalGroup (G ⧸ N)

instance QuotientAddGroup.instIsTopologicalAddGroup {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (N : AddSubgroup G) [N.Normal] : IsTopologicalAddGroup (G ⧸ N)

theorem QuotientGroup.isClosedMap_coe {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] {H : Subgroup G} (hH : IsCompact ↑H) : IsClosedMap mk

theorem QuotientAddGroup.isClosedMap_coe {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] {H : AddSubgroup G} (hH : IsCompact ↑H) : IsClosedMap mk

instance QuotientGroup.instT3Space {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] [hN : IsClosed ↑N] : T3Space (G ⧸ N)

instance QuotientAddGroup.instT3Space {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] (N : AddSubgroup G) [N.Normal] [hN : IsClosed ↑N] : T3Space (G ⧸ N)