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 QuotientAddGroup.instTopologicalSpace {G : Type u_1} [TopologicalSpace G] [AddGroup G] (N : AddSubgroup G) : TopologicalSpace (G ⧸ N)

Equations

• QuotientAddGroup.instTopologicalSpace N = instTopologicalSpaceQuotient

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

Equations

• QuotientGroup.instTopologicalSpace N = instTopologicalSpaceQuotient

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

@[deprecated QuotientGroup.isQuotientMap_mk]

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

Alias of QuotientGroup.isQuotientMap_mk.

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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.

Equations

• ⋯ = ⋯

@[deprecated]

theorem QuotientAddGroup.continuous_smul₁ {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {N : AddSubgroup G} (x : G ⧸ N) : Continuous fun (g : G) => g +ᵥ x

@[deprecated]

theorem QuotientGroup.continuous_smul₁ {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul G] {N : Subgroup G} (x : G ⧸ N) : Continuous fun (g : G) => g • x

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

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

theorem QuotientGroup.nhds_eq {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul G] (N : Subgroup G) (x : G) : nhds ↑x = Filter.map QuotientGroup.mk (nhds x)

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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.

Equations

• ⋯ = ⋯

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.

Equations

• ⋯ = ⋯

@[deprecated]

theorem QuotientAddGroup.nhds_zero_isCountablyGenerated {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (N : AddSubgroup G) [FirstCountableTopology G] [N.Normal] : (nhds 0).IsCountablyGenerated

@[deprecated]

theorem QuotientGroup.nhds_one_isCountablyGenerated {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul G] (N : Subgroup G) [FirstCountableTopology G] [N.Normal] : (nhds 1).IsCountablyGenerated

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[deprecated]

theorem topologicalAddGroup_quotient {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (N : AddSubgroup G) [N.Normal] : TopologicalAddGroup (G ⧸ N)

@[deprecated]

theorem topologicalGroup_quotient {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] (N : Subgroup G) [N.Normal] : TopologicalGroup (G ⧸ N)

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