doc-next-gen

Mathlib.Topology.Maps.OpenQuotient

Module docstring

{"# Open quotient maps

An open quotient map is an open map f : X → Y which is both an open map and a quotient map. Equivalently, it is a surjective continuous open map. We use the latter characterization as a definition.

Many important quotient maps are open quotient maps, including

  • the quotient map from a topological space to its quotient by the action of a group;
  • the quotient map from a topological group to its quotient by a normal subgroup;
  • the quotient map from a topological spaace to its separation quotient.

Contrary to general quotient maps, the category of open quotient maps is closed under Prod.map. "}

IsOpenQuotientMap.id theorem
: IsOpenQuotientMap (id : X → X)
Full source 
protected theorem id : IsOpenQuotientMap (id : X → X) := ⟨surjective_id, continuous_id, .id⟩
Identity Function is an Open Quotient Map
Informal description
The identity function $\mathrm{id} \colon X \to X$ is an open quotient map.
IsOpenQuotientMap.iff_isOpenMap_isQuotientMap theorem
: IsOpenQuotientMap f ↔ IsOpenMap f ∧ IsQuotientMap f
Full source 
theorem iff_isOpenMap_isQuotientMap : IsOpenQuotientMapIsOpenQuotientMap f ↔ IsOpenMap f ∧ IsQuotientMap f :=
  ⟨fun h ↦ ⟨h.isOpenMap, h.isQuotientMap⟩, fun ⟨ho, hq⟩ ↦ ⟨hq.surjective, hq.continuous, ho⟩⟩
Characterization of Open Quotient Maps as Open and Quotient Maps
Informal description
A continuous map $f \colon X \to Y$ is an open quotient map if and only if it is both an open map and a quotient map.
IsOpenQuotientMap.comp theorem
{g : Y → Z} (hg : IsOpenQuotientMap g) (hf : IsOpenQuotientMap f) : IsOpenQuotientMap (g ∘ f)
Full source 
theorem comp {g : Y → Z} (hg : IsOpenQuotientMap g) (hf : IsOpenQuotientMap f) :
    IsOpenQuotientMap (g ∘ f) :=
  ⟨.comp hg.1 hf.1, .comp hg.2 hf.2, .comp hg.3 hf.3⟩
Composition of Open Quotient Maps is Open Quotient Map
Informal description
Let $f \colon X \to Y$ and $g \colon Y \to Z$ be open quotient maps between topological spaces. Then the composition $g \circ f \colon X \to Z$ is also an open quotient map.
IsOpenQuotientMap.map_nhds_eq theorem
(h : IsOpenQuotientMap f) (x : X) : map f (𝓝 x) = 𝓝 (f x)
Full source 
theorem map_nhds_eq (h : IsOpenQuotientMap f) (x : X) : map f (𝓝 x) = 𝓝 (f x) :=
  le_antisymm h.continuous.continuousAt <| h.isOpenMap.nhds_le _
Neighborhood Filter Preservation under Open Quotient Maps
Informal description
For any open quotient map $f \colon X \to Y$ and any point $x \in X$, the image under $f$ of the neighborhood filter $\mathcal{N}(x)$ is equal to the neighborhood filter $\mathcal{N}(f(x))$ at $f(x)$ in $Y$.
IsOpenQuotientMap.continuous_comp_iff theorem
(h : IsOpenQuotientMap f) {g : Y → Z} : Continuous (g ∘ f) ↔ Continuous g
Full source 
theorem continuous_comp_iff (h : IsOpenQuotientMap f) {g : Y → Z} :
    ContinuousContinuous (g ∘ f) ↔ Continuous g :=
  h.isQuotientMap.continuous_iff.symm
Continuity of Composition with Open Quotient Maps
Informal description
Let $f \colon X \to Y$ be an open quotient map. For any function $g \colon Y \to Z$, the composition $g \circ f$ is continuous if and only if $g$ is continuous.
IsOpenQuotientMap.continuousAt_comp_iff theorem
(h : IsOpenQuotientMap f) {g : Y → Z} {x : X} : ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)
Full source 
theorem continuousAt_comp_iff (h : IsOpenQuotientMap f) {g : Y → Z} {x : X} :
    ContinuousAtContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x) := by
  simp only [ContinuousAt, ← h.map_nhds_eq, tendsto_map'_iff, comp_def]
Continuity of Composition with Open Quotient Maps at a Point
Informal description
Let $f \colon X \to Y$ be an open quotient map. For any function $g \colon Y \to Z$ and any point $x \in X$, the composition $g \circ f$ is continuous at $x$ if and only if $g$ is continuous at $f(x)$.
IsOpenQuotientMap.dense_preimage_iff theorem
(h : IsOpenQuotientMap f) {s : Set Y} : Dense (f ⁻¹' s) ↔ Dense s
Full source 
theorem dense_preimage_iff (h : IsOpenQuotientMap f) {s : Set Y} : DenseDense (f ⁻¹' s) ↔ Dense s :=
  ⟨fun hs ↦ h.surjective.denseRange.dense_of_mapsTo h.continuous hs (mapsTo_preimage _ _),
    fun hs ↦ hs.preimage h.isOpenMap⟩
Density Preservation under Open Quotient Maps
Informal description
Let $f \colon X \to Y$ be an open quotient map. For any subset $s \subseteq Y$, the preimage $f^{-1}(s)$ is dense in $X$ if and only if $s$ is dense in $Y$.