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.

Group homomorphisms

In general, the product (in the sense of Prod.map) of two strict maps need not be strict. But thanks to MonoidHom.isOpenQuotientMap_of_isQuotientMap, we can replace IsQuotientMap by IsOpenQuotientMap in the setting of group homomorphisms. Therefore we provide several important properties of strict group homomorphisms :

• isStrictMap_iff_isOpenQuotientMap_rangeRestrict: f is a strict group homomorphism if and only if the rangeRestrict of f is an open quotient map.
• isStrictMap_prodMap: The product (in the sense of Prod.map) of strict group homomorphisms is strict.

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.

theorem Topology.Homeomorph.isStrictMap_comp_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : X ≃ₜ Y) {f : Y → Z} : IsStrictMap (f ∘ ⇑e) ↔ IsStrictMap f

Strict maps are preserved when precomposing with a homeomorphism.

theorem Topology.Homeomorph.comp_isStrictMap_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : Y ≃ₜ Z) {f : X → Y} : IsStrictMap (⇑e ∘ f) ↔ IsStrictMap f

Strict maps are preserved when postcomposing with a homeomorphism.

theorem MonoidHom.isStrictMap_iff_isOpenQuotientMap_rangeRestrict {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace H] : Topology.IsStrictMap ⇑f ↔ IsOpenQuotientMap ⇑f.rangeRestrict

A group homomorphism is strict if and only if its rangeRestrict is an open quotient map.

theorem AddMonoidHom.isStrictMap_iff_isOpenQuotientMap_rangeRestrict {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (f : G →+ H) [TopologicalSpace G] [IsTopologicalAddGroup G] [TopologicalSpace H] : Topology.IsStrictMap ⇑f ↔ IsOpenQuotientMap ⇑f.rangeRestrict

theorem MonoidHom.isStrictMap_prodMap_iff {G : Type u_1} {H : Type u_2} {G' : Type u_3} {H' : Type u_4} [Group G'] [Group H'] [Group G] [Group H] {f : G →* H} {g : G' →* H'} [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace H] [TopologicalSpace G'] [IsTopologicalGroup G'] [TopologicalSpace H'] : Topology.IsStrictMap ⇑(f.prodMap g) ↔ Topology.IsStrictMap ⇑f ∧ Topology.IsStrictMap ⇑g

The product (in the sense of Prod.map) of group homomorphisms is strict if and only if each of the morphisms is strict.

theorem AddMonoidHom.isStrictMap_prodMap_iff {G : Type u_1} {H : Type u_2} {G' : Type u_3} {H' : Type u_4} [AddGroup G'] [AddGroup H'] [AddGroup G] [AddGroup H] {f : G →+ H} {g : G' →+ H'} [TopologicalSpace G] [IsTopologicalAddGroup G] [TopologicalSpace H] [TopologicalSpace G'] [IsTopologicalAddGroup G'] [TopologicalSpace H'] : Topology.IsStrictMap ⇑(f.prodMap g) ↔ Topology.IsStrictMap ⇑f ∧ Topology.IsStrictMap ⇑g

theorem MonoidHom.isStrictMap_prodMap {G : Type u_1} {H : Type u_2} {G' : Type u_3} {H' : Type u_4} [Group G'] [Group H'] [Group G] [Group H] {f : G →* H} {g : G' →* H'} [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace H] [TopologicalSpace G'] [IsTopologicalGroup G'] [TopologicalSpace H'] (hf : Topology.IsStrictMap ⇑f) (hg : Topology.IsStrictMap ⇑g) : Topology.IsStrictMap ⇑(f.prodMap g)

The product (in the sense of Prod.map) of strict group homomorphisms is strict

theorem AddMonoidHom.isStrictMap_prodMap {G : Type u_1} {H : Type u_2} {G' : Type u_3} {H' : Type u_4} [AddGroup G'] [AddGroup H'] [AddGroup G] [AddGroup H] {f : G →+ H} {g : G' →+ H'} [TopologicalSpace G] [IsTopologicalAddGroup G] [TopologicalSpace H] [TopologicalSpace G'] [IsTopologicalAddGroup G'] [TopologicalSpace H'] (hf : Topology.IsStrictMap ⇑f) (hg : Topology.IsStrictMap ⇑g) : Topology.IsStrictMap ⇑(f.prodMap g)