# Documentation

Mathlib.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 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.

Instances For
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: TODO: drop this definition.

Instances For
instance ContinuousMap.HomotopyEquiv.instCoeFunHomotopyEquivForAll {X : Type u} {Y : Type v} [] [] :
CoeFun () fun x => XY
@[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.

Instances For
@[simp]
theorem Homeomorph.coe_toHomotopyEquiv {X : Type u} {Y : Type v} [] [] (h : X ≃ₜ Y) :
= 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.

Instances For
@[simp]
theorem ContinuousMap.HomotopyEquiv.coe_invFun {X : Type u} {Y : Type v} [] [] (h : ) :
h.invFun =
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.

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.

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

Any topological space is homotopy equivalent to itself.

Instances For
@[simp]
theorem ContinuousMap.HomotopyEquiv.trans_symm_apply {X : Type u} {Y : Type v} {Z : Type w} [] [] [] (h₁ : ) (h₂ : ) :
∀ (a : Z),
@[simp]
theorem ContinuousMap.HomotopyEquiv.trans_apply {X : Type u} {Y : Type v} {Z : Type w} [] [] [] (h₁ : ) (h₂ : ) :
∀ (a : X), ↑() a = h₂ (h₁ 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.

Instances For
theorem ContinuousMap.HomotopyEquiv.symm_trans {X : Type u} {Y : Type v} {Z : Type w} [] [] [] (h₁ : ) (h₂ : ) :
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'.

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.

Instances For
@[simp]
@[simp]
theorem Homeomorph.symm_toHomotopyEquiv {X : Type u} {Y : Type v} [] [] (h : X ≃ₜ Y) :
@[simp]
theorem Homeomorph.trans_toHomotopyEquiv {X : Type u} {Y : Type v} {Z : Type w} [] [] [] (h₀ : X ≃ₜ Y) (h₁ : Y ≃ₜ Z) :