mathlib

fc5b2d2e - feat(algebraic_topology/dold_kan): the normalized Moore complex is a direct factor of the alternating face map complex (#16071)

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.) Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>