Documentation

Mathlib.AlgebraicTopology.DoldKan.PInfty

Construction of the projection PInfty for the Dold-Kan correspondence #

In this file, we construct the projection PInfty : 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, PInfty 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.)

@[simp]
@[simp]
theorem AlgebraicTopology.DoldKan.PInfty_idem {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} :
CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty AlgebraicTopology.DoldKan.PInfty = AlgebraicTopology.DoldKan.PInfty
@[simp]
@[simp]
theorem AlgebraicTopology.DoldKan.QInfty_idem {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} :
CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.QInfty AlgebraicTopology.DoldKan.QInfty = AlgebraicTopology.DoldKan.QInfty

PInfty induces a natural transformation, i.e. an endomorphism of the functor alternatingFaceMapComplex C.

Instances For

    Given an object Y : Karoubi (SimplicialObject C), this lemma computes PInfty for the associated object in SimplicialObject (Karoubi C) in terms of PInfty for Y.X : SimplicialObject C and Y.p.