N₁ and N₂ reflects isomorphisms #

In this file, it is shown that the functors N₁ : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ) and N₂ : Karoubi (SimplicialObject C) ⥤ Karoubi (ChainComplex C ℕ)) reflect isomorphisms for any preadditive category C.

(See Equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)

We deduce that N₂ : Karoubi (SimplicialObject C) ⥤ Karoubi (ChainComplex C ℕ)) reflects isomorphisms from the fact that N₁ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) does.

  • =