σ_naturality_apply — Mathlib

English

For morphism f: S ⟶ T and i in Fin(n+1), the diagram σ is natural: f.app(op ⦋n+1⦌) ∘ σ_i = σ_i ∘ f.app(op ⦋n⦌).

Русский

Для морфизма f: S ⟶ T и i ∈ Fin(n+1) диаграмма σ натурализована: f.app(op ⦋n+1⦌) ∘ σ_i = σ_i ∘ f.app(op ⦋n⦌).

LaTeX

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

Lean4

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

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