# 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 ContinuousMap.id.

## Main definitions #

• ContinuousMap.HomotopyEquiv is the type of homotopy equivalences between topological spaces.

## Notation #

We introduce the notation X ≃ₕ Y for ContinuousMap.HomotopyEquiv X Y in the ContinuousMap locale.

theorem ContinuousMap.HomotopyEquiv.ext_iff {X : Type u} {Y : Type v} :
∀ {inst : } {inst_1 : } {x y : }, x = y x.toFun = y.toFun x.invFun = y.invFun
theorem ContinuousMap.HomotopyEquiv.ext {X : Type u} {Y : Type v} :
∀ {inst : } {inst_1 : } {x y : }, x.toFun = y.toFunx.invFun = y.invFunx = y
structure ContinuousMap.HomotopyEquiv (X : Type u) (Y : Type v) [] [] :
Type (max u v)

A homotopy equivalence between topological spaces X and Y are a pair of functions toFun : C(X, Y) and invFun : C(Y, X) such that toFun.comp invFun and invFun.comp toFun are both homotopic to corresponding identity maps.

• toFun : C(X, Y)
• invFun : C(Y, X)
• left_inv : (self.invFun.comp self.toFun).Homotopic
• right_inv : (self.toFun.comp self.invFun).Homotopic
Instances For
theorem ContinuousMap.HomotopyEquiv.left_inv {X : Type u} {Y : Type v} [] [] (self : ) :
(self.invFun.comp self.toFun).Homotopic
theorem ContinuousMap.HomotopyEquiv.right_inv {X : Type u} {Y : Type v} [] [] (self : ) :
(self.toFun.comp self.invFun).Homotopic
Equations
Instances For
def ContinuousMap.HomotopyEquiv.toFun' {X : Type u} {Y : Type v} [] [] (e : ) :
XY

Coercion of a HomotopyEquiv to function. While the Lean 4 way is to unfold coercions, this auxiliary definition will make porting of Lean 3 code easier.

Porting note (#11215): TODO: drop this definition.

Equations
• e = e.toFun
Instances For
instance ContinuousMap.HomotopyEquiv.instCoeFunForall {X : Type u} {Y : Type v} [] [] :
CoeFun fun (x : ) => XY
Equations
• ContinuousMap.HomotopyEquiv.instCoeFunForall = { coe := ContinuousMap.HomotopyEquiv.toFun' }
@[simp]
theorem ContinuousMap.HomotopyEquiv.toFun_eq_coe {X : Type u} {Y : Type v} [] [] (h : ) :
h.toFun = h
theorem ContinuousMap.HomotopyEquiv.continuous {X : Type u} {Y : Type v} [] [] (h : ) :
def Homeomorph.toHomotopyEquiv {X : Type u} {Y : Type v} [] [] (h : X ≃ₜ Y) :

Any homeomorphism is a homotopy equivalence.

Equations
• h.toHomotopyEquiv = { toFun := h.toContinuousMap, invFun := h.symm.toContinuousMap, left_inv := , right_inv := }
Instances For
@[simp]
theorem Homeomorph.coe_toHomotopyEquiv {X : Type u} {Y : Type v} [] [] (h : X ≃ₜ Y) :
h.toHomotopyEquiv = h
def ContinuousMap.HomotopyEquiv.symm {X : Type u} {Y : Type v} [] [] (h : ) :

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

Equations
• h.symm = { toFun := h.invFun, invFun := h.toFun, left_inv := , right_inv := }
Instances For
@[simp]
theorem ContinuousMap.HomotopyEquiv.coe_invFun {X : Type u} {Y : Type v} [] [] (h : ) :
h.invFun = h.symm
def ContinuousMap.HomotopyEquiv.Simps.apply {X : Type u} {Y : Type v} [] [] (h : ) :
XY

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

Equations
Instances For
def ContinuousMap.HomotopyEquiv.Simps.symm_apply {X : Type u} {Y : Type v} [] [] (h : ) :
YX

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

Equations
Instances For
@[simp]
theorem ContinuousMap.HomotopyEquiv.refl_symm_apply (X : Type u) [] (a : X) :
.symm a = a
@[simp]
theorem ContinuousMap.HomotopyEquiv.refl_apply (X : Type u) [] (a : X) :

Any topological space is homotopy equivalent to itself.

Equations
• = .toHomotopyEquiv
Instances For
@[simp]
theorem ContinuousMap.HomotopyEquiv.trans_apply {X : Type u} {Y : Type v} {Z : Type w} [] [] [] (h₁ : ) (h₂ : ) :
∀ (a : X), (h₁.trans h₂) a = h₂ (h₁ a)
@[simp]
theorem ContinuousMap.HomotopyEquiv.trans_symm_apply {X : Type u} {Y : Type v} {Z : Type w} [] [] [] (h₁ : ) (h₂ : ) :
∀ (a : Z), (h₁.trans h₂).symm a = h₁.symm (h₂.symm a)
def ContinuousMap.HomotopyEquiv.trans {X : Type u} {Y : Type v} {Z : Type w} [] [] [] (h₁ : ) (h₂ : ) :

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

Equations
• h₁.trans h₂ = { toFun := h₂.toFun.comp h₁.toFun, invFun := h₁.invFun.comp h₂.invFun, left_inv := , right_inv := }
Instances For
theorem ContinuousMap.HomotopyEquiv.symm_trans {X : Type u} {Y : Type v} {Z : Type w} [] [] [] (h₁ : ) (h₂ : ) :
(h₁.trans h₂).symm = h₂.symm.trans h₁.symm
def ContinuousMap.HomotopyEquiv.prodCongr {X : Type u} {Y : Type v} {Z : Type w} {Z' : Type x} [] [] [] [] (h₁ : ) (h₂ : ) :

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

Equations
• h₁.prodCongr h₂ = { toFun := h₁.toFun.prodMap h₂.toFun, invFun := h₁.invFun.prodMap h₂.invFun, left_inv := , right_inv := }
Instances For
def ContinuousMap.HomotopyEquiv.piCongrRight {ι : Type u_1} {X : ιType u_2} {Y : ιType u_3} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → TopologicalSpace (Y i)] (h : (i : ι) → ContinuousMap.HomotopyEquiv (X i) (Y i)) :
ContinuousMap.HomotopyEquiv ((i : ι) → X i) ((i : ι) → Y i)

If X i is homotopy equivalent to Y i for each i, then the space of functions (a.k.a. the indexed product) ∀ i, X i is homotopy equivalent to ∀ i, Y i.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Homeomorph.refl_toHomotopyEquiv (X : Type u) [] :
.toHomotopyEquiv =
@[simp]
theorem Homeomorph.symm_toHomotopyEquiv {X : Type u} {Y : Type v} [] [] (h : X ≃ₜ Y) :
h.symm.toHomotopyEquiv = h.toHomotopyEquiv.symm
@[simp]
theorem Homeomorph.trans_toHomotopyEquiv {X : Type u} {Y : Type v} {Z : Type w} [] [] [] (h₀ : X ≃ₜ Y) (h₁ : Y ≃ₜ Z) :
(h₀.trans h₁).toHomotopyEquiv = h₀.toHomotopyEquiv.trans h₁.toHomotopyEquiv