spine_map_vertex — Mathlib

English

Given the same setup as above, the vertex compatibility under spine map holds for all intermediate steps, reflecting a naturality of the spine with respect to φ.

Русский

При той же конфигурации свойство совместимости вершин под отображением хребта справедливо для всех промежуточных шагов, отражая естественность хребта относительно φ.

LaTeX

$$$\forall n,m,\ \forall φ,\ i,\ (X.spine m (X.map φ.op Δ)).vertex i = (X.spine n Δ).vertex (φ.toOrderHom i)$$$

Lean4

theorem spine_map_vertex (Δ : X _⦋n⦌) {m : ℕ} (φ : ⦋m⦌ ⟶ ⦋n⦌) (i : Fin (m + 1)) :
    (X.spine m (X.map φ.op Δ)).vertex i = (X.spine n Δ).vertex (φ.toOrderHom i) :=
  truncation (max m n + 1) |>.obj X |>.spine_map_vertex n (by omega) Δ m (by omega) φ i

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