# mathlib3documentation

algebraic_topology.dold_kan.projections

# Construction of projections 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 construct endomorphisms P q : K[X] ⟶ K[X] for all q : ℕ. We study how they behave with respect to face maps with the lemmas higher_faces_vanish.of_P, higher_faces_vanish.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 nat_trans_P 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 p_infty.lean in order to define P_infty : K[X] ⟶ K[X], see equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.

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

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
@[simp]
theorem algebraic_topology.dold_kan.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
theorem algebraic_topology.dold_kan.P_add_Q_f {C : Type u_1} (q n : ) :
= 𝟙 (X.obj
@[simp]
@[simp]
theorem algebraic_topology.dold_kan.Q_f_0_eq {C : Type u_1} (q : ) :
= 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 algebraic_topology.dold_kan.higher_faces_vanish.comp_P_eq_self {C : Type u_1} {Y : C} {n q : } {φ : Y X.obj (opposite.op (simplex_category.mk (n + 1)))}  :
φ (n + 1) = φ
theorem algebraic_topology.dold_kan.higher_faces_vanish.comp_P_eq_self_assoc {C : Type u_1} {Y : C} {n q : } {φ : Y X.obj (opposite.op (simplex_category.mk (n + 1)))} {X' : C} (f' : X') :
φ (n + 1) f' = φ f'
theorem algebraic_topology.dold_kan.comp_P_eq_self_iff {C : Type u_1} {Y : C} {n q : } {φ : Y X.obj (opposite.op (simplex_category.mk (n + 1)))} :
φ (n + 1) = φ
@[simp]
theorem algebraic_topology.dold_kan.P_f_idem_assoc {C : Type u_1} (q n : ) {X' : C} (f' : X') :
f' = f'
@[simp]
theorem algebraic_topology.dold_kan.P_f_idem {C : Type u_1} (q n : ) :
=
@[simp]
theorem algebraic_topology.dold_kan.Q_f_idem {C : Type u_1} (q n : ) :
=
@[simp]
theorem algebraic_topology.dold_kan.Q_f_idem_assoc {C : Type u_1} (q n : ) {X' : C} (f' : X') :
f' = f'
@[simp]
@[simp]
theorem algebraic_topology.dold_kan.P_idem_assoc {C : Type u_1} (q : ) {X' : }  :
@[simp]
@[simp]
theorem algebraic_topology.dold_kan.Q_idem_assoc {C : Type u_1} (q : ) {X' : }  :

For each q, P q is a natural transformation.

Equations
@[simp]
@[simp]
theorem algebraic_topology.dold_kan.P_f_naturality_assoc {C : Type u_1} (q n : ) (f : X Y) {X' : C} (f' : X') :
f.app f' = f.app f'
@[simp]
theorem algebraic_topology.dold_kan.P_f_naturality {C : Type u_1} (q n : ) (f : X Y) :
f.app = f.app
@[simp]
theorem algebraic_topology.dold_kan.Q_f_naturality_assoc {C : Type u_1} (q n : ) (f : X Y) {X' : C} (f' : X') :
f.app f' = f.app f'
@[simp]
theorem algebraic_topology.dold_kan.Q_f_naturality {C : Type u_1} (q n : ) (f : X Y) :
f.app = f.app
@[simp]

For each q, Q q is a natural transformation.

Equations
theorem algebraic_topology.dold_kan.map_P {C : Type u_1} {D : Type u_3} (G : C D) [G.additive] (q n : ) :
G.map n) =
theorem algebraic_topology.dold_kan.map_Q {C : Type u_1} {D : Type u_3} (G : C D) [G.additive] (q n : ) :
G.map n) =