Construction of projections for the Dold-Kan correspondence #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
Then, we show that they are projections (see
P_idem). They are natural transformations (see
P_f_naturality) and are compatible with the application
of additive functors (see
By passing to the limit, these endomorphisms
P q shall be used in
in order to define
P_infty : K[X] ⟶ K[X], see
equivalence.lean for the general
strategy of proof of the Dold-Kan equivalence.
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],
P 0 := 𝟙 _ and
P (q+1) := P q ≫ (𝟙 _ + Hσ q).
P q coincide with
𝟙 _ in degree 0.
Q q is the complement projection associated to
This lemma expresses the vanishing of
(P q).f (n+1) ≫ X.δ k : X _[n+1] ⟶ X _[n] when
P q is a natural transformation.
Q q is a natural transformation.