English
If j = i.succ.castSucc, then the i-th arrow of the spine of δ_j(sx.spineToSimplex f) equals the diagonal edge via spineToDiagonal of f.interval i 2.
Русский
Если j = i.succ.castSucc, то i-ая стрелка спайна δ_j( sx.spineToSimplex f ) равна диагональному ребру через spineToDiagonal от f.interval i 2.
LaTeX
$$$$ (X.spine n (X.\delta j (sx.spineToSimplex f))).arrow i = sx.spineToDiagonal (f.interval i 2) $$$$
Lean4
/-- If we take the path along the spine of a face of a `spineToSimplex`, the
arrows not contained in the original path can be recovered as the diagonal edge
of the `spineToSimplex` that "composes" arrows `i` and `i + 1`. -/
theorem spine_δ_arrow_eq (h : j = i.succ.castSucc) :
(X.spine n (X.δ j (sx.spineToSimplex f))).arrow i = sx.spineToDiagonal (f.interval i 2 (by cutsat)) :=
by
simp only [SimplicialObject.δ, spine_arrow]
rw [← FunctorToTypes.map_comp_apply, ← op_comp]
rw [mkOfSucc_δ_eq h, spineToSimplex_edge]
