# Commit 2022-08-24 18:34 fc5b2d2e

View on Github →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.)