Theorems · Theorem · algebraic topology

SSet.Truncated.spine_map_vertex

∀ {n : ℕ} (X : SSet.Truncated (n + 1)) (m : ℕ) (hₘ : m ≤ n + 1)
  (Δ : X.obj (Opposite.op { obj := { len := m }, property := hₘ })) (a : ℕ) (hₐ : a ≤ n + 1)
  (φ : { obj := { len := a }, property := hₐ } ⟶ { obj := { len := m }, property := hₘ }) (i : Fin (a + 1)),
  (X.spine a hₐ ((CategoryTheory.ConcreteCategory.hom (X.map φ.op)) Δ)).vertex i =
    (X.spine m hₘ Δ).vertex ((SimplexCategory.Hom.toOrderHom φ.hom) i)

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.Path

Cited by

1 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound