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 : TopologicalSpace X} {inst_1 : TopologicalSpace Y} (x y : ContinuousMap.HomotopyEquiv X Y), x = y ↔ x.toFun = y.toFun ∧ x.invFun = y.invFun

theorem ContinuousMap.HomotopyEquiv.ext {X : Type u} {Y : Type v} : ∀ {inst : TopologicalSpace X} {inst_1 : TopologicalSpace Y} (x y : ContinuousMap.HomotopyEquiv X Y), x.toFun = y.toFun → x.invFun = y.invFun → x = y

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 : ContinuousMap.Homotopic (ContinuousMap.comp self.invFun self.toFun) (ContinuousMap.id X)
• right_inv : ContinuousMap.Homotopic (ContinuousMap.comp self.toFun self.invFun) (ContinuousMap.id Y)

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

Equations

• One or more equations did not get rendered due to their size.

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 (#11215): TODO: drop this definition.

Equations

• ↑e = ⇑e.toFun

instance ContinuousMap.HomotopyEquiv.instCoeFunHomotopyEquivForAll {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.instCoeFunHomotopyEquivForAll = { 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

• Homeomorph.toHomotopyEquiv h = { toFun := Homeomorph.toContinuousMap h, invFun := Homeomorph.toContinuousMap (Homeomorph.symm h), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Homeomorph.coe_toHomotopyEquiv {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : ↑(Homeomorph.toHomotopyEquiv h) = ⇑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

• ContinuousMap.HomotopyEquiv.symm h = { 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 = ↑(ContinuousMap.HomotopyEquiv.symm h)

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 = ↑(ContinuousMap.HomotopyEquiv.symm h)

@[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.symm (ContinuousMap.HomotopyEquiv.refl X)) a = a

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.toHomotopyEquiv (Homeomorph.refl X)

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

Equations

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

@[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), ↑(ContinuousMap.HomotopyEquiv.symm (ContinuousMap.HomotopyEquiv.trans h₁ h₂)) a = ↑(ContinuousMap.HomotopyEquiv.symm h₁) (↑(ContinuousMap.HomotopyEquiv.symm h₂) a)

@[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), ↑(ContinuousMap.HomotopyEquiv.trans h₁ h₂) a = ↑h₂ (↑h₁ a)

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

• ContinuousMap.HomotopyEquiv.trans h₁ h₂ = { toFun := ContinuousMap.comp h₂.toFun h₁.toFun, invFun := ContinuousMap.comp h₁.invFun h₂.invFun, left_inv := ⋯, right_inv := ⋯ }

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) : ContinuousMap.HomotopyEquiv.symm (ContinuousMap.HomotopyEquiv.trans h₁ h₂) = ContinuousMap.HomotopyEquiv.trans (ContinuousMap.HomotopyEquiv.symm h₂) (ContinuousMap.HomotopyEquiv.symm h₁)

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

• ContinuousMap.HomotopyEquiv.prodCongr h₁ h₂ = { toFun := ContinuousMap.prodMap h₁.toFun h₂.toFun, invFun := ContinuousMap.prodMap h₁.invFun 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.toHomotopyEquiv (Homeomorph.refl X) = ContinuousMap.HomotopyEquiv.refl X

@[simp]

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

@[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) : Homeomorph.toHomotopyEquiv (Homeomorph.trans h₀ h₁) = ContinuousMap.HomotopyEquiv.trans (Homeomorph.toHomotopyEquiv h₀) (Homeomorph.toHomotopyEquiv h₁)