δ_naturality — Mathlib

English

Natural in f: X ⟶ X' means δ_i commutes with f via naturality: X.δ_i ≫ f.app[n+1] = f.app[n] ≫ X'.δ_i.

Русский

Естественность по отношению к f: X ⟶ X' выражается тем, что δ_i коммутирует с f через естественность: X.δ_i ≫ f.app[n+1] = f.app[n] ≫ X'.δ_i.

LaTeX

$$$X.\delta_i \circ f_{⟨n+1⟩} = f_{⟨n⟩} \circ X'.\delta_i$$$

Lean4

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

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