Documentation

Mathlib.Topology.Maps.OpenQuotient

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

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

An open quotient map is a quotient map.

@[deprecated IsOpenQuotientMap.isQuotientMap (since := "2024-10-22")]

Alias of IsOpenQuotientMap.isQuotientMap.


An open quotient map is a quotient map.

@[deprecated IsOpenQuotientMap.iff_isOpenMap_isQuotientMap (since := "2024-10-22")]

Alias of IsOpenQuotientMap.iff_isOpenMap_isQuotientMap.

@[deprecated IsOpenQuotientMap.of_isOpenMap_isQuotientMap (since := "2024-10-22")]

Alias of IsOpenQuotientMap.of_isOpenMap_isQuotientMap.

theorem IsOpenQuotientMap.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XY} {g : YZ} (hg : IsOpenQuotientMap g) (hf : IsOpenQuotientMap f) :
theorem IsOpenQuotientMap.map_nhds_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (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 : XY} (h : IsOpenQuotientMap f) {g : YZ} :
theorem IsOpenQuotientMap.continuousAt_comp_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XY} (h : IsOpenQuotientMap f) {g : YZ} {x : X} :
theorem IsOpenQuotientMap.dense_preimage_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (h : IsOpenQuotientMap f) {s : Set Y} :
theorem coinduced_eq_induced_of_isOpenQuotientMap_of_isInducing {A : Type u_4} {B : Type u_5} {C : Type u_6} {D : Type u_7} [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace D] (f : AB) (g : CD) (p : AC) (q : BD) (h : g p = q f) (hf : Topology.IsInducing f) (hp : Function.Surjective p) (hq : IsOpenQuotientMap q) (hg : Function.Injective g) (H : q ⁻¹' (q '' Set.range f) Set.range f) :

Given the following diagram with f inducing, p surjective, q an open quotient map, and g injective. Suppose the image of A in B is stable under the equivalence mod q, then the coinduced topology on C (from A) coincides with the induced topology (from D).

A -f→ B
∣     ∣
p     q
↓     ↓
C -g→ D

A typical application is when K ≤ H are subgroups of G, then the quotient topology on H/K is also the subspace topology from G/K.

theorem isEmbedding_of_isOpenQuotientMap_of_isInducing {A : Type u_4} {B : Type u_5} {C : Type u_6} {D : Type u_7} [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [TopologicalSpace D] (f : AB) (g : CD) (p : AC) (q : BD) (h : g p = q f) (hf : Topology.IsInducing f) (hp : Topology.IsQuotientMap p) (hq : IsOpenQuotientMap q) (hg : Function.Injective g) (H : q ⁻¹' (q '' Set.range f) Set.range f) :
theorem isQuotientMap_of_isOpenQuotientMap_of_isInducing {A : Type u_4} {B : Type u_5} {C : Type u_6} {D : Type u_7} [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [TopologicalSpace D] (f : AB) (g : CD) (p : AC) (q : BD) (h : g p = q f) (hf : Topology.IsInducing f) (hp : Function.Surjective p) (hq : IsOpenQuotientMap q) (hg : Topology.IsEmbedding g) (H : q ⁻¹' (q '' Set.range f) Set.range f) :