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.)