mathlib documentation


Construction of functors N for the Dold-Kan correspondence #

TODO (@joelriou) continue adding the various files referenced below

In this file, we construct functors N₁ : simplicial_object C ⥤ karoubi (chain_complex C ℕ) and N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex C ℕ) for any preadditive category C. (The indices of these functors are the number of occurrences of karoubi at the source or the target.)

In the case C is additive, the functor N₂ shall be the functor of the equivalence category_theory.preadditive.dold_kan.equivalence defined in equivalence_additive.lean.

In the case the category C is pseudoabelian, the composition of N₁ with the inverse of the equivalence chain_complex C ℕ ⥤ karoubi (chain_complex C ℕ) will be the functor category_theory.idempotents.dold_kan.N of the equivalence of categories category_theory.idempotents.dold_kan.equivalence : simplicial_object C ≌ chain_complex C ℕ defined in equivalence_pseudoabelian.lean.

When the category C is abelian, a relation between N₁ and the normalized Moore complex functor shall be obtained in normalized.lean.

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