Construction of projections for the Dold-Kan correspondence #

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 HigherFacesVanish.of_P, HigherFacesVanish.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 natTransP 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 PInfty.lean in order to define PInfty : K[X] ⟶ K[X].

(See Equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)

This is the inductive definition of the projections P q : K[X] ⟶ K[X], with P 0 := 𝟙 _ and P (q+1) := P q ≫ (𝟙 _ + Hσ q).

Instances For

    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