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
instance QuotientGroup.instTopologicalSpace {G : Type u_1} [TopologicalSpace G] [Group G] (N : Subgroup G) :
TopologicalSpace (G ⧸ N)
Equations
source
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 QuotientGroup.mk
source
theorem QuotientAddGroup.isQuotientMap_mk {G : Type u_1} [TopologicalSpace G] [AddGroup G] (N : AddSubgroup G) :
Topology.IsQuotientMap QuotientAddGroup.mk
source
@[deprecated QuotientGroup.isQuotientMap_mk]
theorem QuotientGroup.quotientMap_mk {G : Type u_1} [TopologicalSpace G] [Group G] (N : Subgroup G) :
Topology.IsQuotientMap QuotientGroup.mk

Alias of QuotientGroup.isQuotientMap_mk.

source
theorem QuotientGroup.continuous_mk {G : Type u_1} [TopologicalSpace G] [Group G] {N : Subgroup G} :
Continuous QuotientGroup.mk
source
theorem QuotientAddGroup.continuous_mk {G : Type u_1} [TopologicalSpace G] [AddGroup G] {N : AddSubgroup G} :
Continuous QuotientAddGroup.mk
source
theorem QuotientGroup.isOpenMap_coe {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul G] {N : Subgroup G} :
IsOpenMap QuotientGroup.mk
source
theorem QuotientAddGroup.isOpenMap_coe {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {N : AddSubgroup G} :
IsOpenMap QuotientAddGroup.mk
source
theorem QuotientGroup.isOpenQuotientMap_mk {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul G] {N : Subgroup G} :
IsOpenQuotientMap QuotientGroup.mk
source
theorem QuotientAddGroup.isOpenQuotientMap_mk {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {N : AddSubgroup G} :
IsOpenQuotientMap QuotientAddGroup.mk
source
@[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
source
@[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
source
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)
source
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)
source
instance QuotientGroup.instContinuousSMul {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul G] {N : Subgroup G} :
ContinuousSMul G (G ⧸ N)
source
instance QuotientAddGroup.instContinuousVAdd {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {N : AddSubgroup G} :
ContinuousVAdd G (G ⧸ N)
source
instance QuotientGroup.instContinuousConstSMul {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul G] {N : Subgroup G} :
ContinuousConstSMul G (G ⧸ N)
source
instance QuotientAddGroup.instContinuousConstVAdd {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] {N : AddSubgroup G} :
ContinuousConstVAdd G (G ⧸ N)
source
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.

source
instance QuotientAddGroup.instLocallyCompactSpace {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] [LocallyCompactSpace G] (N : AddSubgroup G) :
LocallyCompactSpace (G ⧸ N)
source
@[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
source
@[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
source
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.

source
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.

source
instance QuotientGroup.instFirstCountableTopology {G : Type u_1} [TopologicalSpace G] [Group G] [ContinuousMul G] (N : Subgroup G) [FirstCountableTopology G] :
FirstCountableTopology (G ⧸ N)
source
instance QuotientAddGroup.instFirstCountableTopology {G : Type u_1} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (N : AddSubgroup G) [FirstCountableTopology G] :
FirstCountableTopology (G ⧸ N)
source
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.

source
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.

source
@[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
source
@[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
source
instance QuotientGroup.instTopologicalGroup {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] (N : Subgroup G) [N.Normal] :
TopologicalGroup (G ⧸ N)
source
instance QuotientAddGroup.instTopologicalAddGroup {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (N : AddSubgroup G) [N.Normal] :
TopologicalAddGroup (G ⧸ N)
source
@[deprecated]
theorem topologicalGroup_quotient {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] (N : Subgroup G) [N.Normal] :
TopologicalGroup (G ⧸ N)
source
@[deprecated]
theorem topologicalAddGroup_quotient {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (N : AddSubgroup G) [N.Normal] :
TopologicalAddGroup (G ⧸ N)
source
theorem QuotientGroup.isClosedMap_coe {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] {H : Subgroup G} (hH : IsCompact ↑H) :
IsClosedMap QuotientGroup.mk
source
theorem QuotientAddGroup.isClosedMap_coe {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] {H : AddSubgroup G} (hH : IsCompact ↑H) :
IsClosedMap QuotientAddGroup.mk
source
instance QuotientGroup.instT3Space {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] (N : Subgroup G) [N.Normal] [hN : IsClosed ↑N] :
T3Space (G ⧸ N)
source
instance QuotientAddGroup.instT3Space {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] (N : AddSubgroup G) [N.Normal] [hN : IsClosed ↑N] :
T3Space (G ⧸ N)