spine_δ_arrow_lt — Mathlib

English

If i.castSucc < j, the i-th arrow of the spine along δ j equals the i.castSucc-th arrow of f.

Русский

Если i.castSucc < j, i-я стрелка позвоночника вдоль δ j равна i.castSucc-я стрелка f.

LaTeX

$$$(X.spine m (X.map (tr (δ j)).op (sx.spineToSimplex (m+1) f))).arrow i = f.arrow i.castSucc$$$

Lean4

/-- If we take the path along the spine of the `j`th face of a `spineToSimplex`,
the common arrows will agree with those of the original path `f`. In particular,
an arrow `i` with `i + 1 < j` can be identified with the same arrow in `f`. -/
theorem spine_δ_arrow_lt (hij : i.succ.castSucc < j) :
    (X.spine m _ (X.map (tr (δ j)).op (sx.spineToSimplex (m + 1) _ f))).arrow i = f.arrow i.castSucc := by
  rw [spine_arrow, ← FunctorToTypes.map_comp_apply, ← op_comp, ← tr_comp, mkOfSucc_δ_lt hij, spineToSimplex_arrow]

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