Study of face maps for the Dold-Kan correspondence #
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.
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) = φ.