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

@[inline, reducible]

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

The type of homotopies between two paths.

Equations

• Path.Homotopy p₀ p₁ = ContinuousMap.HomotopyRel p₀.toContinuousMap p₁.toContinuousMap {0, 1}

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

@[simp]

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

@[simp]

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

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

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

Equations

• Path.Homotopy.eval F t = { toContinuousMap := ContinuousMap.mk ⇑((ContinuousMap.Homotopy.curry F.toHomotopy) t), source' := (_ : F (t, 0) = x₀), target' := (_ : F (t, 1) = x₁) }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• Path.Homotopy.refl p = ContinuousMap.HomotopyRel.refl p.toContinuousMap {0, 1}

@[simp]

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

@[simp]

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

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

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

Equations

• Path.Homotopy.symm F = ContinuousMap.HomotopyRel.symm F

@[simp]

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

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

def Path.Homotopy.trans {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} {p₀ : Path x₀ x₁} {p₁ : Path x₀ x₁} {p₂ : Path x₀ x₁} (F : Path.Homotopy p₀ p₁) (G : Path.Homotopy p₁ p₂) : Path.Homotopy p₀ 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

• Path.Homotopy.trans F G = ContinuousMap.HomotopyRel.trans F G

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

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

@[simp]

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

@[simp]

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

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

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

Equations

• Path.Homotopy.cast F h₀ h₁ = ContinuousMap.HomotopyRel.cast F (_ : p₀.toContinuousMap = q₀.toContinuousMap) (_ : p₁.toContinuousMap = q₁.toContinuousMap)

def Path.Homotopy.hcomp {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} {x₂ : X} {p₀ : Path x₀ x₁} {q₀ : Path x₀ x₁} {p₁ : Path x₁ x₂} {q₁ : Path x₁ x₂} (F : Path.Homotopy p₀ q₀) (G : Path.Homotopy p₁ q₁) : Path.Homotopy (Path.trans p₀ p₁) (Path.trans q₀ 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

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

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

theorem Path.Homotopy.hcomp_half {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} {x₂ : X} {p₀ : Path x₀ x₁} {q₀ : Path x₀ x₁} {p₁ : Path x₁ x₂} {q₁ : Path x₁ x₂} (F : Path.Homotopy p₀ q₀) (G : Path.Homotopy p₁ q₁) (t : ↑unitInterval) : (Path.Homotopy.hcomp F G) (t, { val := 1 / 2, property := (_ : 0 ≤ 1 / 2 ∧ 1 / 2 ≤ 1) }) = x₁

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

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

def Path.Homotopy.map {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x₀ : X} {x₁ : X} {p : Path x₀ x₁} {q : Path x₀ x₁} (F : Path.Homotopy p q) (f : C(X, Y)) : Path.Homotopy (Path.map p (_ : Continuous ⇑f)) (Path.map q (_ : Continuous ⇑f))

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

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

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

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

Equations

• Path.Homotopic p₀ p₁ = Nonempty (Path.Homotopy p₀ p₁)

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

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

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

theorem Path.Homotopic.equivalence {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} : Equivalence Path.Homotopic

theorem Path.Homotopic.map {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x₀ : X} {x₁ : X} {p : Path x₀ x₁} {q : Path x₀ x₁} (h : Path.Homotopic p q) (f : C(X, Y)) : Path.Homotopic (Path.map p (_ : Continuous ⇑f)) (Path.map q (_ : Continuous ⇑f))

theorem Path.Homotopic.hcomp {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} {x₂ : X} {p₀ : Path x₀ x₁} {p₁ : Path x₀ x₁} {q₀ : Path x₁ x₂} {q₁ : Path x₁ x₂} (hp : Path.Homotopic p₀ p₁) (hq : Path.Homotopic q₀ q₁) : Path.Homotopic (Path.trans p₀ q₀) (Path.trans p₁ q₁)

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

Equations

• Path.Homotopic.setoid x₀ x₁ = { r := Path.Homotopic, iseqv := (_ : Equivalence Path.Homotopic) }

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

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

Equations

• Path.Homotopic.Quotient x₀ x₁ = Quotient (Path.Homotopic.setoid x₀ x₁)

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

Equations

• Path.Homotopic.instInhabitedQuotientUnitInstTopologicalSpacePUnitUnit = { default := Quotient.mk' (Path.refl ()) }

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

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

Equations

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

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

def Path.Homotopic.Quotient.mapFn {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x₀ : X} {x₁ : X} (P₀ : Path.Homotopic.Quotient x₀ x₁) (f : C(X, Y)) : Path.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.

Equations

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

theorem Path.Homotopic.map_lift {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x₀ : X} {x₁ : X} (P₀ : Path x₀ x₁) (f : C(X, Y)) : ⟦Path.map P₀ (_ : Continuous ⇑f)⟧ = Path.Homotopic.Quotient.mapFn ⟦P₀⟧ f

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

@[simp]

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

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

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

Equations

• Path.toHomotopyConst p = { toContinuousMap := ContinuousMap.comp p.toContinuousMap ContinuousMap.fst, map_zero_left := (_ : Y → p 0 = x₀), map_one_left := (_ : Y → p 1 = x₁) }

@[simp]

theorem ContinuousMap.homotopic_const_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x₀ : X} {x₁ : X} [Nonempty Y] : ContinuousMap.Homotopic (ContinuousMap.const Y x₀) (ContinuousMap.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_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {g : C(X, Y)} (H : ContinuousMap.Homotopy f 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

• ContinuousMap.Homotopy.evalAt H x = { toContinuousMap := ContinuousMap.mk fun (t : ↑unitInterval) => H (t, x), source' := (_ : H (0, x) = f x), target' := (_ : H (1, x) = g x) }