Bourbaki Strict Maps

This file defines Bourbaki strict maps (Topology.IsStrictMap) and proves some of their basic properties. ?

A map f : X → Y between topological spaces is called strict in the sense of Bourbaki if the natural corestriction to its image (i.e., Set.rangeFactorization f) is a quotient map. Equivalently, these are precisely the maps for which the first isomorphism theorem yields a homeomorphism: the canonical bijection X ⧸ ker f ≃ range f is a homeomorphism if and only if f is strict. This provides a natural generalization of quotient maps to non-surjective maps.

Many important classes of maps are automatically continuous strict maps, including:

• continuous open maps (IsOpenMap.isStrictMap);
• continuous closed maps (IsClosedMap.isStrictMap).

Equivalent characterizations

We provide several equivalent ways to characterize a strict map f:

• Topology.isStrictMap_iff_isHomeomorph_quotientKerEquivRange: f is strict if and only if the canonical bijection Quotient (Setoid.ker f) ≃ Set.range f is a homeomorphism.
• Topology.isStrictMap_iff_isEmbedding_kerLift: f is strict if and only if the canonical injection Quotient (Setoid.ker f) → Y (Setoid.kerLift f) is an embedding.

def Topology.IsStrictMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : Prop

A map is a strict map in the sense of Bourbaki if the natural map to its image is a quotient map.

Equations

• Topology.IsStrictMap f = Topology.IsQuotientMap (Set.rangeFactorization f)

theorem Topology.isStrictMap_iff_isQuotientMap_rangeFactorization {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : IsStrictMap f ↔ IsQuotientMap (Set.rangeFactorization f)

theorem Topology.isStrictMap_iff_isHomeomorph_quotientKerEquivRange {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : IsStrictMap f ↔ IsHomeomorph ⇑(Setoid.quotientKerEquivRange f)

A map is a strict map if and only if the canonical bijection Quotient (Setoid.ker f) ≃ Set.range f is a homeomorphism.

noncomputable def Topology.Homeomorph.quotientKerEquivRange {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsStrictMap f) : Quotient (Setoid.ker f) ≃ₜ ↑(Set.range f)

The homeomorphism Quotient (Setoid.ker f) ≃ₜ Set.range f given by a strict map f. This is the homeomorphism obtained from the first isomorphism theorem.

Equations

• Topology.Homeomorph.quotientKerEquivRange hf = IsHomeomorph.homeomorph ⇑(Setoid.quotientKerEquivRange f) ⋯

theorem Topology.isStrictMap_iff_isEmbedding_kerLift {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : IsStrictMap f ↔ IsEmbedding (Setoid.kerLift f)

A map is a strict map if and only if the canonical injection Quotient (Setoid.ker f) → Y (Setoid.kerLift f) is an embedding.

theorem Topology.IsStrictMap.continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsStrictMap f) : Continuous f

A strict map is continuous, since the range factorization is continuous.

theorem Topology.IsOpenMap.isStrictMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (ho : IsOpenMap f) (h_cont : Continuous f) : IsStrictMap f

A open continuous map is a strict map.

theorem Topology.IsClosedMap.isStrictMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hc : IsClosedMap f) (h_cont : Continuous f) : IsStrictMap f

A closed continuous map is a strict map.