mathlib

735943a2 - feat(algebraic_topology/dold_kan): construction of idempotent endomorphisms (#15616)

feat(algebraic_topology/dold_kan): construction of idempotent endomorphisms (#15616) This PR introduces a sequence of idempotent endomorphisms of the alternating face map complex of a simplicial object in a preadditive category. In a future PR, by taking the "limit" of this sequence, we shall get the projection on the normalized subcomplex, parallel to the degenerate sucomplex.