English
Let X and Y be StrictSegal simplicial sets and σ: X → Y a map. For any path f in X of length n+1, spineToSimplex commutes with mapping along σ, i.e. the spine of the mapped path equals the σ-component applied to the spine of f.
Русский
Пусть X и Y — симплициальные множества со строгой сегаловой структурой, и σ: X → Y — отображение. Для любой пути f в X длины n+1, отображение вдоль σ и применение spineToSimplex commuting, то есть spineToSimplex (f.map σ) равно σ_n (spineToSimplex f).
LaTeX
$$$$ \text{sy.spineToSimplex} (f.map \sigma) = \sigma_{n} \bigl( \text{sx.spineToSimplex} f \bigr) $$$$
Lean4
/-- For any `σ : X ⟶ Y` between `StrictSegal` simplicial sets, `spineToSimplex`
commutes with `Path.map`. -/
theorem spineToSimplex_map {X Y : SSet.{u}} (sx : StrictSegal X) (sy : StrictSegal Y) {n : ℕ} (f : Path X (n + 1))
(σ : X ⟶ Y) : sy.spineToSimplex (f.map σ) = σ.app _ (sx.spineToSimplex f) :=
by
apply sy.spineInjective
ext k
dsimp only [spineEquiv, Equiv.coe_fn_mk, spine_arrow]
rw [← types_comp_apply (σ.app _) (Y.map _), ← σ.naturality, types_comp_apply, spineToSimplex_arrow,
spineToSimplex_arrow, Path.map_arrow]
