σ_naturality — Mathlib

English

Naturality of codegeneracies with respect to f: X ⟶ X': X.σ_i ≫ f.app[n] = f.app[n+1] ≫ X'.σ_i.

Русский

Естественность кодогенераторов по отношению к f: X ⟶ X': X.σ_i ∘ f_{⟨n⟩} = f_{⟨n+1⟩} ∘ X'.σ_i.

LaTeX

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

Lean4

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

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