Study of face maps for the Dold-Kan correspondence #
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 HigherFacesVanish.induction. It is based
on two technical lemmas HigherFacesVanish.comp_Hσ_eq and
HigherFacesVanish.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 HigherFacesVanish 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 HigherFacesVanish q φ is equivalent to
the identity φ ≫ (P q).f (n+1) = φ.
Equations
- AlgebraicTopology.DoldKan.HigherFacesVanish q φ = ∀ (j : Fin (n + 1)), n + 1 ≤ ↑j + q → CategoryTheory.CategoryStruct.comp φ (CategoryTheory.SimplicialObject.δ X (Fin.succ j)) = 0