Homotopy between paths

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, inline]

abbrev Path.Homotopy {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} (p₀ p₁ : Path x₀ x₁) : Type u

The type of homotopies between two paths.

theorem Path.Homotopy.coeFn_injective {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ : Path x₀ x₁} : Function.Injective DFunLike.coe

@[simp]

theorem Path.Homotopy.source {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ : Path x₀ x₁} (F : p₀.Homotopy p₁) (t : ↑unitInterval) : F (t, 0) = x₀

@[simp]

theorem Path.Homotopy.target {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ : Path x₀ x₁} (F : p₀.Homotopy p₁) (t : ↑unitInterval) : F (t, 1) = x₁

def Path.Homotopy.eval {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ : Path x₀ x₁} (F : p₀.Homotopy p₁) (t : ↑unitInterval) : Path x₀ x₁

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

@[simp]

theorem Path.Homotopy.eval_apply {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ : Path x₀ x₁} (F : p₀.Homotopy p₁) (t a : ↑unitInterval) : (F.eval t) a = (F.curry t) a

@[simp]

theorem Path.Homotopy.eval_zero {X : Type u} [TopologicalSpace X] {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} [TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ : Path x₀ x₁} (F : p₀.Homotopy p₁) : F.eval 1 = p₁

def Path.Homotopy.refl {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁) : p.Homotopy p

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

@[simp]

theorem Path.Homotopy.refl_apply {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁) (x : ↑unitInterval × ↑unitInterval) : (refl p) x = p x.2

def Path.Homotopy.symm {X : Type u} [TopologicalSpace X] {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.

@[simp]

theorem Path.Homotopy.symm_apply {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ : Path x₀ x₁} (F : p₀.Homotopy p₁) (x : ↑unitInterval × ↑unitInterval) : F.symm x = F (unitInterval.symm x.1, x.2)

@[simp]

theorem Path.Homotopy.symm_symm {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ : Path x₀ x₁} (F : p₀.Homotopy p₁) : F.symm.symm = F

theorem Path.Homotopy.symm_bijective {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ : Path x₀ x₁} : Function.Bijective symm

def Path.Homotopy.trans {X : Type u} [TopologicalSpace X] {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].

theorem Path.Homotopy.trans_apply {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ p₂ : Path x₀ x₁} (F : p₀.Homotopy p₁) (G : p₁.Homotopy p₂) (x : ↑unitInterval × ↑unitInterval) : (F.trans G) x = if h : ↑x.1 ≤ 1 / 2 then F (⟨2 * ↑x.1, ⋯⟩, x.2) else G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)

theorem Path.Homotopy.symm_trans {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ p₂ : Path x₀ x₁} (F : p₀.Homotopy p₁) (G : p₁.Homotopy p₂) : (F.trans G).symm = G.symm.trans F.symm

