# mathlib3documentation

topology.homotopy.path

# Homotopy between paths #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file, we define a homotopy between two paths. In addition, we define a relation homotopic on paths, and prove that it is an equivalence relation.

## Definitions #

• path.homotopy p₀ p₁ is the type of homotopies between paths p₀ and p₁
• path.homotopy.refl p is the constant homotopy between p and itself
• path.homotopy.symm F is the path.homotopy p₁ p₀ defined by reversing the homotopy
• path.homotopy.trans F G, where F : path.homotopy p₀ p₁, G : path.homotopy p₁ p₂ is the path.homotopy p₀ p₂ defined by putting the first homotopy on [0, 1/2] and the second on [1/2, 1]
• path.homotopy.hcomp F G, where F : path.homotopy p₀ q₀ and G : path.homotopy p₁ q₁ is a path.homotopy (p₀.trans p₁) (q₀.trans q₁)
• path.homotopic p₀ p₁ is the relation saying that there is a homotopy between p₀ and p₁
• path.homotopic.setoid x₀ x₁ is the setoid on paths from path.homotopic
• path.homotopic.quotient x₀ x₁ is the quotient type from path x₀ x₀ by path.homotopic.setoid
@[reducible]
def path.homotopy {X : Type u} {x₀ x₁ : X} (p₀ p₁ : path x₀ x₁) :

The type of homotopies between two paths.

@[protected, instance]
def path.homotopy.has_coe_to_fun {X : Type u} {x₀ x₁ : X} {p₀ p₁ : path x₀ x₁} :
has_coe_to_fun (p₀.homotopy p₁) (λ (_x : p₀.homotopy p₁),
Equations
theorem path.homotopy.coe_fn_injective {X : Type u} {x₀ x₁ : X} {p₀ p₁ : path x₀ x₁} :
@[simp]
theorem path.homotopy.source {X : Type u} {x₀ x₁ : X} {p₀ p₁ : path x₀ x₁} (F : p₀.homotopy p₁) (t : unit_interval) :
F (t, 0) = x₀
@[simp]
theorem path.homotopy.target {X : Type u} {x₀ x₁ : X} {p₀ p₁ : path x₀ x₁} (F : p₀.homotopy p₁) (t : unit_interval) :
F (t, 1) = x₁
def path.homotopy.eval {X : Type u} {x₀ x₁ : X} {p₀ p₁ : path x₀ x₁} (F : p₀.homotopy p₁) (t : unit_interval) :
path x₀ x₁

Evaluating a path homotopy at an intermediate point, giving us a path.

Equations
@[simp]
theorem path.homotopy.eval_zero {X : Type u} {x₀ x₁ : X} {p₀ p₁ : path x₀ x₁} (F : p₀.homotopy p₁) :
F.eval 0 = p₀
@[simp]
theorem path.homotopy.eval_one {X : Type u} {x₀ x₁ : X} {p₀ p₁ : path x₀ x₁} (F : p₀.homotopy p₁) :
F.eval 1 = p₁
@[simp]
theorem path.homotopy.refl_apply {X : Type u} {x₀ x₁ : X} (p : path x₀ x₁)  :
x = p x.snd
@[simp]
theorem path.homotopy.refl_to_homotopy {X : Type u} {x₀ x₁ : X} (p : path x₀ x₁) :
def path.homotopy.refl {X : Type u} {x₀ x₁ : X} (p : path x₀ x₁) :

Given a path p, we can define a homotopy p p by F (t, x) = p x

Equations
def path.homotopy.symm {X : Type u} {x₀ x₁ : X} {p₀ p₁ : path x₀ x₁} (F : p₀.homotopy p₁) :
p₁.homotopy p₀

Given a homotopy p₀ p₁, we can define a homotopy p₁ p₀ by reversing the homotopy.

Equations
@[simp]
theorem path.homotopy.symm_apply {X : Type u} {x₀ x₁ : X} {p₀ p₁ : path x₀ x₁} (F : p₀.homotopy p₁)  :
(F.symm) x = F , x.snd)
@[simp]
theorem path.homotopy.symm_to_homotopy {X : Type u} {x₀ x₁ : X} {p₀ p₁ : path x₀ x₁} (F : p₀.homotopy p₁) :
@[simp]
theorem path.homotopy.symm_symm {X : Type u} {x₀ x₁ : X} {p₀ p₁ : path x₀ x₁} (F : p₀.homotopy p₁) :
F.symm.symm = F
noncomputable def path.homotopy.trans {X : Type u} {x₀ x₁ : X} {p₀ p₁ p₂ : path x₀ x₁} (F : p₀.homotopy p₁) (G : p₁.homotopy p₂) :
p₀.homotopy p₂

