Study of face maps 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 obtain the technical lemmas that are used in the file
projections.lean in order to get basic properties of the endomorphisms
P q : K[X] ⟶ K[X] with respect to face maps (see homotopies.lean for the
role of these endomorphisms in the overall strategy of proof).
The main lemma in this file is higher_faces_vanish.induction. It is based
on two technical lemmas higher_faces_vanish.comp_Hσ_eq and
higher_faces_vanish.comp_Hσ_eq_zero.
(See equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)
A morphism φ : Y ⟶ X _[n+1] satisfies higher_faces_vanish q φ
when the compositions φ ≫ X.δ j are 0 for j ≥ max 1 (n+2-q). When q ≤ n+1,
it basically means that the composition φ ≫ X.δ j are 0 for the q highest
possible values of a nonzero j. Otherwise, when q ≥ n+2, all the compositions
φ ≫ X.δ j for nonzero j vanish. See also the lemma comp_P_eq_self_iff in
projections.lean which states that higher_faces_vanish q φ is equivalent to
the identity φ ≫ (P q).f (n+1) = φ.