mathlib documentation

topology.homotopy.equiv

Homotopy equivalences between topological spaces #

In this file, we define homotopy equivalences between topological spaces X and Y as a pair of functions f : C(X, Y) and g : C(Y, X) such that f.comp g and g.comp f are both homotopic to id.

Main definitions #

Notation #

We introduce the notation X ≃ₕ Y for continuous_map.homotopy_equiv X Y in the continuous_map locale.

theorem continuous_map.homotopy_equiv.ext {X : Type u} {Y : Type v} {_inst_4 : topological_space X} {_inst_5 : topological_space Y} (x y : continuous_map.homotopy_equiv X Y) (h : x.to_fun = y.to_fun) (h_1 : x.inv_fun = y.inv_fun) :
x = y
@[ext]
structure continuous_map.homotopy_equiv (X : Type u) (Y : Type v) [topological_space X] [topological_space Y] :
Type (max u v)

A homotopy equivalence between topological spaces X and Y are a pair of functions to_fun : C(X, Y) and inv_fun : C(Y, X) such that to_fun.comp inv_fun and inv_fun.comp to_fun are both homotopic to id.

Instances for continuous_map.homotopy_equiv
theorem continuous_map.homotopy_equiv.ext_iff {X : Type u} {Y : Type v} {_inst_4 : topological_space X} {_inst_5 : topological_space Y} (x y : continuous_map.homotopy_equiv X Y) :

Any homeomorphism is a homotopy equivalence.

Equations
@[simp]
theorem homeomorph.coe_to_homotopy_equiv {X : Type u} {Y : Type v} [topological_space X] [topological_space Y] (h : X ≃ₜ Y) :

If X is homotopy equivalent to Y, then Y is homotopy equivalent to X.

Equations

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations

Any topological space is homotopy equivalent to itself.

Equations

If X is homotopy equivalent to Y, and Y is homotopy equivalent to Z, then X is homotopy equivalent to Z.

Equations
@[simp]
theorem continuous_map.homotopy_equiv.trans_symm_apply {X : Type u} {Y : Type v} {Z : Type w} [topological_space X] [topological_space Y] [topological_space Z] (h₁ : continuous_map.homotopy_equiv X Y) (h₂ : continuous_map.homotopy_equiv Y Z) (ᾰ : Z) :
((h₁.trans h₂).symm) = (h₁.symm) ((h₂.symm) ᾰ)
@[simp]
theorem continuous_map.homotopy_equiv.trans_apply {X : Type u} {Y : Type v} {Z : Type w} [topological_space X] [topological_space Y] [topological_space Z] (h₁ : continuous_map.homotopy_equiv X Y) (h₂ : continuous_map.homotopy_equiv Y Z) (ᾰ : X) :
(h₁.trans h₂) = h₂ (h₁ ᾰ)
theorem continuous_map.homotopy_equiv.symm_trans {X : Type u} {Y : Type v} {Z : Type w} [topological_space X] [topological_space Y] [topological_space Z] (h₁ : continuous_map.homotopy_equiv X Y) (h₂ : continuous_map.homotopy_equiv Y Z) :
(h₁.trans h₂).symm = h₂.symm.trans h₁.symm
@[simp]
theorem homeomorph.trans_to_homotopy_equiv {X : Type u} {Y : Type v} {Z : Type w} [topological_space X] [topological_space Y] [topological_space Z] (h₀ : X ≃ₜ Y) (h₁ : Y ≃ₜ Z) :