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 space to its separation quotient.

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

theorem IsOpenQuotientMap.id {X : Type u_1} [TopologicalSpace X] : IsOpenQuotientMap id

theorem IsOpenQuotientMap.isQuotientMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (h : IsOpenQuotientMap f) : Topology.IsQuotientMap f

An open quotient map is a quotient map.

theorem IsOpenQuotientMap.iff_isOpenMap_isQuotientMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : IsOpenQuotientMap f ↔ IsOpenMap f ∧ Topology.IsQuotientMap f

theorem IsOpenQuotientMap.of_isOpenMap_isQuotientMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (ho : IsOpenMap f) (hq : Topology.IsQuotientMap f) : IsOpenQuotientMap 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} : Dense (f ⁻¹' s) ↔ Dense s

theorem Topology.IsInducing.isOpenQuotientMap_of_surjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (ind : IsInducing f) (surj : Function.Surjective f) : IsOpenQuotientMap f

theorem Topology.IsInducing.isQuotientMap_of_surjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (ind : IsInducing f) (surj : Function.Surjective f) : IsQuotientMap f

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 : A → B) (g : C → D) (p : A → C) (q : B → D) (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) : TopologicalSpace.coinduced p inst✝ = TopologicalSpace.induced g inst✝¹

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 : A → B) (g : C → D) (p : A → C) (q : B → D) (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) : Topology.IsEmbedding g

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 : A → B) (g : C → D) (p : A → C) (q : B → D) (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) : Topology.IsQuotientMap p