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.

source

theorem continuous_map.homotopy_equiv.ext {X : Type u} {Y : Type v} {_inst_4 : topological_space X} {_inst_5 : topological_space Y} (x y : continuous_map.homotopy_equiv X Y) (h : x.to_fun = y.to_fun) (h_1 : x.inv_fun = y.inv_fun) :

x = y

source

@[ext]

structure continuous_map.homotopy_equiv (X : Type u) (Y : Type v) [topological_space X] [topological_space Y] :

Type (max u v)

to_fun : C(X, Y)
inv_fun : C(Y, X)
left_inv : (self.inv_fun.comp self.to_fun).homotopic (continuous_map.id X)
right_inv : (self.to_fun.comp self.inv_fun).homotopic (continuous_map.id Y)

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

continuous_map.homotopy_equiv.has_sizeof_inst
continuous_map.homotopy_equiv.has_coe_to_fun
continuous_map.homotopy_equiv.inhabited

source

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 : continuous_map.homotopy_equiv X Y) :

x = y ↔ x.to_fun = y.to_fun ∧ x.inv_fun = y.inv_fun

source

@[protected, instance]

def continuous_map.homotopy_equiv.has_coe_to_fun {X : Type u} {Y : Type v} [topological_space X] [topological_space Y] :

has_coe_to_fun (continuous_map.homotopy_equiv X Y) (λ (_x : continuous_map.homotopy_equiv X Y), X → Y)

Equations

continuous_map.homotopy_equiv.has_coe_to_fun = {coe := λ (h : continuous_map.homotopy_equiv X Y), ⇑(h.to_fun)}

source

@[simp]

theorem continuous_map.homotopy_equiv.to_fun_eq_coe {X : Type u} {Y : Type v} [topological_space X] [topological_space Y] (h : continuous_map.homotopy_equiv X Y) :

⇑(h.to_fun) = ⇑h

source

@[continuity]

theorem continuous_map.homotopy_equiv.continuous {X : Type u} {Y : Type v} [topological_space X] [topological_space Y] (h : continuous_map.homotopy_equiv X Y) :

continuous ⇑h

source

def homeomorph.to_homotopy_equiv {X : Type u} {Y : Type v} [topological_space X] [topological_space Y] (h : X ≃ₜ Y) :

continuous_map.homotopy_equiv X Y

Any homeomorphism is a homotopy equivalence.

Equations

h.to_homotopy_equiv = {to_fun := {to_fun := ⇑h, continuous_to_fun := _}, inv_fun := {to_fun := ⇑(h.symm), continuous_to_fun := _}, left_inv := _, right_inv := _}

source

@[simp]

theorem homeomorph.coe_to_homotopy_equiv {X : Type u} {Y : Type v} [topological_space X] [topological_space Y] (h : X ≃ₜ Y) :

⇑(h.to_homotopy_equiv) = ⇑h

source

def continuous_map.homotopy_equiv.symm {X : Type u} {Y : Type v} [topological_space X] [topological_space Y] (h : continuous_map.homotopy_equiv X Y) :

continuous_map.homotopy_equiv Y X

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

Equations

h.symm = {to_fun := h.inv_fun, inv_fun := h.to_fun, left_inv := _, right_inv := _}

source

@[simp]

theorem continuous_map.homotopy_equiv.coe_inv_fun {X : Type u} {Y : Type v} [topological_space X] [topological_space Y] (h : continuous_map.homotopy_equiv X Y) :

⇑(h.inv_fun) = ⇑(h.symm)

source

