# mathlib3documentation

algebraic_topology.dold_kan.faces

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

def algebraic_topology.dold_kan.higher_faces_vanish {C : Type u_1} {Y : C} {n : } (q : ) (φ : Y X.obj (opposite.op (simplex_category.mk (n + 1)))) :
Prop

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

Equations
theorem algebraic_topology.dold_kan.higher_faces_vanish.comp_δ_eq_zero_assoc {C : Type u_1} {Y : C} {n q : } {φ : Y X.obj (opposite.op (simplex_category.mk (n + 1)))} (j : fin (n + 2)) (hj₁ : j 0) (hj₂ : n + 2 j + q) {X' : C} (f' : X.obj X') :
φ X.δ j f' = 0 f'
theorem algebraic_topology.dold_kan.higher_faces_vanish.comp_δ_eq_zero {C : Type u_1} {Y : C} {n q : } {φ : Y X.obj (opposite.op (simplex_category.mk (n + 1)))} (j : fin (n + 2)) (hj₁ : j 0) (hj₂ : n + 2 j + q) :
φ X.δ j = 0
theorem algebraic_topology.dold_kan.higher_faces_vanish.of_succ {C : Type u_1} {Y : C} {n q : } {φ : Y X.obj (opposite.op (simplex_category.mk (n + 1)))} (v : φ) :
theorem algebraic_topology.dold_kan.higher_faces_vanish.of_comp {C : Type u_1} {Y Z : C} {q n : } {φ : Y X.obj (opposite.op (simplex_category.mk (n + 1)))} (f : Z Y) :
theorem algebraic_topology.dold_kan.higher_faces_vanish.comp_Hσ_eq {C : Type u_1} {Y : C} {n a q : } {φ : Y X.obj (opposite.op (simplex_category.mk (n + 1)))} (hnaq : n = a + q) :
φ (n + 1) = -φ X.δ a + 1, _⟩ X.σ a, _⟩
theorem algebraic_topology.dold_kan.higher_faces_vanish.comp_Hσ_eq_zero {C : Type u_1} {Y : C} {n q : } {φ : Y X.obj (opposite.op (simplex_category.mk (n + 1)))} (hqn : n < q) :
φ (n + 1) = 0