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.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.

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

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

Alias of IsOpenQuotientMap.isQuotientMap.

---

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

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

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

Alias of IsOpenQuotientMap.iff_isOpenMap_isQuotientMap.

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

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

theorem IsOpenQuotientMap.of_isOpenMap_quotientMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (ho : IsOpenMap f) (hq : Topology.IsQuotientMap f) : IsOpenQuotientMap f

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 : 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