# mathlib3documentation

algebraic_topology.dold_kan.p_infty

# Construction of the projection P_infty 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 the projection P_infty : K[X] ⟶ K[X] by passing to the limit the projections P q defined in projections.lean. This projection is a critical tool in this formalisation of the Dold-Kan correspondence, because in the case of abelian categories, P_infty corresponds to the projection on the normalized Moore subcomplex, with kernel the degenerate subcomplex.

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

The endomorphism P_infty : K[X] ⟶ K[X] obtained from the P q by passing to the limit.

Equations

The endomorphism Q_infty : K[X] ⟶ K[X] obtained from the Q q by passing to the limit.

Equations
@[simp]
@[simp]
@[simp]
theorem algebraic_topology.dold_kan.P_infty_f_naturality {C : Type u_1} (n : ) (f : X Y) :
@[simp]
theorem algebraic_topology.dold_kan.P_infty_f_naturality_assoc {C : Type u_1} (n : ) (f : X Y) {X' : C} (f' : X') :
=
@[simp]
theorem algebraic_topology.dold_kan.Q_infty_f_naturality {C : Type u_1} (n : ) (f : X Y) :
@[simp]
theorem algebraic_topology.dold_kan.Q_infty_f_naturality_assoc {C : Type u_1} (n : ) (f : X Y) {X' : C} (f' : X') :
=
@[simp]
theorem algebraic_topology.dold_kan.P_infty_f_idem_assoc {C : Type u_1} (n : ) {X' : C} (f' : X') :
@[simp]
@[simp]
@[simp]
@[simp]
theorem algebraic_topology.dold_kan.Q_infty_f_idem_assoc {C : Type u_1} (n : ) {X' : C} (f' : X') :
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem algebraic_topology.dold_kan.P_infty_f_comp_Q_infty_f_assoc {C : Type u_1} (n : ) {X' : C} (f' : X') :
@[simp]
@[simp]
@[simp]
@[simp]
theorem algebraic_topology.dold_kan.Q_infty_f_comp_P_infty_f_assoc {C : Type u_1} (n : ) {X' : C} (f' : X') :
@[simp]
@[simp]
@[simp]

P_infty induces a natural transformation, i.e. an endomorphism of the functor alternating_face_map_complex C.

Equations
@[simp]

The natural transformation in each degree that is induced by nat_trans_P_infty.

Equations
@[simp]
@[simp]
theorem algebraic_topology.dold_kan.map_P_infty_f {C : Type u_1} {D : Type u_3} (G : C D) [G.additive] (n : ) :

Given an object Y : karoubi (simplicial_object C), this lemma computes P_infty for the associated object in simplicial_object (karoubi C) in terms of P_infty for Y.X : simplicial_object C and Y.p.