mathlib

3dbd6809 - feat(algebraic_topology/dold_kan): construction of an idempotent endomorphism (#15950)

feat(algebraic_topology/dold_kan): construction of an idempotent endomorphism (#15950) In this PR, we pass to the limit in order to obtain the endomorphism `P_infty : K[X] ⟶ K[X]` of the alternating face map complex. In the case of abelian categories, it shall be the projection on the normalized subcomplex, with kernel the degenerate subcomplex. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>