spineToDiagonal — Mathlib

English

Under the strict Segal condition, a path of length m can be composed into a single edge of length 1 by taking the diagonal edge of the corresponding m-simplex.

Русский

При строгом условии Segal путь длины m можно составить в один ребро длины 1, взяв диагональный ребро соответствующего m-симплексa.

LaTeX

$$$spineToDiagonal: Path(X,m) \to X_{\langle 1\rangle_{n+1}}$ is defined by $spineToDiagonal(f) = X.map(tr(diag(m)).op)(spineToSimplex(m,h,f))$$$

Lean4

/-- In the presence of the strict Segal condition, a path of length `m` can be
"composed" by taking the diagonal edge of the resulting `m`-simplex. -/
def spineToDiagonal : Path X m → X _⦋1⦌ₙ ₊ ₁ :=
  X.map (tr (diag m)).op ∘ sx.spineToSimplex m h

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