# Construction of projections for the Dold-Kan correspondence #

In this file, we construct endomorphisms P q : K[X] ⟶ K[X] for all q : ℕ. We study how they behave with respect to face maps with the lemmas HigherFacesVanish.of_P, HigherFacesVanish.comp_P_eq_self and comp_P_eq_self_iff.

Then, we show that they are projections (see P_f_idem and P_idem). They are natural transformations (see natTransP and P_f_naturality) and are compatible with the application of additive functors (see map_P).

By passing to the limit, these endomorphisms P q shall be used in PInfty.lean in order to define PInfty : K[X] ⟶ K[X].

(See Equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)

noncomputable def AlgebraicTopology.DoldKan.P {C : Type u_1} [] :

This is the inductive definition of the projections P q : K[X] ⟶ K[X], with P 0 := 𝟙 _ and P (q+1) := P q ≫ (𝟙 _ + Hσ q).

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AlgebraicTopology.DoldKan.P_succ {C : Type u_1} [] (q : ) :
@[simp]
theorem AlgebraicTopology.DoldKan.P_f_0_eq {C : Type u_1} [] (q : ) :

All the P q coincide with 𝟙 _ in degree 0.

Q q is the complement projection associated to P q

Equations
Instances For
theorem AlgebraicTopology.DoldKan.P_add_Q_f {C : Type u_1} [] (q : ) (n : ) :
n + n =
@[simp]
theorem AlgebraicTopology.DoldKan.Q_zero {C : Type u_1} [] :
theorem AlgebraicTopology.DoldKan.Q_succ {C : Type u_1} [] (q : ) :
@[simp]
theorem AlgebraicTopology.DoldKan.Q_f_0_eq {C : Type u_1} [] (q : ) :
0 = 0

All the Q q coincide with 0 in degree 0.

This lemma expresses the vanishing of (P q).f (n+1) ≫ X.δ k : X _[n+1] ⟶ X _[n] when k≠0 and k≥n-q+2

theorem AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self_assoc {C : Type u_1} [] {Y : C} {n : } {q : } {φ : Y X.obj (Opposite.op (SimplexCategory.mk (n + 1)))} {Z : C} (h : (n + 1) Z) :
theorem AlgebraicTopology.DoldKan.comp_P_eq_self_iff {C : Type u_1} [] {Y : C} {n : } {q : } {φ : Y X.obj (Opposite.op (SimplexCategory.mk (n + 1)))} :
@[simp]
theorem AlgebraicTopology.DoldKan.P_f_idem_assoc {C : Type u_1} [] (q : ) (n : ) {Z : C} (h : ) :
@[simp]
theorem AlgebraicTopology.DoldKan.P_f_idem {C : Type u_1} [] (q : ) (n : ) :
= n
@[simp]
theorem AlgebraicTopology.DoldKan.Q_f_idem_assoc {C : Type u_1} [] (q : ) (n : ) {Z : C} (h : ) :
@[simp]
theorem AlgebraicTopology.DoldKan.Q_f_idem {C : Type u_1} [] (q : ) (n : ) :
= n
@[simp]
theorem AlgebraicTopology.DoldKan.P_idem_assoc {C : Type u_1} [] (q : ) {Z : } :
@[simp]
theorem AlgebraicTopology.DoldKan.P_idem {C : Type u_1} [] (q : ) :
@[simp]
theorem AlgebraicTopology.DoldKan.Q_idem_assoc {C : Type u_1} [] (q : ) {Z : } :
@[simp]
theorem AlgebraicTopology.DoldKan.Q_idem {C : Type u_1} [] (q : ) :
@[simp]
theorem AlgebraicTopology.DoldKan.natTransP_app {C : Type u_1} [] (q : ) :

For each q, P q is a natural transformation.

Equations
• = { app := fun (X : ) => , naturality := }
Instances For
@[simp]
theorem AlgebraicTopology.DoldKan.P_f_naturality_assoc {C : Type u_1} [] (q : ) (n : ) (f : X Y) {Z : C} (h : ) :
=
@[simp]
@[simp]
theorem AlgebraicTopology.DoldKan.Q_f_naturality_assoc {C : Type u_1} [] (q : ) (n : ) (f : X Y) {Z : C} (h : ) :
=
@[simp]
@[simp]
theorem AlgebraicTopology.DoldKan.natTransQ_app {C : Type u_1} [] (q : ) :

For each q, Q q is a natural transformation.

Equations
• = { app := fun (X : ) => , naturality := }
Instances For
theorem AlgebraicTopology.DoldKan.map_P {C : Type u_1} [] {D : Type u_2} [] (G : ) [G.Additive] (q : ) (n : ) :
G.map ( n) = n
theorem AlgebraicTopology.DoldKan.map_Q {C : Type u_1} [] {D : Type u_2} [] (G : ) [G.Additive] (q : ) (n : ) :
G.map ( n) = n