mathlib documentation


Construction of projections for the Dold-Kan correspondence #

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

In this file, we construct endomorphisms P q : K[X] ⟶ K[X] for all q : ℕ. We study how they behave with respect to face maps with the lemmas higher_faces_vanish.of_P, higher_faces_vanish.comp_P_eq_self and comp_P_eq_self_iff.

Then, we show that they are projections (see P_f_idem and P_idem). They are natural transformations (see nat_trans_P and P_f_naturality) and are compatible with the application of additive functors (see map_P).

By passing to the limit, these endomorphisms P q shall be used in p_infty.lean in order to define P_infty : K[X] ⟶ K[X], see equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.


All the Q q coincide with 0 in degree 0.

This lemma expresses the vanishing of (P q).f (n+1) ≫ X.δ k : X _[n+1] ⟶ X _[n] when k≠0 and k≥n-q+2