Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-27 14:35 735943a2

View on Github →

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.

Estimated changes