spine_δ_arrow_gt — Mathlib

English

If j < i.succ.castSucc, then the i-th arrow of the spine of δ_j(sx.spineToSimplex f) equals the i+1-th arrow of f.

Русский

Если j < i.succ.castSucc, то i-я стрелка спайна δ_j( sx.spineToSimplex f ) равна стрелке f на позиции i+1.

LaTeX

$$$$ (X.spine n (X.\delta j (sx.spineToSimplex f))).arrow i = f.arrow i.succ $$$$

Lean4

/-- If we take the path along the spine of the `j`th face of a `spineToSimplex`,
an arrow `i` with `i + 1 > j` can be identified with arrow `i + 1` in the
original path. -/
theorem spine_δ_arrow_gt (h : j < i.succ.castSucc) :
    (X.spine n (X.δ j (sx.spineToSimplex f))).arrow i = f.arrow i.succ :=
  by
  simp only [SimplicialObject.δ, spine_arrow]
  rw [← FunctorToTypes.map_comp_apply, ← op_comp]
  rw [mkOfSucc_δ_gt h, spineToSimplex_arrow]

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