def Path.Homotopy.cast {X : Type u} [TopologicalSpace X] {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₁.

@[simp]

theorem Path.Homotopy.cast_apply {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ q₀ q₁ : Path x₀ x₁} (F : p₀.Homotopy p₁) (h₀ : p₀ = q₀) (h₁ : p₁ = q₁) (a : ↑unitInterval × ↑unitInterval) : (F.cast h₀ h₁) a = F a

def Path.Homotopy.pathCast {X : Type u} [TopologicalSpace X] {x x' y y' : X} {p q : Path x y} (F : p.Homotopy q) (hx : x' = x) (hy : y' = y) : (p.cast hx hy).Homotopy (q.cast hx hy)

If paths p and q are homotopic as paths x ⟶ y, then they are homotopic as paths x' ⟶ y', where x' = x and y' = y.

def Path.Homotopy.hcomp {X : Type u} [TopologicalSpace X] {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₁.

theorem Path.Homotopy.hcomp_apply {X : Type u} [TopologicalSpace X] {x₀ x₁ x₂ : X} {p₀ q₀ : Path x₀ x₁} {p₁ q₁ : Path x₁ x₂} (F : p₀.Homotopy q₀) (G : p₁.Homotopy q₁) (x : ↑unitInterval × ↑unitInterval) : (F.hcomp G) x = if h : ↑x.2 ≤ 1 / 2 then (F.eval x.1) ⟨2 * ↑x.2, ⋯⟩ else (G.eval x.1) ⟨2 * ↑x.2 - 1, ⋯⟩

theorem Path.Homotopy.hcomp_half {X : Type u} [TopologicalSpace X] {x₀ x₁ x₂ : X} {p₀ q₀ : Path x₀ x₁} {p₁ q₁ : Path x₁ x₂} (F : p₀.Homotopy q₀) (G : p₁.Homotopy q₁) (t : ↑unitInterval) : (F.hcomp G) (t, ⟨1 / 2, ⋯⟩) = x₁

def Path.Homotopy.reparam {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁) (f : ↑unitInterval → ↑unitInterval) (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.

def Path.Homotopy.symm₂ {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {p q : Path x₀ x₁} (F : p.Homotopy q) : p.symm.Homotopy q.symm

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

@[simp]

theorem Path.Homotopy.symm₂_apply {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {p q : Path x₀ x₁} (F : p.Homotopy q) (x : ↑unitInterval × ↑unitInterval) : F.symm₂ x = F (x.1, unitInterval.symm x.2)

def Path.Homotopy.map {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {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.

@[simp]

theorem Path.Homotopy.map_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x₀ x₁ : X} {p q : Path x₀ x₁} (F : p.Homotopy q) (f : C(X, Y)) (a✝ : ↑unitInterval × ↑unitInterval) : (F.map f) a✝ = (⇑f ∘ ⇑F) a✝

def Path.Homotopic {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} (p₀ p₁ : Path x₀ x₁) : Prop

Two paths p₀ and p₁ are Path.Homotopic if there exists a Homotopy between them.

theorem Path.Homotopic.refl {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁) : p.Homotopic p

theorem Path.Homotopic.symm {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} ⦃p₀ p₁ : Path x₀ x₁⦄ (h : p₀.Homotopic p₁) : p₁.Homotopic p₀

theorem Path.Homotopic.symm₂ {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {p q : Path x₀ x₁} (h : p.Homotopic q) : p.symm.Homotopic q.symm

theorem Path.Homotopic.trans {X : Type u} [TopologicalSpace X] {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} [TopologicalSpace X] {x₀ x₁ : X} : Equivalence Homotopic

instance Path.Homotopic.instIsEquiv {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} : IsEquiv (Path x₀ x₁) Homotopic

theorem Path.Homotopic.map {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {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} [TopologicalSpace X] {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₁)

theorem Path.Homotopic.pathCast {X : Type u} [TopologicalSpace X] {x₀ x₁ x₂ x₃ : X} {p q : Path x₀ x₁} (hpq : p.Homotopic q) (hsource : x₂ = x₀) (htarget : x₃ = x₁) : (p.cast hsource htarget).Homotopic (q.cast hsource htarget)

If paths p and q are homotopic as paths x ⟶ y, then they are homotopic as paths x' ⟶ y', where x' = x and y' = y.

def Path.Homotopic.setoid {X : Type u} [TopologicalSpace X] (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.

def Path.Homotopic.Quotient {X : Type u} [TopologicalSpace X] (x₀ x₁ : X) : Type u

The quotient on Path x₀ x₁ by the equivalence relation Path.Homotopic.

instance Path.Homotopic.instInhabitedQuotientUnitUnit : Inhabited (Homotopic.Quotient () ())

def Path.Homotopic.Quotient.mk {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁) : Homotopic.Quotient x₀ x₁

The canonical map from Path x₀ x₁ to Path.Homotopic.Quotient x₀ x₁.

theorem Path.Homotopic.Quotient.mk_surjective {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} : Function.Surjective mk

@[simp]

theorem Path.Homotopic.Quotient.mk'_eq_mk {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁) : Quotient.mk' p = mk p

Path.Homotopic.Quotient.mk is the simp normal form.

@[simp]

theorem Path.Homotopic.Quotient.mk''_eq_mk {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁) : Quotient.mk'' p = mk p

theorem Path.Homotopic.Quotient.exact {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {p q : Path x₀ x₁} (h : mk p = mk q) : p.Homotopic q

theorem Path.Homotopic.Quotient.eq {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} {p q : Path x₀ x₁} : mk p = mk q ↔ p.Homotopic q

theorem Path.Homotopic.Quotient.ind {X : Type u} [TopologicalSpace X] {x y : X} {motive : Homotopic.Quotient x y → Prop} (mk : ∀ (a : Path x y), motive (mk a)) (q : Homotopic.Quotient x y) : motive q

A reasoning principle for quotients that allows proofs about quotients to assume that all values are constructed with Quotient.mk.

theorem Path.Homotopic.Quotient.ind₂ {X : Type u} [TopologicalSpace X] {Y : Type u_1} [TopologicalSpace Y] {x₀ y₀ : X} {x₁ y₁ : Y} {motive : Homotopic.Quotient x₀ y₀ → Homotopic.Quotient x₁ y₁ → Prop} (mk : ∀ (a : Path x₀ y₀) (b : Path x₁ y₁), motive (mk a) (mk b)) (q₀ : Homotopic.Quotient x₀ y₀) (q₁ : Homotopic.Quotient x₁ y₁) : motive q₀ q₁

A reasoning principle for quotients that allows proofs about quotients to assume that all values are constructed with Quotient.mk. This is the two-variable version of ind.

def Path.Homotopic.Quotient.refl {X : Type u} [TopologicalSpace X] (x : X) : Homotopic.Quotient x x

The constant path homotopy class at a point. This is Path.refl descended to the quotient.

@[simp]

theorem Path.Homotopic.Quotient.mk_refl {X : Type u} [TopologicalSpace X] (x : X) : mk (Path.refl x) = refl x

def Path.Homotopic.Quotient.symm {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} (P : Homotopic.Quotient x₀ x₁) : Homotopic.Quotient x₁ x₀

The reverse of a path homotopy class. This is Path.symm descended to the quotient.

@[simp]

theorem Path.Homotopic.Quotient.mk_symm {X : Type u} [TopologicalSpace X] {x₀ x₁ : X} (P : Path x₀ x₁) : mk P.symm = (mk P).symm

def Path.Homotopic.Quotient.cast {X : Type u} [TopologicalSpace X] {x y : X} (γ : Homotopic.Quotient x y) {x' y' : X} (hx : x' = x) (hy : y' = y) : Homotopic.Quotient x' y'

Cast a path homotopy class using equalities of endpoints.

@[simp]

theorem Path.Homotopic.Quotient.mk_cast {X : Type u} [TopologicalSpace X] {x y : X} (P : Path x y) {x' y' : X} (hx : x' = x) (hy : y' = y) : mk (P.cast hx hy) = (mk P).cast hx hy

@[simp]

theorem Path.Homotopic.Quotient.cast_rfl_rfl {X : Type u} [TopologicalSpace X] {x y : X} (γ : Homotopic.Quotient x y) : γ.cast ⋯ ⋯ = γ

@[simp]

theorem Path.Homotopic.Quotient.cast_cast {X : Type u} [TopologicalSpace X] {x y : X} (γ : Homotopic.Quotient x y) {x' y' : X} (hx : x' = x) (hy : y' = y) {x'' y'' : X} (hx' : x'' = x') (hy' : y'' = y') : (γ.cast hx hy).cast hx' hy' = γ.cast ⋯ ⋯

def Path.Homotopic.Quotient.trans {X : Type u} [TopologicalSpace X] {x₀ x₁ x₂ : X} (P₀ : Homotopic.Quotient x₀ x₁) (P₁ : Homotopic.Quotient x₁ x₂) : Homotopic.Quotient x₀ x₂

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

@[deprecated Path.Homotopic.Quotient.trans (since := "2025-11-13")]

def Path.Homotopic.Quotient.comp {X : Type u} [TopologicalSpace X] {x₀ x₁ x₂ : X} (P₀ : Homotopic.Quotient x₀ x₁) (P₁ : Homotopic.Quotient x₁ x₂) : Homotopic.Quotient x₀ x₂

Alias of Path.Homotopic.Quotient.trans.

---

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

@[simp]

theorem Path.Homotopic.Quotient.mk_trans {X : Type u} [TopologicalSpace X] {x₀ x₁ x₂ : X} (P₀ : Path x₀ x₁) (P₁ : Path x₁ x₂) : mk (P₀.trans P₁) = (mk P₀).trans (mk P₁)

@[deprecated Path.Homotopic.Quotient.mk_trans (since := "2025-11-13")]

theorem Path.Homotopic.comp_lift {X : Type u} [TopologicalSpace X] {x₀ x₁ x₂ : X} (P₀ : Path x₀ x₁) (P₁ : Path x₁ x₂) : Quotient.mk (P₀.trans P₁) = (Quotient.mk P₀).trans (Quotient.mk P₁)

Alias of Path.Homotopic.Quotient.mk_trans.

def Path.Homotopic.Quotient.map {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x₀ x₁ : X} (P₀ : Homotopic.Quotient x₀ x₁) (f : C(X, Y)) : Homotopic.Quotient (f x₀) (f x₁)

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

@[deprecated Path.Homotopic.Quotient.map (since := "2025-11-13")]

def Path.Homotopic.Quotient.mapFn {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x₀ x₁ : X} (P₀ : Homotopic.Quotient x₀ x₁) (f : C(X, Y)) : Homotopic.Quotient (f x₀) (f x₁)

Alias of Path.Homotopic.Quotient.map.

---

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

theorem Path.Homotopic.Quotient.mk_map {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x₀ x₁ : X} (P₀ : Path x₀ x₁) (f : C(X, Y)) : mk (P₀.map ⋯) = (mk P₀).map f

@[deprecated Path.Homotopic.Quotient.mk_map (since := "2025-11-13")]

theorem Path.Homotopic.map_lift {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x₀ x₁ : X} (P₀ : Path x₀ x₁) (f : C(X, Y)) : Quotient.mk (P₀.map ⋯) = (Quotient.mk P₀).map f

Alias of Path.Homotopic.Quotient.mk_map.

theorem Path.Homotopic.hpath_hext {X : Type u} [TopologicalSpace X] {x₀ x₁ x₂ x₃ : X} {p₁ : Path x₀ x₁} {p₂ : Path x₂ x₃} (hp : ∀ (t : ↑unitInterval), p₁ t = p₂ t) : ⟦p₁⟧ ≍ ⟦p₂⟧

def Path.toHomotopyConst {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x₀ x₁ : X} (p : Path x₀ x₁) : (ContinuousMap.const Y x₀).Homotopy (ContinuousMap.const Y x₁)

A path Path x₀ x₁ generates a homotopy between constant functions fun _ ↦ x₀ and fun _ ↦ x₁.

@[simp]

theorem Path.toHomotopyConst_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x₀ x₁ : X} (p : Path x₀ x₁) (a✝ : ↑unitInterval × Y) : p.toHomotopyConst a✝ = p a✝.1

@[simp]

theorem ContinuousMap.homotopic_const_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x₀ x₁ : X} [Nonempty Y] : (const Y x₀).Homotopic (const Y x₁) ↔ Joined x₀ x₁

Two constant continuous maps with nonempty domain are homotopic if and only if their values are joined by a path in the codomain.

def ContinuousMap.Homotopy.evalAt {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {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.

@[simp]

theorem ContinuousMap.Homotopy.evalAt_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (H : f.Homotopy g) (x : X) (t : ↑unitInterval) : (H.evalAt x) t = H (t, x)

@[simp]

theorem ContinuousMap.Homotopy.pathExtend_evalAt {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (H : f.Homotopy g) (x : X) : ⇑(H.evalAt x).extend = fun (t : ℝ) => (H.extend t) x