# mathlib3documentation

topology.homotopy.equiv

# Homotopy equivalences between topological spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• continuous_map.homotopy_equiv is the type of homotopy equivalences between topological spaces.

## 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 : 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)  :
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 : Y) :
@[protected, instance]
def continuous_map.homotopy_equiv.has_coe_to_fun {X : Type u} {Y : Type v}  :
(λ (_x : , X Y)
Equations
@[simp]
theorem continuous_map.homotopy_equiv.to_fun_eq_coe {X : Type u} {Y : Type v} (h : Y) :
@[continuity]
theorem continuous_map.homotopy_equiv.continuous {X : Type u} {Y : Type v} (h : Y) :
def homeomorph.to_homotopy_equiv {X : Type u} {Y : Type v} (h : X ≃ₜ Y) :

Any homeomorphism is a homotopy equivalence.

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

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

Equations
@[simp]
theorem continuous_map.homotopy_equiv.coe_inv_fun {X : Type u} {Y : Type v} (h : Y) :
def continuous_map.homotopy_equiv.simps.apply {X : Type u} {Y : Type v} (h : Y) :
X Y

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

Equations
def continuous_map.homotopy_equiv.simps.symm_apply {X : Type u} {Y : Type v} (h : Y) :
Y X

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
@[simp]
theorem continuous_map.homotopy_equiv.refl_symm_apply (X : Type u) (ᾰ : X) :
=
@[simp]
theorem continuous_map.homotopy_equiv.refl_apply (X : Type u) (ᾰ : X) :
@[protected, instance]
Equations
def continuous_map.homotopy_equiv.trans {X : Type u} {Y : Type v} {Z : Type w} (h₁ : Y) (h₂ : Z) :

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} (h₁ : Y) (h₂ : 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} (h₁ : Y) (h₂ : Z) (ᾰ : X) :
(h₁.trans h₂) = h₂ (h₁ ᾰ)
theorem continuous_map.homotopy_equiv.symm_trans {X : Type u} {Y : Type v} {Z : Type w} (h₁ : Y) (h₂ : Z) :
(h₁.trans h₂).symm = h₂.symm.trans h₁.symm
@[simp]
@[simp]
theorem homeomorph.symm_to_homotopy_equiv {X : Type u} {Y : Type v} (h : X ≃ₜ Y) :
@[simp]
theorem homeomorph.trans_to_homotopy_equiv {X : Type u} {Y : Type v} {Z : Type w} (h₀ : X ≃ₜ Y) (h₁ : Y ≃ₜ Z) :