LeanPool.DirectedTopologyLean4.DihomotopyToPathDihomotopy

def DirectedMap.Dihomotopy.MinDirected : D(↑unitInterval × ↑unitInterval,↑unitInterval)

The directed map taking the pointwise minimum of the two coordinates on I × I.

Equations

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

def DirectedMap.Dihomotopy.MaxDirected : D(↑unitInterval × ↑unitInterval,↑unitInterval)

The directed map taking the pointwise maximum of the two coordinates on I × I.

Equations

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

def DirectedMap.Dihomotopy.SourceToPath {X : dTopCat} {x y : ↑X} (γ : Dipath x y) : (Dipath.refl x).toDirectedMap.Dihomotopy γ.toDirectedMap

Dihomotopy from the constant path at the source to a dipath, given by SourceToPath γ (s, t) = γ (min s t).

Equations

• DirectedMap.Dihomotopy.SourceToPath γ = { toDirectedMap := γ.toDirectedMap.comp DirectedMap.Dihomotopy.MinDirected, map_zero_left := ⋯, map_one_left := ⋯ }

theorem DirectedMap.Dihomotopy.sourceToPath_apply {X : dTopCat} {x y : ↑X} (γ : Dipath x y) (s t : ↑unitInterval) : (SourceToPath γ) (s, t) = γ (min s t)

theorem DirectedMap.Dihomotopy.sourceToPath_range {X : dTopCat} {x y : ↑X} (γ : Dipath x y) : Set.range ⇑(SourceToPath γ) = Set.range ⇑γ

def DirectedMap.Dihomotopy.PathToTarget {X : dTopCat} {x y : ↑X} (γ : Dipath x y) : γ.toDirectedMap.Dihomotopy (Dipath.refl y).toDirectedMap

Dihomotopy from a dipath to the constant path at the target, given by PathToTarget γ (s, t) = γ (max s t).

Equations

• DirectedMap.Dihomotopy.PathToTarget γ = { toDirectedMap := γ.toDirectedMap.comp DirectedMap.Dihomotopy.MaxDirected, map_zero_left := ⋯, map_one_left := ⋯ }

theorem DirectedMap.Dihomotopy.pathToTarget_apply {X : dTopCat} {x y : ↑X} (γ : Dipath x y) (s t : ↑unitInterval) : (PathToTarget γ) (s, t) = γ (max s t)

theorem DirectedMap.Dihomotopy.pathToTarget_range {X : dTopCat} {x y : ↑X} (γ : Dipath x y) : Set.range ⇑(PathToTarget γ) = Set.range ⇑γ

def DihomToPathDihom.dihomToDihomOfPaths {X : dTopCat} {f g : D(↑unitInterval,↑X)} (F : f.Dihomotopy g) : (Dipath.ofDirectedMap f).toDirectedMap.Dihomotopy (Dipath.ofDirectedMap g).toDirectedMap

Reinterpret a dihomotopy between directed maps f g : D(I, X) as a dihomotopy between the associated dipaths Dipath.ofDirectedMap f and Dipath.ofDirectedMap g.

Equations

• DihomToPathDihom.dihomToDihomOfPaths F = { toDirectedMap := F.toDirectedMap, map_zero_left := ⋯, map_one_left := ⋯ }

noncomputable def DihomToPathDihom.dihomToPathDihom {X : dTopCat} {f g : D(↑unitInterval,↑X)} (F : f.Dihomotopy g) : (((Dipath.refl (f 0)).trans (Dipath.ofDirectedMap f)).trans (F.evalAtRight 1)).Dihomotopy (((F.evalAtRight 0).trans (Dipath.ofDirectedMap g)).trans (Dipath.refl (g 1)))

Let a dihomotopy F : f ~ g, with f g : D(I,X) be given: C----- g -----D | | | | | | | | A----- f -----B Then there is a path-dihomotopy between the paths A --refl A--> A --f--> B --F.evalAtRight 1--> D and A --F.evalAtRight 0--> C --g--> D --refl D--> D

Equations

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

theorem DihomToPathDihom.dihom_to_path_dihom_range {X : dTopCat} {f g : D(↑unitInterval,↑X)} (F : f.Dihomotopy g) : Set.range ⇑(dihomToPathDihom F) ⊆ Set.range ⇑F