hσ'_eq_zero — Mathlib

English

The family of maps hσ' q n m hnm is natural in the simplicial object: for any map f between simplicial objects, applying f commutes with hσ'.

Русский

Семейство отображений hσ' q n m hnm естественно по отношению к объектам, то есть при любом морфизме f между симпликциальными объектами композиции с hσ' совпадают.

LaTeX

$$$$ f_{\mathrm{app}}(\,n\,) \circ hσ' q n m hnm = hσ' q n m hnm \circ f_{\mathrm{app}}(\,m\,) $$$$

Lean4

theorem hσ'_eq_zero {q n m : ℕ} (hnq : n < q) (hnm : c.Rel m n) : (hσ' q n m hnm : X _⦋n⦌ ⟶ X _⦋m⦌) = 0 :=
  by
  simp only [hσ', hσ]
  split_ifs
  exact zero_comp

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