LeanPool.DirectedTopologyLean4.DirectedPathHomotopy

@[reducible, inline]

abbrev Dipath.Dihomotopy {X : Type u} [DirectedSpace X] {x y : X} (p₀ p₁ : Dipath x y) : Type u

The type of dihomotopies between two directed paths.

Equations

• p₀.Dihomotopy p₁ = p₀.toDirectedMap.DihomotopyRel p₁.toDirectedMap {0, 1}

theorem Dipath.Dihomotopy.coeFn_injective {X : Type u} [DirectedSpace X] {x y : X} {p₀ p₁ : Dipath x y} : Function.Injective DFunLike.coe

@[simp]

theorem Dipath.Dihomotopy.source {X : Type u} [DirectedSpace X] {x y : X} {p₀ p₁ : Dipath x y} (F : p₀.Dihomotopy p₁) (t : ↑unitInterval) : F (t, 0) = x

@[simp]

theorem Dipath.Dihomotopy.target {X : Type u} [DirectedSpace X] {x y : X} {p₀ p₁ : Dipath x y} (F : p₀.Dihomotopy p₁) (t : ↑unitInterval) : F (t, 1) = y

def Dipath.Dihomotopy.homToDihom {X : Type u} [DirectedSpace X] {x y : X} {p₀ p₁ : Dipath x y} (F : p₀.Homotopy p₁.toPath) (HF : DirectedMap.Directed F.toContinuousMap) : p₀.Dihomotopy p₁

A F : Dihomotopy ↑p₁ ↑p₂ between two dipaths p₁ p₂ : Dipath y z can be coerced into a dihomotopy, if it is directed

Equations

