spineToSimplex_edge — Mathlib

English

The intervalEdge map interacts with spineToSimplex to give spineToDiagonal along a 2-edge path.

Русский

Отображение intervalEdge взаимодействует с spineToSimplex, давая spineToDiagonal вдоль 2-реберного пути.

LaTeX

$$X.map (intervalEdge j l hjl).op (sx.spineToSimplex f) = sx.spineToDiagonal (f.interval j l hjl)$$

Lean4

theorem spineToSimplex_edge :
    X.map (intervalEdge j l hjl).op (sx.spineToSimplex f) = sx.spineToDiagonal (f.interval j l hjl) :=
  by
  dsimp only [spineToDiagonal, SimplicialObject.diagonal]
  rw [← spineToSimplex_interval, ← FunctorToTypes.map_comp_apply, ← op_comp, diag_subinterval_eq]

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