Mathlib.Topology.Algebra.Group.Quotient

QuotientGroup.instTopologicalSpace instance

(N : Subgroup G) : TopologicalSpace (G ⧸ N)

Full source

@[to_additive]
instance instTopologicalSpace (N : Subgroup G) : TopologicalSpace (G ⧸ N) :=
  instTopologicalSpaceQuotient

Quotient Topology on Quotient Groups

Informal description

For any group $G$ and subgroup $N$ of $G$, the quotient group $G ⧸ N$ is equipped with the quotient topology induced by the canonical projection $G \to G ⧸ N$.

QuotientGroup.instCompactSpaceQuotientSubgroup instance

[CompactSpace G] (N : Subgroup G) : CompactSpace (G ⧸ N)

Full source

@[to_additive]
instance [CompactSpace G] (N : Subgroup G) : CompactSpace (G ⧸ N) :=
  Quotient.compactSpace

Compactness of Quotient Groups from Compact Groups

Informal description

For any compact topological group $G$ and subgroup $N$ of $G$, the quotient group $G ⧸ N$ is also compact when equipped with the quotient topology.

QuotientGroup.isQuotientMap_mk theorem

(N : Subgroup G) : IsQuotientMap (mk : G → G ⧸ N)

Full source

@[to_additive]
theorem isQuotientMap_mk (N : Subgroup G) : IsQuotientMap (mk : G → G ⧸ N) :=
  isQuotientMap_quot_mk

Canonical Projection is Quotient Map for Quotient Group Topology

Informal description

For any subgroup $N$ of a group $G$, the canonical projection map $\pi : G \to G/N$ is a quotient map in the topological sense. This means $\pi$ is continuous and surjective, and the topology on $G/N$ is the finest topology for which $\pi$ is continuous.

QuotientGroup.continuous_mk theorem

{N : Subgroup G} : Continuous (mk : G → G ⧸ N)

Full source

@[to_additive (attr := continuity, fun_prop)]
theorem continuous_mk {N : Subgroup G} : Continuous (mk : G → G ⧸ N) :=
  continuous_quot_mk

Continuity of the Quotient Group Projection

Informal description

For any subgroup $N$ of a topological group $G$, the canonical projection map $\pi \colon G \to G/N$ to the quotient group $G/N$ (equipped with the quotient topology) is continuous.

QuotientGroup.isOpenMap_coe theorem

: IsOpenMap ((↑) : G → G ⧸ N)

Full source

@[to_additive]
theorem isOpenMap_coe : IsOpenMap ((↑) : G → G ⧸ N) := isOpenMap_quotient_mk'_mul

Openness of the Quotient Group Projection Map

Informal description

The canonical projection map $\pi \colon G \to G/N$ from a topological group $G$ to its quotient group $G/N$ by a subgroup $N$ is an open map, i.e., for every open subset $U \subseteq G$, the image $\pi(U)$ is open in $G/N$.

QuotientGroup.isOpenQuotientMap_mk theorem

: IsOpenQuotientMap (mk : G → G ⧸ N)

Full source

@[to_additive]
theorem isOpenQuotientMap_mk : IsOpenQuotientMap (mk : G → G ⧸ N) :=
  MulAction.isOpenQuotientMap_quotientMk

Open Quotient Map Property for Quotient Groups

Informal description

The canonical projection map $\pi \colon G \to G/N$ from a topological group $G$ to its quotient group $G/N$ by a subgroup $N$ is an open quotient map. That is, $\pi$ is surjective, continuous, and maps open sets in $G$ to open sets in $G/N$.

QuotientGroup.dense_preimage_mk theorem