• Dipath.Dihomotopy.homToDihom F HF = { toContinuousMap := F.toContinuousMap, directed_toFun := HF, map_zero_left := ⋯, map_one_left := ⋯, prop' := ⋯ }

def Dipath.Dihomotopy.dihomToHom {X : Type u} [DirectedSpace X] {x y : X} {p₀ p₁ : Dipath x y} (F : p₀.Dihomotopy p₁) : p₀.Homotopy p₁.toPath

A Dihomotopy F between two Dipaths p₁ p₂ can be coerced into a Homotopy between p₀.toPath and p₁.toPath.

Equations

• F.dihomToHom = { toContinuousMap := F.toContinuousMap, map_zero_left := ⋯, map_one_left := ⋯, prop' := ⋯ }

@[implicit_reducible]

instance Dipath.Dihomotopy.coeDihomToHom {X : Type u} [DirectedSpace X] {x y : X} {p₀ p₁ : Dipath x y} : Coe (p₀.Dihomotopy p₁) (p₀.Homotopy p₁.toPath)

Equations

• Dipath.Dihomotopy.coeDihomToHom = { coe := fun (F : p₀.Dihomotopy p₁) => F.dihomToHom }

def Dipath.Dihomotopy.eval {X : Type u} [DirectedSpace X] {x y : X} {p₀ p₁ : Dipath x y} (F : p₀.Dihomotopy p₁) (t : ↑unitInterval) : Dipath x y

Evaluating a dipath homotopy at an intermediate point, giving us a Dipath.

Equations

• F.eval t = { toFun := ⇑(F.curry t), continuous_toFun := ⋯, source' := ⋯, target' := ⋯, dipath_toPath := ⋯ }

@[simp]

theorem Dipath.Dihomotopy.coe_eval {X : Type u} [DirectedSpace X] {x y : X} {p₀ p₁ : Dipath x y} (F : p₀.Dihomotopy p₁) (t : ↑unitInterval) : ⇑(F.eval t) = ⇑(F.curry t)

@[simp]

theorem Dipath.Dihomotopy.eval_zero {X : Type u} [DirectedSpace X] {x y : X} {p₀ p₁ : Dipath x y} (F : p₀.Dihomotopy p₁) : F.eval 0 = p₀

@[simp]

theorem Dipath.Dihomotopy.eval_one {X : Type u} [DirectedSpace X] {x y : X} {p₀ p₁ : Dipath x y} (F : p₀.Dihomotopy p₁) : F.eval 1 = p₁

def Dipath.Dihomotopy.refl {X : Type u} [DirectedSpace X] {x y : X} (p : Dipath x y) : p.Dihomotopy p

Given a dipath p, we can define a Dihomotopy p p by F (t, x) = p x

Equations

• Dipath.Dihomotopy.refl p = DirectedMap.DihomotopyRel.refl p.toDirectedMap {0, 1}

@[simp]

theorem Dipath.Dihomotopy.refl_apply {X : Type u} [DirectedSpace X] {x y : X} (p : Dipath x y) (x✝ : ↑unitInterval × ↑unitInterval) : (refl p) x✝ = p x✝.2

@[simp]

theorem Dipath.Dihomotopy.refl_toFun {X : Type u} [DirectedSpace X] {x y : X} (p : Dipath x y) (x✝ : ↑unitInterval × ↑unitInterval) : (refl p) x✝ = p x✝.2

noncomputable def Dipath.Dihomotopy.trans {X : Type u} [DirectedSpace X] {x y : X} {p₀ p₁ p₂ : Dipath x y} (F : p₀.Dihomotopy p₁) (G : p₁.Dihomotopy p₂) : p₀.Dihomotopy p₂

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

Equations

• F.trans G = DirectedMap.DihomotopyRel.trans F G

theorem Dipath.Dihomotopy.trans_apply {X : Type u} [DirectedSpace X] {x y : X} {p₀ p₁ p₂ : Dipath x y} (F : p₀.Dihomotopy p₁) (G : p₁.Dihomotopy 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)

def Dipath.Dihomotopy.cast {X : Type u} [DirectedSpace X] {x y : X} {p₀ p₁ q₀ q₁ : Dipath x y} (F : p₀.Dihomotopy p₁) (h₀ : p₀ = q₀) (h₁ : p₁ = q₁) : q₀.Dihomotopy q₁

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

Equations

• F.cast h₀ h₁ = DirectedMap.DihomotopyRel.cast F ⋯ ⋯

theorem Dipath.Dihomotopy.hcomp_apply_half_left {X : Type u} [DirectedSpace X] {x y z : X} {p₀ q₀ : Dipath x y} {p₁ q₁ : Dipath y z} (F : p₀.Dihomotopy q₀) (G : p₁.Dihomotopy q₁) (s t : ↑unitInterval) (ht : t = unitIAux.halfI) : (F.dihomToHom.hcomp G.dihomToHom) (s, t) = F (s, 1)

theorem Dipath.Dihomotopy.hcomp_apply_half_right {X : Type u} [DirectedSpace X] {x y z : X} {p₀ q₀ : Dipath x y} {p₁ q₁ : Dipath y z} (F : p₀.Dihomotopy q₀) (G : p₁.Dihomotopy q₁) (s t : ↑unitInterval) (ht : t = unitIAux.halfI) : (F.dihomToHom.hcomp G.dihomToHom) (s, t) = G (s, 0)

theorem Dipath.Dihomotopy.hcomp_apply_left {X : Type u} [DirectedSpace X] {x y z : X} {p₀ q₀ : Dipath x y} {p₁ q₁ : Dipath y z} (F : p₀.Dihomotopy q₀) (G : p₁.Dihomotopy q₁) (s t : ↑unitInterval) (ht : ↑t ≤ 2⁻¹) : (F.dihomToHom.hcomp G.dihomToHom) (s, t) = F (s, ⟨2 * ↑t, ⋯⟩)

theorem Dipath.Dihomotopy.hcomp_apply_right {X : Type u} [DirectedSpace X] {x y z : X} {p₀ q₀ : Dipath x y} {p₁ q₁ : Dipath y z} (F : p₀.Dihomotopy q₀) (G : p₁.Dihomotopy q₁) (s t : ↑unitInterval) (ht : 2⁻¹ ≤ ↑t) : (F.dihomToHom.hcomp G.dihomToHom) (s, t) = G (s, ⟨2 * ↑t - 1, ⋯⟩)

theorem Dipath.Dihomotopy.hcomp_first_case {X : Type u} [DirectedSpace X] {x y z : X} {p₀ q₀ : Dipath x y} {p₁ q₁ : Dipath y z} (F : p₀.Dihomotopy q₀) (G : p₁.Dihomotopy q₁) {a₀ a₁ : ↑unitInterval × ↑unitInterval} {γ : Path a₀ a₁} (γ_dipath : IsDipath γ) (ht₁ : ↑a₁.2 ≤ 2⁻¹) : IsDipath (γ.map ⋯)

theorem Dipath.Dihomotopy.hcomp_second_case {X : Type u} [DirectedSpace X] {x y z : X} {p₀ q₀ : Dipath x y} {p₁ q₁ : Dipath y z} (F : p₀.Dihomotopy q₀) (G : p₁.Dihomotopy q₁) {a₀ a₁ : ↑unitInterval × ↑unitInterval} {γ : Path a₀ a₁} (γ_dipath : IsDipath γ) (ht₀ : 2⁻¹ ≤ ↑a₀.2) : IsDipath (γ.map ⋯)

noncomputable def Dipath.Dihomotopy.hcomp {X : Type u} [DirectedSpace X] {x y z : X} {p₀ q₀ : Dipath x y} {p₁ q₁ : Dipath y z} (F : p₀.Dihomotopy q₀) (G : p₁.Dihomotopy q₁) : (p₀.trans p₁).Dihomotopy (q₀.trans q₁)

Suppose p₀ and q₀ are dipaths from x to y, p₁ and q₁ are dipaths from y to z. Furthermore, suppose F : Dihomotopy p₀ q₀ and G : Dihomotopy p₁ q₁. Then we can define a dihomotopy from p₀.trans p₁ to q₀.trans q₁.

Equations

• F.hcomp G = Dipath.Dihomotopy.homToDihom (F.dihomToHom.hcomp G.dihomToHom) ⋯

theorem Dipath.Dihomotopy.hcomp_apply {X : Type u} [DirectedSpace X] {x y z : X} {p₀ q₀ : Dipath x y} {p₁ q₁ : Dipath y z} (F : p₀.Dihomotopy q₀) (G : p₁.Dihomotopy 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 Dipath.Dihomotopy.hcomp_half {X : Type u} [DirectedSpace X] {x y z : X} {p₀ q₀ : Dipath x y} {p₁ q₁ : Dipath y z} (F : p₀.Dihomotopy q₀) (G : p₁.Dihomotopy q₁) (t : ↑unitInterval) : (F.hcomp G) (t, ⟨1 / 2, ⋯⟩) = y

def Dipath.Dihomotopy.reparam {X : Type u} [DirectedSpace X] {x y : X} (p : Dipath x y) (f g : D(↑unitInterval,↑unitInterval)) (hf_le_g : ∀ (t : ↑unitInterval), f t ≤ g t) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) (hg₀ : g 0 = 0) (hg₁ : g 1 = 1) : (p.reparam f hf₀ hf₁).Dihomotopy (p.reparam g hg₀ hg₁)

Suppose p is a dipath, and f g : D(I,I) two monotonic subparametrizations. If f is dominated by g, i.e. ∀ t, f t ≤ g t, then we obtain a dihomotopy between the two subparametrization of p as the interpolation between the two becomes directed.

Equations

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

noncomputable def Dipath.Dihomotopy.transRefl {X : Type u} [DirectedSpace X] {x y : X} (p : Dipath x y) : p.Dihomotopy (p.trans (Dipath.refl y))

For any p : Dipath x y, there is a dihomotopy from p to p.trans (Dipath.refl y).

Equations

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

noncomputable def Dipath.Dihomotopy.reflTrans {X : Type u} [DirectedSpace X] {x y : X} (p : Dipath x y) : ((Dipath.refl x).trans p).Dihomotopy p

For any p : Dipath x y, there is a dihomotopy from (Dipath.refl x).trans p to p.

Equations

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

noncomputable def Dipath.Dihomotopy.reflTransToReparamTransRefl {X : Type u} [DirectedSpace X] {x y : X} (p : Dipath x y) (f : D(↑unitInterval,↑unitInterval)) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : ((Dipath.refl x).trans p).Dihomotopy ((p.reparam f hf₀ hf₁).trans (Dipath.refl y))

For any p : Dipath x y, there is a homotopy from (Dipath.refl x).trans p to q.trans (Dipath.refl y), where q is any directed reparametrization of p.

Equations

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

def Dipath.Dihomotopy.map {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {x y : X} {p q : Dipath x y} (F : p.Dihomotopy q) (f : D(X,Y)) : (p.map f).Dihomotopy (q.map f)

Given F : Dihomotopy p q, and f : D(X,Y), there is a dihomotopy from p.map f to q.map f given by f ∘ F.

Equations

• F.map f = { toFun := ⇑f ∘ ⇑F, continuous_toFun := ⋯, directed_toFun := ⋯, map_zero_left := ⋯, map_one_left := ⋯, prop' := ⋯ }

@[simp]

theorem Dipath.Dihomotopy.map_toFun {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {x y : X} {p q : Dipath x y} (F : p.Dihomotopy q) (f : D(X,Y)) (a✝ : ↑unitInterval × ↑unitInterval) : (F.map f) a✝ = f (F a✝)

@[simp]

theorem Dipath.Dihomotopy.map_apply {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {x y : X} {p q : Dipath x y} (F : p.Dihomotopy q) (f : D(X,Y)) (a✝ : ↑unitInterval × ↑unitInterval) : (F.map f) a✝ = f (F a✝)

def Dipath.PreDihomotopic {X : Type u} [DirectedSpace X] {x y : X} (p₀ p₁ : Dipath x y) : Prop

Two dipaths p₀ and p₁ are Dipath.PreDihomotopic if there exists a Dihomotopy from p₀ to p₁.

Equations

• p₀.PreDihomotopic p₁ = Nonempty (p₀.Dihomotopy p₁)

def Dipath.Dihomotopic {X : Type u} [DirectedSpace X] {x y : X} (p₀ p₁ : Dipath x y) : Prop

Dipath.Dihomotopic is the equivalence generated by Dipath.PreDihomotopic.

Equations

• p₀.Dihomotopic p₁ = Relation.EqvGen Dipath.PreDihomotopic p₀ p₁

theorem Dipath.Dihomotopic.equivalence {X : Type u} [DirectedSpace X] {x y : X} : Equivalence Dihomotopic

theorem Dipath.Dihomotopic.map {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {x y : X} {p q : Dipath x y} (h : p.Dihomotopic q) (f : D(X,Y)) : (p.map f).Dihomotopic (q.map f)

If p is dihomotopic with q, then f ∘ p is dihomotopic with f ∘ q for any directed map f

theorem Dipath.Dihomotopic.hcomp_aid_left {X : Type u} [DirectedSpace X] {x y z : X} {p₀ p₁ : Dipath x y} (q : Dipath y z) (hp : p₀.Dihomotopic p₁) : (p₀.trans q).Dihomotopic (p₁.trans q)

theorem Dipath.Dihomotopic.hcomp_aid_right {X : Type u} [DirectedSpace X] {x y z : X} (p : Dipath x y) {q₀ q₁ : Dipath y z} (hq : q₀.Dihomotopic q₁) : (p.trans q₀).Dihomotopic (p.trans q₁)

theorem Dipath.Dihomotopic.hcomp {X : Type u} [DirectedSpace X] {x y z : X} {p₀ p₁ : Dipath x y} {q₀ q₁ : Dipath y z} (hp : p₀.Dihomotopic p₁) (hq : q₀.Dihomotopic q₁) : (p₀.trans q₀).Dihomotopic (p₁.trans q₁)

Suppose we havep₀ p₁ : Dipath x y and q₀ q₁ : Dipath y z. If p₀ is dihomotopic with p₁ and q₀ is dihomotopic with q₁, then p₀.trans q₀ is dihomotopic with p₁.trans q₁.

theorem Dipath.Dihomotopic.reparam {X : Type u} [DirectedSpace X] {x y : X} (p : Dipath x y) (f : D(↑unitInterval,↑unitInterval)) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : p.Dihomotopic (p.reparam f hf₀ hf₁)

If p is a dipath, then it is dihomotopic with any monotonic subparametrization.

@[reducible]

def Dipath.Dihomotopic.setoid {X : Type u} [DirectedSpace X] (x y : X) : Setoid (Dipath x y)

The setoid on Dipaths defined by the equivalence relation Dipath.Dihomotopic. That is, two paths are equivalent if there is a chain of Dihomotopies starting in one and ending in the other.

Equations

• Dipath.Dihomotopic.setoid x y = { r := Dipath.Dihomotopic, iseqv := ⋯ }

def Dipath.Dihomotopic.Quotient {X : Type u} [DirectedSpace X] (x y : X) : Type u

The quotient on Dipath x y by the equivalence relation Dipath.Dihomotopic.

Equations

• Dipath.Dihomotopic.Quotient x y = Quotient (Dipath.Dihomotopic.setoid x y)

@[implicit_reducible]

instance Dipath.Dihomotopic.instInhabitedQuotient {X : Type u} [DirectedSpace X] {x : X} : Inhabited (Dihomotopic.Quotient x x)

Equations

• Dipath.Dihomotopic.instInhabitedQuotient = { default := Quotient.mk' (Dipath.refl x) }

noncomputable def Dipath.Dihomotopic.Quotient.comp {X : Type u} [DirectedSpace X] {x y z : X} (P₀ : Dihomotopic.Quotient x y) (P₁ : Dihomotopic.Quotient y z) : Dihomotopic.Quotient x z

The composition of dipath dihomotopy classes. This is Dipath.trans descended to the quotient.

Equations

• P₀.comp P₁ = Quotient.map₂ Dipath.trans ⋯ P₀ P₁

theorem Dipath.Dihomotopic.comp_lift {X : Type u} [DirectedSpace X] {x y z : X} (P₀ : Dipath x y) (P₁ : Dipath y z) : ⟦P₀.trans P₁⟧ = Quotient.comp ⟦P₀⟧ ⟦P₁⟧

def Dipath.Dihomotopic.Quotient.mapFn {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {x y : X} (P₀ : Dihomotopic.Quotient x y) (f : D(X,Y)) : Dihomotopic.Quotient (f x) (f y)

The image of a dipath dihomotopy class P₀ under a directed map f. This is Dipath.map descended to the quotient.

Equations

• P₀.mapFn f = Quotient.map (fun (q : Dipath x y) => q.map f) ⋯ P₀

theorem Dipath.Dihomotopic.map_lift {X : Type u} {Y : Type v} [DirectedSpace X] [DirectedSpace Y] {x y : X} (P₀ : Dipath x y) (f : D(X,Y)) : ⟦P₀.map f⟧ = Quotient.mapFn ⟦P₀⟧ f

theorem Dipath.Dihomotopic.quot_reparam {X : Type u} [DirectedSpace X] {x y : X} (γ : Dipath x y) {f : D(↑unitInterval,↑unitInterval)} (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : ⟦γ.reparam f hf₀ hf₁⟧ = ⟦γ⟧

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