Commit 2022-08-24 18:34 fc5b2d2e

feat(algebraic_topology/dold_kan): the normalized Moore complex is a direct factor of the alternating face map complex (#16071) In this PR, we show that when the category A is abelian, there is an isomorphism N₁_iso_to_karoubi_normalized A 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 ℕ). (In particular, the normalized Moore complex is a direct factor of the alternating face map complex.)