LeanPool.DirectedTopologyLean4.DihomotopyFlip

def DirectedMap.Dihomotopy.flip {X : dTopCat} {f g : D(↑unitInterval,↑X)} (F : f.Dihomotopy g) : (F.evalAtRight 0).toDirectedMap.Dihomotopy (F.evalAtRight 1).toDirectedMap

Flip a dihomotopy by swapping its two coordinates.

Equations

• F.flip = { toFun := fun (t : ↑unitInterval × ↑unitInterval) => F (t.2, t.1), continuous_toFun := ⋯, directed_toFun := ⋯, map_zero_left := ⋯, map_one_left := ⋯ }

theorem DirectedMap.Dihomotopy.flip_apply {X : dTopCat} {f g : D(↑unitInterval,↑X)} (F : f.Dihomotopy g) (t₀ t₁ : ↑unitInterval) : F.flip (t₀, t₁) = F (t₁, t₀)

noncomputable def DirectedMap.Dihomotopy.hcomp' {X : dTopCat} {x₀ x₁ x₂ y₀ y₁ y₂ : ↑X} {p₀ : Dipath x₀ x₁} {p₁ : Dipath x₁ x₂} {q₀ : Dipath y₀ y₁} {q₁ : Dipath y₁ y₂} (F : p₀.toDirectedMap.Dihomotopy q₀.toDirectedMap) (G : p₁.toDirectedMap.Dihomotopy q₁.toDirectedMap) (h : (F.evalAtRight 1).toDirectedMap = (G.evalAtRight 0).toDirectedMap) : (p₀.trans p₁).toDirectedMap.Dihomotopy (q₀.trans q₁).toDirectedMap

Suppose the following are given:

• p₀ : dipath x₀ x₁
• p₁ : dipath x₁ x₂
• q₀ : dipath y₀ y₁
• q₁ : dipath y₁ y₂
• F : dihomotopy p₀.toDirectedMap q₀.toDirectedMap
• G : dihomotopy p₁.toDirectedMap p₁.toDirectedMap
• h : F.evalAtRight 1 = G.evalAtRight 0 Then we can compose these horizontally to obtain: dihomotopy (p₀.trans p₁).toDirectedMap (q₀.trans q₁).toDirectedMap

Equations

• F.hcomp' G h = ((F.flip.cast ⋯ h).trans G.flip).flip.cast ⋯ ⋯

theorem DirectedMap.Dihomotopy.hcomp'_apply {X : dTopCat} {x₀ x₁ x₂ y₀ y₁ y₂ : ↑X} {p₀ : Dipath x₀ x₁} {p₁ : Dipath x₁ x₂} {q₀ : Dipath y₀ y₁} {q₁ : Dipath y₁ y₂} (F : p₀.toDirectedMap.Dihomotopy q₀.toDirectedMap) (G : p₁.toDirectedMap.Dihomotopy q₁.toDirectedMap) (h : (F.evalAtRight 1).toDirectedMap = (G.evalAtRight 0).toDirectedMap) (t₁ t₂ : ↑unitInterval) : (F.hcomp' G h) (t₁, t₂) = if h : ↑t₂ ≤ 1 / 2 then (F.evalAtLeft t₁) ⟨2 * ↑t₂, ⋯⟩ else (G.evalAtLeft t₁) ⟨2 * ↑t₂ - 1, ⋯⟩

theorem DirectedMap.Dihomotopy.hcomp'_apply_zero_right {X : dTopCat} {x₀ x₁ x₂ y₀ y₁ y₂ : ↑X} {p₀ : Dipath x₀ x₁} {p₁ : Dipath x₁ x₂} {q₀ : Dipath y₀ y₁} {q₁ : Dipath y₁ y₂} (F : p₀.toDirectedMap.Dihomotopy q₀.toDirectedMap) (G : p₁.toDirectedMap.Dihomotopy q₁.toDirectedMap) (h : (F.evalAtRight 1).toDirectedMap = (G.evalAtRight 0).toDirectedMap) (x : ↑unitInterval) : (F.hcomp' G h) (x, 0) = F (x, 0)

theorem DirectedMap.Dihomotopy.hcomp'_apply_one_right {X : dTopCat} {x₀ x₁ x₂ y₀ y₁ y₂ : ↑X} {p₀ : Dipath x₀ x₁} {p₁ : Dipath x₁ x₂} {q₀ : Dipath y₀ y₁} {q₁ : Dipath y₁ y₂} (F : p₀.toDirectedMap.Dihomotopy q₀.toDirectedMap) (G : p₁.toDirectedMap.Dihomotopy q₁.toDirectedMap) (h : (F.evalAtRight 1).toDirectedMap = (G.evalAtRight 0).toDirectedMap) (x : ↑unitInterval) : (F.hcomp' G h) (x, 1) = G (x, 1)

theorem DirectedMap.Dihomotopy.hcomp'_range {X : dTopCat} {x₀ x₁ x₂ y₀ y₁ y₂ : ↑X} {p₀ : Dipath x₀ x₁} {p₁ : Dipath x₁ x₂} {q₀ : Dipath y₀ y₁} {q₁ : Dipath y₁ y₂} (F : p₀.toDirectedMap.Dihomotopy q₀.toDirectedMap) (G : p₁.toDirectedMap.Dihomotopy q₁.toDirectedMap) (h : (F.evalAtRight 1).toDirectedMap = (G.evalAtRight 0).toDirectedMap) : Set.range ⇑(F.hcomp' G h) ⊆ Set.range ⇑F ∪ Set.range ⇑G