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

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For

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

    Equations
    Instances For
      @[simp]
      theorem AlgebraicTopology.DoldKan.PInfty_f_idem_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (n : ) {Z : C} (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X n Z) :
      CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) h) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) h
      @[simp]
      theorem AlgebraicTopology.DoldKan.PInfty_f_idem {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (n : ) :
      CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) (AlgebraicTopology.DoldKan.PInfty.f n) = AlgebraicTopology.DoldKan.PInfty.f n
      @[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]
      theorem AlgebraicTopology.DoldKan.QInfty_f_idem_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (n : ) {Z : C} (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X n Z) :
      CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.QInfty.f n) (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.QInfty.f n) h) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.QInfty.f n) h
      @[simp]
      theorem AlgebraicTopology.DoldKan.QInfty_f_idem {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (n : ) :
      CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.QInfty.f n) (AlgebraicTopology.DoldKan.QInfty.f n) = AlgebraicTopology.DoldKan.QInfty.f n
      @[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
      @[simp]
      theorem AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (n : ) :
      CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) (AlgebraicTopology.DoldKan.QInfty.f n) = 0
      @[simp]
      theorem AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (n : ) :
      CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.QInfty.f n) (AlgebraicTopology.DoldKan.PInfty.f n) = 0

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

      Equations
      Instances For
        @[simp]

        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.