diagonalPath — Mathlib

English

The diagonal path d of a homotopy H on a path p is obtained by projecting the lifted product path through the lifted homotopy.

Русский

Диагональный путь d гомотопии H по пути p получен проецированием подъема произведения путей через подъёмную гомотопию.

LaTeX

$$$$ \\text{diagonalPath}(H,p) = \\pi_m(TopCat.ofHom H.uliftMap)\\Big( \\text{prodToProdTopI }(uhpath01,p) \\Big). $$$$

Lean4

/-- The diagonal path `d` of a homotopy `H` on a path `p` -/
def diagonalPath : fromTop (H (0, x₀)) ⟶ fromTop (H (1, x₁)) :=
  (πₘ (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 p)

Похожие утверждения