Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-01 11:17 9af20344

View on Github →

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.

Estimated changes