English
The functor N is defined on Karoubi(SimplicialObject C) to Karoubi(ChainComplex C Nat) and is simplicial-compatible with the standard Dold–Kan translation.
Русский
Функтор N задаётся на Карауби(SimplicialObject C) и отображает в Карауби(ChainComplex C Nat), сохраняет совместимость со стандартным переводом Dold–Kan.
LaTeX
$$$$ N : \mathrm{Karoubi}(\mathrm{SimplicialObject}(C)) \to \mathrm{Karoubi}(\mathrm{ChainComplex}(C, \mathbb{N})) $$$$
Lean4
/-- The maps `hσ' q n m hnm` are natural on the simplicial object -/
theorem hσ'_naturality (q : ℕ) (n m : ℕ) (hnm : c.Rel m n) {X Y : SimplicialObject C} (f : X ⟶ Y) :
f.app (op ⦋n⦌) ≫ hσ' q n m hnm = hσ' q n m hnm ≫ f.app (op ⦋m⦌) :=
by
have h : n + 1 = m := hnm
subst h
simp only [hσ', eqToHom_refl, comp_id]
unfold hσ
split_ifs
· rw [zero_comp, comp_zero]
· simp