Given homotopy p₀ p₁ and homotopy p₁ p₂, we can define a homotopy p₀ p₂ by putting the first homotopy on [0, 1/2] and the second on [1/2, 1].

Equations
theorem path.homotopy.trans_apply {X : Type u} {x₀ x₁ : X} {p₀ p₁ p₂ : path x₀ x₁} (F : p₀.homotopy p₁) (G : p₁.homotopy p₂)  :
(F.trans G) x = dite ((x.fst) 1 / 2) (λ (h : (x.fst) 1 / 2), F (2 * (x.fst), _⟩, x.snd)) (λ (h : ¬(x.fst) 1 / 2), G (2 * (x.fst) - 1, _⟩, x.snd))
theorem path.homotopy.symm_trans {X : Type u} {x₀ x₁ : X} {p₀ p₁ p₂ : path x₀ x₁} (F : p₀.homotopy p₁) (G : p₁.homotopy p₂) :
def path.homotopy.cast {X : Type u} {x₀ x₁ : X} {p₀ p₁ q₀ q₁ : path x₀ x₁} (F : p₀.homotopy p₁) (h₀ : p₀ = q₀) (h₁ : p₁ = q₁) :
q₀.homotopy q₁

Casting a homotopy p₀ p₁ to a homotopy q₀ q₁ where p₀ = q₀ and p₁ = q₁.

Equations
@[simp]
theorem path.homotopy.cast_apply {X : Type u} {x₀ x₁ : X} {p₀ p₁ q₀ q₁ : path x₀ x₁} (F : p₀.homotopy p₁) (h₀ : p₀ = q₀) (h₁ : p₁ = q₁)  :
(F.cast h₀ h₁) = F ᾰ
@[simp]
theorem path.homotopy.cast_to_homotopy {X : Type u} {x₀ x₁ : X} {p₀ p₁ q₀ q₁ : path x₀ x₁} (F : p₀.homotopy p₁) (h₀ : p₀ = q₀) (h₁ : p₁ = q₁) :
(F.cast h₀ h₁).to_homotopy = F.to_homotopy.cast _ _
noncomputable def path.homotopy.hcomp {X : Type u} {x₀ x₁ x₂ : X} {p₀ q₀ : path x₀ x₁} {p₁ q₁ : path x₁ x₂} (F : p₀.homotopy q₀) (G : p₁.homotopy q₁) :
(p₀.trans p₁).homotopy (q₀.trans q₁)

Suppose p₀ and q₀ are paths from x₀ to x₁, p₁ and q₁ are paths from x₁ to x₂. Furthermore, suppose F : homotopy p₀ q₀ and G : homotopy p₁ q₁. Then we can define a homotopy from p₀.trans p₁ to q₀.trans q₁.

Equations
theorem path.homotopy.hcomp_apply {X : Type u} {x₀ x₁ x₂ : X} {p₀ q₀ : path x₀ x₁} {p₁ q₁ : path x₁ x₂} (F : p₀.homotopy q₀) (G : p₁.homotopy q₁)  :
(F.hcomp G) x = dite ((x.snd) 1 / 2) (λ (h : (x.snd) 1 / 2), (F.eval x.fst) 2 * (x.snd), _⟩) (λ (h : ¬(x.snd) 1 / 2), (G.eval x.fst) 2 * (x.snd) - 1, _⟩)
theorem path.homotopy.hcomp_half {X : Type u} {x₀ x₁ x₂ : X} {p₀ q₀ : path x₀ x₁} {p₁ q₁ : path x₁ x₂} (F : p₀.homotopy q₀) (G : p₁.homotopy q₁) (t : unit_interval) :
(F.hcomp G) (t, 1 / 2, _⟩) = x₁
def path.homotopy.reparam {X : Type u} {x₀ x₁ : X} (p : path x₀ x₁) (hf : continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) :
p.homotopy (p.reparam f hf hf₀ hf₁)

Suppose p is a path, then we have a homotopy from p to p.reparam f by the convexity of I.

Equations
def path.homotopy.symm₂ {X : Type u} {x₀ x₁ : X} {p q : path x₀ x₁} (F : p.homotopy q) :

Suppose F : homotopy p q. Then we have a homotopy p.symm q.symm by reversing the second argument.

