mathlib3 documentation


Comparison with the normalized Moore complex functor #

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

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

In this file, we show that when the category A is abelian, there is an isomorphism N₁_iso_normalized_Moore_complex_comp_to_karoubi between the functor N₁ : simplicial_object A ⥤ karoubi (chain_complex A ℕ) defined in functor_n.lean and the composition of normalized_Moore_complex A with the inclusion chain_complex A ℕ ⥤ karoubi (chain_complex A ℕ).

This isomorphism shall be used in equivalence.lean in order to obtain the Dold-Kan equivalence category_theory.abelian.dold_kan.equivalence : simplicial_object A ≌ chain_complex A ℕ with a functor (definitionally) equal to normalized_Moore_complex A.

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