def continuous_map.homotopy_equiv.simps.apply {X : Type u} {Y : Type v} [topological_space X] [topological_space Y] (h : continuous_map.homotopy_equiv 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

continuous_map.homotopy_equiv.simps.apply h = ⇑h

source

def continuous_map.homotopy_equiv.simps.symm_apply {X : Type u} {Y : Type v} [topological_space X] [topological_space Y] (h : continuous_map.homotopy_equiv 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

continuous_map.homotopy_equiv.simps.symm_apply h = ⇑(h.symm)

source

def continuous_map.homotopy_equiv.refl (X : Type u) [topological_space X] :

continuous_map.homotopy_equiv X X

Any topological space is homotopy equivalent to itself.

Equations

continuous_map.homotopy_equiv.refl X = (homeomorph.refl X).to_homotopy_equiv

source

@[simp]

theorem continuous_map.homotopy_equiv.refl_symm_apply (X : Type u) [topological_space X] (ᾰ : X) :

⇑((continuous_map.homotopy_equiv.refl X).symm) ᾰ = ᾰ

source

@[simp]

theorem continuous_map.homotopy_equiv.refl_apply (X : Type u) [topological_space X] (ᾰ : X) :

⇑(continuous_map.homotopy_equiv.refl X) ᾰ = ᾰ

source

@[protected, instance]

def continuous_map.homotopy_equiv.inhabited :

inhabited (continuous_map.homotopy_equiv unit unit)

Equations

continuous_map.homotopy_equiv.inhabited = {default := continuous_map.homotopy_equiv.refl unit punit.topological_space}

source

def continuous_map.homotopy_equiv.trans {X : Type u} {Y : Type v} {Z : Type w} [topological_space X] [topological_space Y] [topological_space Z] (h₁ : continuous_map.homotopy_equiv X Y) (h₂ : continuous_map.homotopy_equiv Y Z) :

continuous_map.homotopy_equiv 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₂ = {to_fun := h₂.to_fun.comp h₁.to_fun, inv_fun := h₁.inv_fun.comp h₂.inv_fun, left_inv := _, right_inv := _}

source

@[simp]

theorem continuous_map.homotopy_equiv.trans_symm_apply {X : Type u} {Y : Type v} {Z : Type w} [topological_space X] [topological_space Y] [topological_space Z] (h₁ : continuous_map.homotopy_equiv X Y) (h₂ : continuous_map.homotopy_equiv Y Z) (ᾰ : Z) :

⇑((h₁.trans h₂).symm) ᾰ = ⇑(h₁.symm) (⇑(h₂.symm) ᾰ)

source

@[simp]

theorem continuous_map.homotopy_equiv.trans_apply {X : Type u} {Y : Type v} {Z : Type w} [topological_space X] [topological_space Y] [topological_space Z] (h₁ : continuous_map.homotopy_equiv X Y) (h₂ : continuous_map.homotopy_equiv Y Z) (ᾰ : X) :

⇑(h₁.trans h₂) ᾰ = ⇑h₂ (⇑h₁ ᾰ)

source

theorem continuous_map.homotopy_equiv.symm_trans {X : Type u} {Y : Type v} {Z : Type w} [topological_space X] [topological_space Y] [topological_space Z] (h₁ : continuous_map.homotopy_equiv X Y) (h₂ : continuous_map.homotopy_equiv Y Z) :

(h₁.trans h₂).symm = h₂.symm.trans h₁.symm

source

@[simp]

theorem homeomorph.refl_to_homotopy_equiv (X : Type u) [topological_space X] :

(homeomorph.refl X).to_homotopy_equiv = continuous_map.homotopy_equiv.refl X

source

@[simp]

theorem homeomorph.symm_to_homotopy_equiv {X : Type u} {Y : Type v} [topological_space X] [topological_space Y] (h : X ≃ₜ Y) :

h.symm.to_homotopy_equiv = h.to_homotopy_equiv.symm

source

@[simp]

theorem homeomorph.trans_to_homotopy_equiv {X : Type u} {Y : Type v} {Z : Type w} [topological_space X] [topological_space Y] [topological_space Z] (h₀ : X ≃ₜ Y) (h₁ : Y ≃ₜ Z) :

(h₀.trans h₁).to_homotopy_equiv = h₀.to_homotopy_equiv.trans h₁.to_homotopy_equiv