mathlib3 documentation


N₁ and N₂ reflects isomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

@[protected, instance]

We deduce that N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ)) reflects isomorphisms from the fact that N₁ : simplicial_object (karoubi C) ⥤ karoubi (chain_complex (karoubi C) ℕ) does.