feat(algebraic_topology/dold_kan): decomposition of Q (#16357)
In this PR, a decomposition of the endomorphisms `Q q` acting on `X _[n+1]` is obtained. In the case of abelian categories, it shows that the image of `Q q` is contained in a certain sum of images of degeneracy operators. Critical tools are also introduced in order to show (in a future PR) that the normalized Moore complex functor reflects isomorphisms.
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
