δ_naturality_apply — Mathlib

English

Let f: S ⟶ T be a morphism of simplicial sets. Then for each i, f.app(op ⦋n+2⦌) ∘ δ_i = δ_i ∘ f.app(op ⦋n+1⦌) on S, i.e., δ is natural with respect to f.

Русский

Пусть f: S ⟶ T — морфизм симпликальных множеств. Тогда для каждого i выполняется естественность: f.app(op ⦋n+2⦌) ∘ δ_i = δ_i ∘ f.app(op ⦋n+1⦌) на S; δ естественен относительно f.

LaTeX

$$$ f.app(\\mathrm{op}\\langle n+2 \\rangle) \\circ \\delta_i = \\delta_i \\circ f.app(\\mathrm{op}\\langle n+1 \\rangle) $$$

Lean4

theorem δ_naturality_apply {n : ℕ} (i : Fin (n + 2)) (x : S _⦋n + 1⦌) :
    f.app (op ⦋n⦌) (S.δ i x) = T.δ i (f.app (op ⦋n + 1⦌) x) :=
  by
  change (S.δ i ≫ f.app (op ⦋n⦌)) x = (f.app (op ⦋n + 1⦌) ≫ T.δ i) x
  exact congr_fun (SimplicialObject.δ_naturality f i) x

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