spineToSimplex_map — Mathlib

English

For any map σ: X → Y of truncated StrictSegal objects, spineToSimplex commutes with Path.map.

Русский

Для любого отображения σ: X → Y между усеченными StrictSegal, отображение spineToSimplex commute с Path.map.

LaTeX

$$sy.spineToSimplex (m+1) _ (f.map(σ)) = σ.app (op ⦋m+1⦌) (sx.spineToSimplex (m+1) _ f)$$

Lean4

/-- For any `σ : X ⟶ Y` between `n + 1`-truncated `StrictSegal` simplicial sets,
`spineToSimplex` commutes with `Path.map`. -/
theorem spineToSimplex_map {X Y : SSet.Truncated.{u} (n + 1)} (sx : StrictSegal X) (sy : StrictSegal Y) (m : ℕ)
    (h : m ≤ n) (f : Path X (m + 1)) (σ : X ⟶ Y) :
    sy.spineToSimplex (m + 1) _ (f.map σ) = σ.app (op ⦋m + 1⦌ₙ ₊ ₁) (sx.spineToSimplex (m + 1) _ f) :=
  by
  apply sy.spineInjective (m + 1)
  ext k
  dsimp only [spineEquiv, Equiv.coe_fn_mk, spine_arrow]
  rw [← types_comp_apply (σ.app _) (Y.map _), ← σ.naturality]
  simp

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