{s : Set (G ⧸ N)} : Dense ((↑) ⁻¹' s : Set G) ↔ Dense s

Full source

@[to_additive (attr := simp)]
theorem dense_preimage_mk {s : Set (G ⧸ N)} : DenseDense ((↑) ⁻¹' s : Set G) ↔ Dense s :=
  isOpenQuotientMap_mk.dense_preimage_iff

Density Preservation under Quotient Group Projection

Informal description

For any subset $s$ of the quotient group $G/N$, the preimage of $s$ under the canonical projection $\pi \colon G \to G/N$ is dense in $G$ if and only if $s$ is dense in $G/N$.

QuotientGroup.dense_image_mk theorem

{s : Set G} : Dense (mk '' s : Set (G ⧸ N)) ↔ Dense (s * (N : Set G))

Full source

@[to_additive]
theorem dense_image_mk {s : Set G} :
    DenseDense (mk '' s : Set (G ⧸ N)) ↔ Dense (s * (N : Set G)) := by
  rw [← dense_preimage_mk, preimage_image_mk_eq_mul]

Density of Image in Quotient Group Equals Density of Product with Subgroup

Informal description

For any subset $s$ of a group $G$ and a subgroup $N$ of $G$, the image of $s$ under the canonical projection $\pi \colon G \to G/N$ is dense in the quotient group $G/N$ if and only if the product set $s \cdot N$ is dense in $G$.

QuotientGroup.instContinuousSMul instance

: ContinuousSMul G (G ⧸ N)

Full source

@[to_additive]
instance instContinuousSMul : ContinuousSMul G (G ⧸ N) where
  continuous_smul := by
    rw [← (IsOpenQuotientMap.id.prodMap isOpenQuotientMap_mk).continuous_comp_iff]
    exact continuous_mk.comp continuous_mul

Continuity of Scalar Multiplication on Quotient Groups

Informal description

For any topological group $G$ and subgroup $N$ of $G$, the scalar multiplication operation $G \times (G/N) \to G/N$ defined by $(g, xN) \mapsto (gx)N$ is continuous with respect to the quotient topology on $G/N$.

QuotientGroup.instContinuousConstSMul instance

: ContinuousConstSMul G (G ⧸ N)

Full source

@[to_additive]
instance instContinuousConstSMul : ContinuousConstSMul G (G ⧸ N) := inferInstance

Continuous Scalar Multiplication on Quotient Groups

Informal description

For any topological group $G$ and subgroup $N$ of $G$, the quotient group $G ⧸ N$ is equipped with a continuous scalar multiplication structure where for each fixed $g \in G$, the map $xN \mapsto (gx)N$ is continuous.

QuotientGroup.instLocallyCompactSpace instance

[LocallyCompactSpace G] (N : Subgroup G) : LocallyCompactSpace (G ⧸ N)

Full source

/-- A quotient of a locally compact group is locally compact. -/
@[to_additive]
instance instLocallyCompactSpace [LocallyCompactSpace G] (N : Subgroup G) :
    LocallyCompactSpace (G ⧸ N) :=
  QuotientGroup.isOpenQuotientMap_mk.locallyCompactSpace

Local Compactness of Quotient Groups

Informal description

For any locally compact group $G$ and subgroup $N$ of $G$, the quotient group $G ⧸ N$ is also locally compact.

QuotientGroup.nhds_eq theorem

(x : G) : 𝓝 (x : G ⧸ N) = Filter.map (↑) (𝓝 x)

Full source

/-- Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient. -/
@[to_additive
  "Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient."]
theorem nhds_eq (x : G) : 𝓝 (x : G ⧸ N) = Filter.map (↑) (𝓝 x) :=
  (isOpenQuotientMap_mk.map_nhds_eq _).symm

Neighborhood Filter Characterization in Quotient Groups

Informal description

For any element $x$ in a topological group $G$ and any subgroup $N$ of $G$, the neighborhood filter of the coset $[x] \in G/N$ is equal to the image under the canonical projection $\pi \colon G \to G/N$ of the neighborhood filter of $x$ in $G$. In other words, $\mathcal{N}([x]) = \pi_*(\mathcal{N}(x))$.

QuotientGroup.instFirstCountableTopology instance

[FirstCountableTopology G] : FirstCountableTopology (G ⧸ N)

Full source

@[to_additive]
instance instFirstCountableTopology [FirstCountableTopology G] :
    FirstCountableTopology (G ⧸ N) where
  nhds_generated_countable := mk_surjective.forall.2 fun x ↦ nhds_eq N x ▸ inferInstance

First-Countability of Quotient Groups

Informal description

For any topological group $G$ that is first-countable and any subgroup $N$ of $G$, the quotient group $G ⧸ N$ equipped with the quotient topology is also first-countable.

QuotientGroup.instSecondCountableTopology instance

[SecondCountableTopology G] : SecondCountableTopology (G ⧸ N)

Full source

/-- The quotient of a second countable topological group by a subgroup is second countable. -/
@[to_additive
  "The quotient of a second countable additive topological group by a subgroup is second
  countable."]
instance instSecondCountableTopology [SecondCountableTopology G] :
    SecondCountableTopology (G ⧸ N) :=
  ContinuousConstSMul.secondCountableTopology

Second Countability of Quotient Groups

Informal description

For any topological group $G$ that is second-countable and any subgroup $N$ of $G$, the quotient group $G ⧸ N$ equipped with the quotient topology is also second-countable.

QuotientGroup.instIsTopologicalGroup instance

[N.Normal] : IsTopologicalGroup (G ⧸ N)

Full source

@[to_additive]
instance instIsTopologicalGroup [N.Normal] : IsTopologicalGroup (G ⧸ N) where
  continuous_mul := by
    rw [← (isOpenQuotientMap_mk.prodMap isOpenQuotientMap_mk).continuous_comp_iff]
    exact continuous_mk.comp continuous_mul
  continuous_inv := continuous_inv.quotient_map' _

Quotient of a Topological Group by a Normal Subgroup is a Topological Group

Informal description

For any topological group $G$ and normal subgroup $N$ of $G$, the quotient group $G/N$ equipped with the quotient topology is a topological group. That is, the group operations (multiplication and inversion) are continuous with respect to the quotient topology.

QuotientGroup.isClosedMap_coe theorem

{H : Subgroup G} (hH : IsCompact (H : Set G)) : IsClosedMap ((↑) : G → G ⧸ H)

Full source

@[to_additive]
theorem isClosedMap_coe {H : Subgroup G} (hH : IsCompact (H : Set G)) :
    IsClosedMap ((↑) : G → G ⧸ H) := by
  intro t ht
  rw [← (isQuotientMap_mk H).isClosed_preimage, preimage_image_mk_eq_mul]
  exact ht.mul_right_of_isCompact hH

Canonical Projection is Closed Map for Compact Subgroup Quotient

Informal description

Let $G$ be a topological group and $H$ a subgroup of $G$ such that $H$ is compact as a subset of $G$. Then the canonical projection map $\pi \colon G \to G/H$ is a closed map, meaning that for every closed subset $C \subseteq G$, the image $\pi(C)$ is closed in the quotient space $G/H$.

QuotientGroup.instT3Space instance

[N.Normal] [hN : IsClosed (N : Set G)] : T3Space (G ⧸ N)

Full source

@[to_additive]
instance instT3Space [N.Normal] [hN : IsClosed (N : Set G)] : T3Space (G ⧸ N) := by
  rw [← QuotientGroup.ker_mk' N] at hN
  haveI := IsTopologicalGroup.t1Space (G ⧸ N) ((isQuotientMap_mk N).isClosed_preimage.mp hN)
  infer_instance

Quotient of a Topological Group by a Closed Normal Subgroup is T₃

Informal description

For any topological group $G$ and normal subgroup $N$ of $G$, if $N$ is closed as a subset of $G$, then the quotient group $G/N$ equipped with the quotient topology is a T₃ space.