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 pathsp₀andp₁path.homotopy.refl pis the constant homotopy betweenpand itselfpath.homotopy.symm Fis thepath.homotopy p₁ p₀defined by reversing the homotopypath.homotopy.trans F G, whereF : path.homotopy p₀ p₁,G : path.homotopy p₁ p₂is thepath.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, whereF : path.homotopy p₀ q₀andG : path.homotopy p₁ q₁is apath.homotopy (p₀.trans p₁) (q₀.trans q₁)path.homotopic p₀ p₁is the relation saying that there is a homotopy betweenp₀andp₁path.homotopic.setoid x₀ x₁is the setoid onpaths frompath.homotopicpath.homotopic.quotient x₀ x₁is the quotient type frompath x₀ x₀bypath.homotopic.setoid
@[reducible]
The type of homotopies between two paths.
@[protected, instance]
def
path.homotopy.has_coe_to_fun
{X : Type u}
[topological_space X]
{x₀ x₁ : X}
{p₀ p₁ : path x₀ x₁} :
has_coe_to_fun (p₀.homotopy p₁) (λ (_x : p₀.homotopy p₁), ↥unit_interval × ↥unit_interval → X)
Equations
- path.homotopy.has_coe_to_fun = {coe := λ (F : p₀.homotopy p₁), F.to_homotopy.to_continuous_map.to_fun}
theorem
path.homotopy.coe_fn_injective
{X : Type u}
[topological_space X]
{x₀ x₁ : X}
{p₀ p₁ : path x₀ x₁} :
@[simp]
theorem
path.homotopy.source
{X : Type u}
[topological_space X]
{x₀ x₁ : X}
{p₀ p₁ : path x₀ x₁}
(F : p₀.homotopy p₁)
(t : ↥unit_interval) :
@[simp]
theorem
path.homotopy.target
{X : Type u}
[topological_space X]
{x₀ x₁ : X}
{p₀ p₁ : path x₀ x₁}
(F : p₀.homotopy p₁)
(t : ↥unit_interval) :
def
path.homotopy.eval
{X : Type u}
[topological_space X]
{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
- F.eval t = {to_continuous_map := {to_fun := ⇑(⇑(F.to_homotopy.curry) t), continuous_to_fun := _}, source' := _, target' := _}
@[simp]
theorem
path.homotopy.eval_zero
{X : Type u}
[topological_space X]
{x₀ x₁ : X}
{p₀ p₁ : path x₀ x₁}
(F : p₀.homotopy p₁) :
@[simp]
theorem
path.homotopy.eval_one
{X : Type u}
[topological_space X]
{x₀ x₁ : X}
{p₀ p₁ : path x₀ x₁}
(F : p₀.homotopy p₁) :
@[simp]
theorem
path.homotopy.refl_apply
{X : Type u}
[topological_space X]
{x₀ x₁ : X}
(p : path x₀ x₁)
(x : ↥unit_interval × ↥unit_interval) :
⇑(path.homotopy.refl p) x = ⇑p x.snd
@[simp]
theorem
path.homotopy.refl_to_homotopy
{X : Type u}
[topological_space X]
{x₀ x₁ : X}
(p : path x₀ x₁) :
def
path.homotopy.refl
{X : Type u}
[topological_space 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
def
path.homotopy.symm
{X : Type u}
[topological_space 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.
Equations
@[simp]
theorem
path.homotopy.symm_apply
{X : Type u}
[topological_space X]
{x₀ x₁ : X}
{p₀ p₁ : path x₀ x₁}
(F : p₀.homotopy p₁)
(x : ↥unit_interval × ↥unit_interval) :
@[simp]
theorem
path.homotopy.symm_to_homotopy
{X : Type u}
[topological_space X]
{x₀ x₁ : X}
{p₀ p₁ : path x₀ x₁}
(F : p₀.homotopy p₁) :
F.symm.to_homotopy = F.to_homotopy.symm
@[simp]
theorem
path.homotopy.symm_symm
{X : Type u}
[topological_space X]
{x₀ x₁ : X}
{p₀ p₁ : path x₀ x₁}
(F : p₀.homotopy p₁) :
noncomputable
def
path.homotopy.trans
{X : Type u}
[topological_space 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].
Equations
- F.trans G = continuous_map.homotopy_rel.trans F G
theorem
path.homotopy.trans_apply
{X : Type u}
[topological_space X]
{x₀ x₁ : X}
{p₀ p₁ p₂ : path x₀ x₁}
(F : p₀.homotopy p₁)
(G : p₁.homotopy p₂)
(x : ↥unit_interval × ↥unit_interval) :
def
path.homotopy.cast
{X : Type u}
[topological_space 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₁.
Equations
- F.cast h₀ h₁ = continuous_map.homotopy_rel.cast F _ _
@[simp]
theorem
path.homotopy.cast_apply
{X : Type u}
[topological_space X]
{x₀ x₁ : X}
{p₀ p₁ q₀ q₁ : path x₀ x₁}
(F : p₀.homotopy p₁)
(h₀ : p₀ = q₀)
(h₁ : p₁ = q₁)
(ᾰ : ↥unit_interval × ↥unit_interval) :
@[simp]
theorem
path.homotopy.cast_to_homotopy
{X : Type u}
[topological_space X]
{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}
[topological_space X]
{x₀ x₁ x₂ : X}
{p₀ q₀ : path x₀ x₁}
{p₁ q₁ : path x₁ x₂}
(F : p₀.homotopy q₀)
(G : p₁.homotopy 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
- F.hcomp G = {to_homotopy := {to_continuous_map := {to_fun := λ (x : ↥unit_interval × ↥unit_interval), ite (↑(x.snd) ≤ 1 / 2) ((F.eval x.fst).extend (2 * ↑(x.snd))) ((G.eval x.fst).extend (2 * ↑(x.snd) - 1)), continuous_to_fun := _}, map_zero_left' := _, map_one_left' := _}, prop' := _}
theorem
path.homotopy.hcomp_apply
{X : Type u}
[topological_space X]
{x₀ x₁ x₂ : X}
{p₀ q₀ : path x₀ x₁}
{p₁ q₁ : path x₁ x₂}
(F : p₀.homotopy q₀)
(G : p₁.homotopy q₁)
(x : ↥unit_interval × ↥unit_interval) :
theorem
path.homotopy.hcomp_half
{X : Type u}
[topological_space X]
{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) :
def
path.homotopy.reparam
{X : Type u}
[topological_space X]
{x₀ x₁ : X}
(p : path x₀ x₁)
(f : ↥unit_interval → ↥unit_interval)
(hf : continuous f)
(hf₀ : f 0 = 0)
(hf₁ : f 1 = 1) :
Suppose p is a path, then we have a homotopy from p to p.reparam f by the convexity of I.
Equations
- path.homotopy.reparam p f hf hf₀ hf₁ = {to_homotopy := {to_continuous_map := {to_fun := λ (x : ↥unit_interval × ↥unit_interval), ⇑p ⟨↑(unit_interval.symm x.fst) * ↑(x.snd) + ↑(x.fst) * ↑(f x.snd), _⟩, continuous_to_fun := _}, map_zero_left' := _, map_one_left' := _}, prop' := _}
def
path.homotopy.symm₂
{X : Type u}
[topological_space X]
{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
- F.symm₂ = {to_homotopy := {to_continuous_map := {to_fun := λ (x : ↥unit_interval × ↥unit_interval), ⇑F (x.fst, unit_interval.symm x.snd), continuous_to_fun := _}, map_zero_left' := _, map_one_left' := _}, prop' := _}
@[simp]
theorem
path.homotopy.symm₂_apply
{X : Type u}
[topological_space X]
{x₀ x₁ : X}
{p q : path x₀ x₁}
(F : p.homotopy q)
(x : ↥unit_interval × ↥unit_interval) :
@[simp]
theorem
path.homotopy.symm₂_to_homotopy_apply
{X : Type u}
[topological_space X]
{x₀ x₁ : X}
{p q : path x₀ x₁}
(F : p.homotopy q)
(x : ↥unit_interval × ↥unit_interval) :
⇑(F.symm₂.to_homotopy) x = ⇑F (x.fst, unit_interval.symm x.snd)
@[simp]
theorem
path.homotopy.map_apply
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{x₀ x₁ : X}
{p q : path x₀ x₁}
(F : p.homotopy q)
(f : C(X, Y))
(ᾰ : ↥unit_interval × ↥unit_interval) :
@[simp]
theorem
path.homotopy.map_to_homotopy_apply
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{x₀ x₁ : X}
{p q : path x₀ x₁}
(F : p.homotopy q)
(f : C(X, Y))
(ᾰ : ↥unit_interval × ↥unit_interval) :
def
path.homotopy.map
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{x₀ x₁ : X}
{p q : path x₀ x₁}
(F : p.homotopy q)
(f : C(X, Y)) :
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 = {to_homotopy := {to_continuous_map := {to_fun := ⇑f ∘ ⇑F, continuous_to_fun := _}, map_zero_left' := _, map_one_left' := _}, prop' := _}
Two paths p₀ and p₁ are path.homotopic if there exists a homotopy between them.
@[refl]
theorem
path.homotopic.refl
{X : Type u}
[topological_space X]
{x₀ x₁ : X}
(p : path x₀ x₁) :
p.homotopic p
@[symm]
theorem
path.homotopic.symm
{X : Type u}
[topological_space X]
{x₀ x₁ : X}
⦃p₀ p₁ : path x₀ x₁⦄
(h : p₀.homotopic p₁) :
p₁.homotopic p₀
@[trans]
theorem
path.homotopic.trans
{X : Type u}
[topological_space X]
{x₀ x₁ : X}
⦃p₀ p₁ p₂ : path x₀ x₁⦄
(h₀ : p₀.homotopic p₁)
(h₁ : p₁.homotopic p₂) :
p₀.homotopic p₂
theorem
path.homotopic.map
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{x₀ x₁ : X}
{p q : path x₀ x₁}
(h : p.homotopic q)
(f : C(X, Y)) :
@[protected]
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 x₁, iseqv := _}
@[protected]
The quotient on path x₀ x₁ by the equivalence relation path.homotopic.
Equations
- path.homotopic.quotient x₀ x₁ = quotient (path.homotopic.setoid x₀ x₁)
Instances for path.homotopic.quotient
noncomputable
def
path.homotopic.quotient.comp
{X : Type u}
[topological_space 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
- P₀.comp P₁ = quotient.map₂ path.trans path.homotopic.quotient.comp._proof_1 P₀ P₁
theorem
path.homotopic.comp_lift
{X : Type u}
[topological_space X]
{x₀ x₁ x₂ : X}
(P₀ : path x₀ x₁)
(P₁ : path x₁ x₂) :
def
path.homotopic.quotient.map_fn
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{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
- P₀.map_fn f = quotient.map (λ (q : path x₀ x₁), q.map _) _ P₀
theorem
path.homotopic.map_lift
{X : Type u}
{Y : Type v}
[topological_space X]
[topological_space Y]
{x₀ x₁ : X}
(P₀ : path x₀ x₁)
(f : C(X, Y)) :
def
continuous_map.homotopy.eval_at
{X : Type u_1}
{Y : Type u_2}
[topological_space X]
[topological_space Y]
{f g : C(X, Y)}
(H : f.homotopy g)
(x : 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.eval_at x = {to_continuous_map := {to_fun := λ (t : ↥unit_interval), ⇑H (t, x), continuous_to_fun := _}, source' := _, target' := _}