Equations
@[simp]
theorem path.homotopy.symm₂_apply {X : Type u} {x₀ x₁ : X} {p q : path x₀ x₁} (F : p.homotopy q)  :
(F.symm₂) x = F (x.fst,
@[simp]
theorem path.homotopy.symm₂_to_homotopy_apply {X : Type u} {x₀ x₁ : X} {p q : path x₀ x₁} (F : p.homotopy q)  :
@[simp]
theorem path.homotopy.map_apply {X : Type u} {Y : Type v} {x₀ x₁ : X} {p q : path x₀ x₁} (F : p.homotopy q) (f : C(X, Y))  :
(F.map f) = (f F)
@[simp]
theorem path.homotopy.map_to_homotopy_apply {X : Type u} {Y : Type v} {x₀ x₁ : X} {p q : path x₀ x₁} (F : p.homotopy q) (f : C(X, Y))  :
((F.map f).to_homotopy) = (f F)
def path.homotopy.map {X : Type u} {Y : Type v} {x₀ x₁ : X} {p q : path x₀ x₁} (F : p.homotopy q) (f : C(X, Y)) :
(p.map _).homotopy (q.map _)

Given F : homotopy p q, and f : C(X, Y), we can define a homotopy from p.map f.continuous to q.map f.continuous.

Equations
def path.homotopic {X : Type u} {x₀ x₁ : X} (p₀ p₁ : path x₀ x₁) :
Prop

Two paths p₀ and p₁ are path.homotopic if there exists a homotopy between them.

Equations
@[refl]
theorem path.homotopic.refl {X : Type u} {x₀ x₁ : X} (p : path x₀ x₁) :
@[symm]
theorem path.homotopic.symm {X : Type u} {x₀ x₁ : X} ⦃p₀ p₁ : path x₀ x₁⦄ (h : p₀.homotopic p₁) :
p₁.homotopic p₀
@[trans]
theorem path.homotopic.trans {X : Type u} {x₀ x₁ : X} ⦃p₀ p₁ p₂ : path x₀ x₁⦄ (h₀ : p₀.homotopic p₁) (h₁ : p₁.homotopic p₂) :
p₀.homotopic p₂
theorem path.homotopic.equivalence {X : Type u} {x₀ x₁ : X} :
theorem path.homotopic.map {X : Type u} {Y : Type v} {x₀ x₁ : X} {p q : path x₀ x₁} (h : p.homotopic q) (f : C(X, Y)) :
(p.map _).homotopic (q.map _)
theorem path.homotopic.hcomp {X : Type u} {x₀ x₁ x₂ : X} {p₀ p₁ : path x₀ x₁} {q₀ q₁ : path x₁ x₂} (hp : p₀.homotopic p₁) (hq : q₀.homotopic q₁) :
(p₀.trans q₀).homotopic (p₁.trans q₁)
@[protected]
def path.homotopic.setoid {X : Type u} (x₀ x₁ : X) :
setoid (path x₀ x₁)

The setoid on paths defined by the equivalence relation path.homotopic. That is, two paths are equivalent if there is a homotopy between them.

Equations
@[protected]
def path.homotopic.quotient {X : Type u} (x₀ x₁ : X) :

The quotient on path x₀ x₁ by the equivalence relation path.homotopic.

Equations
Instances for path.homotopic.quotient
@[protected, instance]
Equations
noncomputable def path.homotopic.quotient.comp {X : Type u} {x₀ x₁ x₂ : X} (P₀ : x₁) (P₁ : x₂) :

The composition of path homotopy classes. This is path.trans descended to the quotient.

Equations
• P₀.comp P₁ = path.homotopic.quotient.comp._proof_1 P₀ P₁
theorem path.homotopic.comp_lift {X : Type u} {x₀ x₁ x₂ : X} (P₀ : path x₀ x₁) (P₁ : path x₁ x₂) :
P₀.trans P₁ =
def path.homotopic.quotient.map_fn {X : Type u} {Y : Type v} {x₀ x₁ : X} (P₀ : x₁) (f : C(X, Y)) :

The image of a path homotopy class P₀ under a map f. This is path.map descended to the quotient

Equations
theorem path.homotopic.map_lift {X : Type u} {Y : Type v} {x₀ x₁ : X} (P₀ : path x₀ x₁) (f : C(X, Y)) :
P₀.map _ =
theorem path.homotopic.hpath_hext {X : Type u} {x₀ x₁ x₂ x₃ : X} {p₁ : path x₀ x₁} {p₂ : path x₂ x₃} (hp : (t : unit_interval), p₁ t = p₂ t) :
p₁ == p₂
def continuous_map.homotopy.eval_at {X : Type u_1} {Y : Type u_2} {f g : C(X, Y)} (H : f.homotopy g) (x : X) :
path (f x) (g x)

Given a homotopy H: f ∼ g, get the path traced by the point x as it moves from f x to g x

Equations