In this file, we construct the projection
PInfty : K[X] ⟶ K[X] by passing
to the limit the projections
P q defined in
projection is a critical tool in this formalisation of the Dold-Kan correspondence,
because in the case of abelian categories,
PInfty corresponds to the
projection on the normalized Moore subcomplex, with kernel the degenerate subcomplex.
Equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)
PInfty : K[X] ⟶ K[X] obtained from the
P q by passing to the limit.
QInfty : K[X] ⟶ K[X] obtained from the
Q q by passing to the limit.
PInfty induces a natural transformation, i.e. an endomorphism of
The natural transformation in each degree that is induced by