spineToSimplex_edge — Mathlib

English

If i is an index in 0,...,m-1, the map along the i-th edge yields the i-th edge of the path.

Русский

Если i принадлежит диапазону, отображение вдоль i-й ребра возвращает i-ю дугу пути.

LaTeX

$$$X.map(\mathrm{tr}\; (\mathrm{mkOfSucc}(i))^{op}(\mathrm{spineToSimplex}(m,h,f))) = f.arrow(i)$$$

Lean4

theorem spineToSimplex_edge (f : Path X m) (j l : ℕ) (hjl : j + l ≤ m) :
    X.map (tr (intervalEdge j l hjl)).op (sx.spineToSimplex m h f) =
      sx.spineToDiagonal l (by cutsat) (f.interval j l hjl) :=
  by
  dsimp only [spineToDiagonal, Function.comp_apply]
  rw [← spineToSimplex_interval, ← FunctorToTypes.map_comp_apply, ← op_comp, ← tr_comp, diag_subinterval_eq]

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