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.
theorem
IsOpenQuotientMap.quotientMap
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(h : IsOpenQuotientMap f)
:
An open quotient map is a quotient map.
theorem
IsOpenQuotientMap.iff_isOpenMap_quotientMap
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
:
IsOpenQuotientMap f ↔ IsOpenMap f ∧ QuotientMap f
theorem
IsOpenQuotientMap.of_isOpenMap_quotientMap
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(ho : IsOpenMap f)
(hq : QuotientMap f)
:
theorem
IsOpenQuotientMap.comp
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Y}
{g : Y → Z}
(hg : IsOpenQuotientMap g)
(hf : IsOpenQuotientMap f)
:
IsOpenQuotientMap (g ∘ f)
theorem
IsOpenQuotientMap.map_nhds_eq
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(h : IsOpenQuotientMap f)
(x : X)
:
Filter.map f (nhds x) = nhds (f x)
theorem
IsOpenQuotientMap.continuous_comp_iff
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Y}
(h : IsOpenQuotientMap f)
{g : Y → Z}
:
Continuous (g ∘ f) ↔ Continuous g
theorem
IsOpenQuotientMap.continuousAt_comp_iff
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
{f : X → Y}
(h : IsOpenQuotientMap f)
{g : Y → Z}
{x : X}
:
ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)
theorem
IsOpenQuotientMap.dense_preimage_iff
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
{f : X → Y}
(h : IsOpenQuotientMap f)
{s : Set Y}
: