Documentation

Mathlib.Topology.Homotopy.Path

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 #

@[reducible, inline]
abbrev Path.Homotopy {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} (p₀ : Path x₀ x₁) (p₁ : Path x₀ x₁) :
Type (max 0 u)

The type of homotopies between two paths.

Equations
  • p₀.Homotopy p₁ = p₀.HomotopyRel 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 : p₀.Homotopy 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 : p₀.Homotopy 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 : p₀.Homotopy p₁) (t : unitInterval) :
Path x₀ x₁

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

Equations
  • F.eval t = { toFun := (F.curry t), continuous_toFun := , source' := , target' := }
@[simp]
theorem Path.Homotopy.eval_zero {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} {p₀ : Path x₀ x₁} {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₁ : X} {p₀ : Path x₀ x₁} {p₁ : Path x₀ x₁} (F : p₀.Homotopy p₁) :
F.eval 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₁) :
p.Homotopy p

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

Equations
@[simp]
theorem Path.Homotopy.symm_apply {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} {p₀ : Path x₀ x₁} {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_toFun {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} {p₀ : Path x₀ x₁} {p₁ : Path x₀ x₁} (F : p₀.Homotopy p₁) (x : unitInterval × unitInterval) :
F.symm 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 : 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_symm {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} {p₀ : Path x₀ x₁} {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₁ : 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 : 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} [TopologicalSpace X] {x₀ : X} {x₁ : X} {p₀ : Path x₀ x₁} {p₁ : Path x₀ x₁} {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₁ : X} {p₀ : Path x₀ x₁} {p₁ : Path x₀ x₁} {p₂ : Path x₀ x₁} (F : p₀.Homotopy p₁) (G : p₁.Homotopy p₂) :
(F.trans G).symm = G.symm.trans F.symm
@[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 : p₀.Homotopy p₁) (h₀ : p₀ = q₀) (h₁ : p₁ = q₁) (a : unitInterval × unitInterval) :
(F.cast 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 : p₀.Homotopy p₁) (h₀ : p₀ = q₀) (h₁ : p₁ = q₁) (a : unitInterval × unitInterval) :
(F.cast 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 : 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
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 : 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
  • 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 : 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} {x₂ : X} {p₀ : Path x₀ x₁} {q₀ : Path x₀ x₁} {p₁ : Path x₁ x₂} {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₁ : X} (p : Path x₀ x₁) (f : unitIntervalunitInterval) (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
  • 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 : p.Homotopy q) (x : unitInterval × unitInterval) :
F.symm₂ 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 : p.Homotopy q) (x : unitInterval × unitInterval) :
F.symm₂ 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 : 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.

Equations
@[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 : p.Homotopy q) (f : C(X, Y)) :
∀ (a : unitInterval × unitInterval), (F.map 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 : p.Homotopy q) (f : C(X, Y)) :
∀ (a : unitInterval × unitInterval), (F.map 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 : 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
  • F.map f = { toFun := f F, continuous_toFun := , map_zero_left := , map_one_left := , prop' := }
def Path.Homotopic {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} (p₀ : Path x₀ x₁) (p₁ : Path x₀ x₁) :

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

Equations
  • p₀.Homotopic p₁ = Nonempty (p₀.Homotopy p₁)
theorem Path.Homotopic.refl {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} (p : Path x₀ x₁) :
p.Homotopic p
theorem Path.Homotopic.symm {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} ⦃p₀ : Path x₀ x₁ ⦃p₁ : Path x₀ x₁ (h : p₀.Homotopic p₁) :
p₁.Homotopic 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₀ : p₀.Homotopic p₁) (h₁ : p₁.Homotopic p₂) :
p₀.Homotopic 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 : 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} {x₂ : X} {p₀ : Path x₀ x₁} {p₁ : Path x₀ x₁} {q₀ : Path x₁ x₂} {q₁ : Path x₁ x₂} (hp : p₀.Homotopic p₁) (hq : q₀.Homotopic q₁) :
(p₀.trans q₀).Homotopic (p₁.trans 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
def Path.Homotopic.Quotient {X : Type u} [TopologicalSpace X] (x₀ : X) (x₁ : X) :

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

Equations
Instances For
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₂) :

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

Equations
theorem Path.Homotopic.comp_lift {X : Type u} [TopologicalSpace X] {x₀ : X} {x₁ : X} {x₂ : X} (P₀ : Path x₀ x₁) (P₁ : Path x₁ x₂) :
P₀.trans 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
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)) :
P₀.map = 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), p.toHomotopyConst 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.const Y x₀).Homotopy (ContinuousMap.const Y x₁)

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

Equations
  • p.toHomotopyConst = { toContinuousMap := p.comp ContinuousMap.fst, map_zero_left := , map_one_left := }
@[simp]
theorem ContinuousMap.homotopic_const_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x₀ : X} {x₁ : X} [Nonempty Y] :
(ContinuousMap.const Y x₀).Homotopic (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 : 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
  • H.evalAt x = { toFun := fun (t : unitInterval) => H (t, x), continuous_toFun := , source' := , target' := }