English
In the additive setting, there is a strict equivalence between Karoubi(SimplicialObject C) and Karoubi(ChainComplex C Nat) with explicit functors N and Γ and natural isomorphisms exhibiting the equivalence.
Русский
В аддитивном контексте существует строгая эквивалентность между Карауби(SimplicialObject C) и Карауби(ChainComplex C Nat) с явными функторaми N и Γ и естественными изоморфизмами, доказывающими эквивалентность.
LaTeX
$$$$ \mathrm{Karoubi}(\mathrm{SimplicialObject}(C)) \simeq \mathrm{Karoubi}(\mathrm{ChainComplex}(C, \mathbb{N})) $$$$
Lean4
/-- In degree `0`, the null homotopic map `Hσ` is zero. -/
theorem Hσ_eq_zero (q : ℕ) : (Hσ q : K[X] ⟶ K[X]).f 0 = 0 :=
by
unfold Hσ
rw [nullHomotopicMap'_f_of_not_rel_left (c_mk 1 0 rfl) cs_down_0_not_rel_left]
rcases q with (_ | q)
· rw [hσ'_eq (show 0 = 0 + 0 by rfl) (c_mk 1 0 rfl)]
simp only [pow_zero, Fin.mk_zero, one_zsmul, eqToHom_refl, Category.comp_id]
-- This `erw` is needed to show `0 + 1 = 1`.
erw [ChainComplex.of_d]
rw [AlternatingFaceMapComplex.objD, Fin.sum_univ_two, Fin.val_zero, Fin.val_one, pow_zero, pow_one, one_smul,
neg_smul, one_smul, comp_add, comp_neg, add_neg_eq_zero, ← Fin.succ_zero_eq_one, δ_comp_σ_succ,
δ_comp_σ_self' X (by rw [Fin.castSucc_zero'])]
· rw [hσ'_eq_zero (Nat.succ_pos q) (c_mk 1 0 rfl), zero_comp]
