δ_naturality — Mathlib

English

Morphisms between simplicial objects commute with δ maps in a natural way: the naturality square for δ with any morphism f: X → X'.

Русский

Генерализованная естественность отображений δ между симпликальными объектами: диаграмма естественности δ для f: X → X'.

LaTeX

$$$f.\mathrm{nat}_{\delta}: X.\delta_i \circ f_{\!}\text{(n)} = f_{\!}\text{(n+1)} \circ X'.\delta_i$$$

Lean4

@[reassoc (attr := simp)]
theorem δ_naturality {X' X : SimplicialObject C} (f : X ⟶ X') {n : ℕ} (i : Fin (n + 2)) :
    X.δ i ≫ f.app (op ⦋n⦌) = f.app (op ⦋n + 1⦌) ≫ X'.δ i :=
  f.naturality _

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