English
The Dold–Kan equivalence extends to Karoubi-ified categories in the additive setting, yielding an equivalence between Karoubi(SimplicialObject C) and Karoubi(ChainComplex C Nat).
Русский
Эквивалентность Dold–Kan распространяется на Карауби-преобразования в аддитивной обстановке, давая эквивалентность между Карауби(СимпликальныеОбъекты C) и Карауби(ЦепочныеКомплексы C Nat).
LaTeX
$$$$ \mathrm{Karoubi}\big(\mathrm{SimplicialObject}(C)\big) \simeq \mathrm{Karoubi}\big(\mathrm{ChainComplex}(C, \mathbb{N})\big) $$$$
Lean4
/-- The Dold-Kan equivalence `Karoubi (SimplicialObject C) ≌ Karoubi (ChainComplex C ℕ)`
for additive categories. -/
@[simps]
def equivalence : Karoubi (SimplicialObject C) ≌ Karoubi (ChainComplex C ℕ)
where
functor := N
inverse := Γ
unitIso := Γ₂N₂
counitIso := N₂Γ₂
functor_unitIso_comp
P := by
let α := N.mapIso (Γ₂N₂.app P)
let β := N₂Γ₂.app (N.obj P)
symm
change 𝟙 _ = α.hom ≫ β.hom
rw [← Iso.inv_comp_eq, comp_id, ← comp_id β.hom, ← Iso.inv_comp_eq]
exact AlgebraicTopology.DoldKan.identity_N₂_objectwise P
