mathlib documentation


Construction of the projection P_infty for the Dold-Kan correspondence #

TODO (@joelriou) continue adding the various files referenced below

In this file, we construct the projection P_infty : K[X] ⟶ K[X] by passing to the limit the projections P q defined in projections.lean. This projection is a critical tool in this formalisation of the Dold-Kan correspondence, because in the case of abelian categories, P_infty corresponds to the projection on the normalized Moore subcomplex, with kernel the degenerate subcomplex. (See equivalence.lean for the general strategy of proof.)

Given an object Y : karoubi (simplicial_object C), this lemma computes P_infty for the associated object in simplicial_object (karoubi C) in terms of P_infty for Y.X : simplicial_object C and Y.p.