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.

structure ContinuousMap.HomotopyEquiv (X : Type u) (Y : Type v) [TopologicalSpace X] [TopologicalSpace Y] : 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 (ContinuousMap.id X)
• right_inv : (self.toFun.comp self.invFun).Homotopic (ContinuousMap.id Y)

theorem ContinuousMap.HomotopyEquiv.ext {X : Type u} {Y : Type v} {inst✝ : TopologicalSpace X} {inst✝¹ : TopologicalSpace Y} {x y : ContinuousMap.HomotopyEquiv X Y} (toFun : x.toFun = y.toFun) (invFun : x.invFun = y.invFun) : x = y

def ContinuousMap.«term_≃ₕ_» : Lean.TrailingParserDescr

Equations

• ContinuousMap.«term_≃ₕ_» = Lean.ParserDescr.trailingNode `ContinuousMap.«term_≃ₕ_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ₕ ") (Lean.ParserDescr.cat `term 26))

def ContinuousMap.HomotopyEquiv.toFun' {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (e : ContinuousMap.HomotopyEquiv X Y) : X → Y

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 (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: drop this definition.

Equations

• ↑e = ⇑e.toFun

instance ContinuousMap.HomotopyEquiv.instCoeFunForall {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : CoeFun (ContinuousMap.HomotopyEquiv X Y) fun (x : ContinuousMap.HomotopyEquiv X Y) => X → Y

Equations

• ContinuousMap.HomotopyEquiv.instCoeFunForall = { coe := ContinuousMap.HomotopyEquiv.toFun' }

@[simp]

theorem ContinuousMap.HomotopyEquiv.toFun_eq_coe {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (h : ContinuousMap.HomotopyEquiv X Y) : ⇑h.toFun = ↑h

theorem ContinuousMap.HomotopyEquiv.continuous {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (h : ContinuousMap.HomotopyEquiv X Y) : Continuous ↑h

def Homeomorph.toHomotopyEquiv {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : ContinuousMap.HomotopyEquiv X Y

Any homeomorphism is a homotopy equivalence.

Equations

• h.toHomotopyEquiv = { toFun := ↑h, invFun := ↑h.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Homeomorph.coe_toHomotopyEquiv {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : ↑h.toHomotopyEquiv = ⇑h

def ContinuousMap.HomotopyEquiv.symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (h : ContinuousMap.HomotopyEquiv X Y) : ContinuousMap.HomotopyEquiv Y X

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 := ⋯ }

@[simp]

theorem ContinuousMap.HomotopyEquiv.coe_invFun {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (h : ContinuousMap.HomotopyEquiv X Y) : ⇑h.invFun = ↑h.symm

def ContinuousMap.HomotopyEquiv.Simps.apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (h : ContinuousMap.HomotopyEquiv X 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

• ContinuousMap.HomotopyEquiv.Simps.apply h = ↑h

def ContinuousMap.HomotopyEquiv.Simps.symm_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (h : ContinuousMap.HomotopyEquiv X 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

• ContinuousMap.HomotopyEquiv.Simps.symm_apply h = ↑h.symm

def ContinuousMap.HomotopyEquiv.refl (X : Type u) [TopologicalSpace X] : ContinuousMap.HomotopyEquiv X X

Any topological space is homotopy equivalent to itself.

Equations

• ContinuousMap.HomotopyEquiv.refl X = (Homeomorph.refl X).toHomotopyEquiv

@[simp]

theorem ContinuousMap.HomotopyEquiv.refl_apply (X : Type u) [TopologicalSpace X] (a : X) : ↑(ContinuousMap.HomotopyEquiv.refl X) a = a

@[simp]

theorem ContinuousMap.HomotopyEquiv.refl_symm_apply (X : Type u) [TopologicalSpace X] (a : X) : ↑(ContinuousMap.HomotopyEquiv.refl X).symm a = a

instance ContinuousMap.HomotopyEquiv.instInhabitedUnit : Inhabited (ContinuousMap.HomotopyEquiv Unit Unit)

Equations

• ContinuousMap.HomotopyEquiv.instInhabitedUnit = { default := ContinuousMap.HomotopyEquiv.refl Unit }

def ContinuousMap.HomotopyEquiv.trans {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h₁ : ContinuousMap.HomotopyEquiv X Y) (h₂ : ContinuousMap.HomotopyEquiv Y Z) : ContinuousMap.HomotopyEquiv X Z

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 := ⋯ }

@[simp]

theorem ContinuousMap.HomotopyEquiv.trans_apply {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h₁ : ContinuousMap.HomotopyEquiv X Y) (h₂ : ContinuousMap.HomotopyEquiv Y Z) (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} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h₁ : ContinuousMap.HomotopyEquiv X Y) (h₂ : ContinuousMap.HomotopyEquiv Y Z) (a✝ : Z) : ↑(h₁.trans h₂).symm a✝ = ↑h₁.symm (↑h₂.symm a✝)

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

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 := ⋯ }

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.

@[simp]

theorem Homeomorph.refl_toHomotopyEquiv (X : Type u) [TopologicalSpace X] : (Homeomorph.refl X).toHomotopyEquiv = ContinuousMap.HomotopyEquiv.refl X

@[simp]

theorem Homeomorph.symm_toHomotopyEquiv {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : h.symm.toHomotopyEquiv = h.toHomotopyEquiv.symm

@[simp]

theorem Homeomorph.trans_toHomotopyEquiv {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (h₀ : X ≃ₜ Y) (h₁ : Y ≃ₜ Z) : (h₀.trans h₁).toHomotopyEquiv = h₀.toHomotopyEquiv.trans h₁.toHomotopyEquiv