# Documentation

Mathlib.AlgebraicTopology.DoldKan.Faces

# 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.)

def AlgebraicTopology.DoldKan.HigherFacesVanish {C : Type u_1} [] {Y : C} {n : } (q : ) (φ : Y X.obj (Opposite.op (SimplexCategory.mk (n + 1)))) :

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) = φ.

Instances For
theorem AlgebraicTopology.DoldKan.HigherFacesVanish.comp_δ_eq_zero_assoc {C : Type u_1} [] {Y : C} {n : } {q : } {φ : Y X.obj (Opposite.op (SimplexCategory.mk (n + 1)))} (j : Fin (n + 2)) (hj₁ : j 0) (hj₂ : n + 2 j + q) {Z : C} (h : X.obj () Z) :
theorem AlgebraicTopology.DoldKan.HigherFacesVanish.comp_δ_eq_zero {C : Type u_1} [] {Y : C} {n : } {q : } {φ : Y X.obj (Opposite.op (SimplexCategory.mk (n + 1)))} (j : Fin (n + 2)) (hj₁ : j 0) (hj₂ : n + 2 j + q) :
theorem AlgebraicTopology.DoldKan.HigherFacesVanish.of_succ {C : Type u_1} [] {Y : C} {n : } {q : } {φ : Y X.obj (Opposite.op (SimplexCategory.mk (n + 1)))} (v : ) :
theorem AlgebraicTopology.DoldKan.HigherFacesVanish.of_comp {C : Type u_1} [] {Y : C} {Z : C} {q : } {n : } {φ : Y X.obj (Opposite.op (SimplexCategory.mk (n + 1)))} (f : Z Y) :
theorem AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq {C : Type u_1} [] {Y : C} {n : } {a : } {q : } {φ : Y X.obj (Opposite.op (SimplexCategory.mk (n + 1)))} (hnaq : n = a + q) :
theorem AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq_zero {C : Type u_1} [] {Y : C} {n : } {q : } {φ : Y X.obj (Opposite.op (SimplexCategory.mk (n + 1)))} (hqn : n < q) :