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.

theorem Topology.IsHomeomorph.isStrictMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (f_homeo : IsHomeomorph f) : IsStrictMap f

A homeomorphism is a strict map.

theorem Topology.IsStrictMap.id {X : Type u_1} [TopologicalSpace X] : IsStrictMap _root_.id

The identity is a strict map.

theorem Topology.IsQuotientMap.isStrictMap_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : Y → Z} (f_quot : IsQuotientMap f) : IsStrictMap g ↔ IsStrictMap (g ∘ f)

Assume that f : X → Y is a quotient map. Then g : Y → Z is strict if and only if g ∘ f is strict.

theorem Topology.IsQuotientMap.isStrictMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (f_quot : IsQuotientMap f) : IsStrictMap f

A quotient map is strict. See also isQuotientMap_iff_isStrictMap_surjective.

theorem Topology.IsEmbedding.isStrictMap_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : Y → Z} (g_emb : IsEmbedding g) : IsStrictMap f ↔ IsStrictMap (g ∘ f)

Assume that g : Y → Z is an embedding. Then f : X → Y is strict if and only if g ∘ f is strict.

theorem Topology.IsEmbedding.isStrictMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (f_emb : IsEmbedding f) : IsStrictMap f

An embedding is strict. See also isEmbedding_iff_isStrictMap_injective.

theorem Topology.isQuotientMap_iff_isStrictMap_surjective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : IsQuotientMap f ↔ IsStrictMap f ∧ Function.Surjective f

Quotient maps are precisely surjective strict maps.

theorem Topology.isEmbedding_iff_isStrictMap_injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : IsEmbedding f ↔ IsStrictMap f ∧ Function.Injective f

Embeddings are precisely injective strict maps.