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

theorem AlgebraicTopology.DoldKan.P_is_eventually_constant {C : Type u_1} [] {q : } {n : } (hqn : n q) :
theorem AlgebraicTopology.DoldKan.Q_is_eventually_constant {C : Type u_1} [] {q : } {n : } (hqn : n q) :

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

Instances For

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

Instances For
@[simp]
theorem AlgebraicTopology.DoldKan.PInfty_f_0 {C : Type u_1} [] :
HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty 0 =
theorem AlgebraicTopology.DoldKan.PInfty_f {C : Type u_1} [] (n : ) :
HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n =
@[simp]
theorem AlgebraicTopology.DoldKan.QInfty_f_0 {C : Type u_1} [] :
HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty 0 = 0
theorem AlgebraicTopology.DoldKan.QInfty_f {C : Type u_1} [] (n : ) :
HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n =
@[simp]
@[simp]
theorem AlgebraicTopology.DoldKan.PInfty_f_naturality {C : Type u_1} [] (n : ) (f : X Y) :
CategoryTheory.CategoryStruct.comp (f.app ()) (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) (f.app ())
@[simp]
@[simp]
theorem AlgebraicTopology.DoldKan.QInfty_f_naturality {C : Type u_1} [] (n : ) (f : X Y) :
CategoryTheory.CategoryStruct.comp (f.app ()) (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n) (f.app ())
@[simp]
theorem AlgebraicTopology.DoldKan.PInfty_f_idem_assoc {C : Type u_1} [] (n : ) {Z : C} :
CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) h
@[simp]
theorem AlgebraicTopology.DoldKan.PInfty_f_idem {C : Type u_1} [] (n : ) :
CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) = HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n
@[simp]
theorem AlgebraicTopology.DoldKan.PInfty_idem_assoc {C : Type u_1} [] {Z : } :
CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty (CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty h) = CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty h
@[simp]
theorem AlgebraicTopology.DoldKan.PInfty_idem {C : Type u_1} [] :
CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty AlgebraicTopology.DoldKan.PInfty = AlgebraicTopology.DoldKan.PInfty
@[simp]
theorem AlgebraicTopology.DoldKan.QInfty_f_idem_assoc {C : Type u_1} [] (n : ) {Z : C} :
CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n) h
@[simp]
theorem AlgebraicTopology.DoldKan.QInfty_f_idem {C : Type u_1} [] (n : ) :
CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n) (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n) = HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n
@[simp]
theorem AlgebraicTopology.DoldKan.QInfty_idem_assoc {C : Type u_1} [] {Z : } :
CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.QInfty (CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.QInfty h) = CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.QInfty h
@[simp]
theorem AlgebraicTopology.DoldKan.QInfty_idem {C : Type u_1} [] :
CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.QInfty AlgebraicTopology.DoldKan.QInfty = AlgebraicTopology.DoldKan.QInfty
@[simp]
theorem AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f_assoc {C : Type u_1} [] (n : ) {Z : C} :
CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n) h) =
@[simp]
theorem AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f {C : Type u_1} [] (n : ) :
CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n) = 0
@[simp]
theorem AlgebraicTopology.DoldKan.PInfty_comp_QInfty_assoc {C : Type u_1} [] {Z : } :
CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty (CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.QInfty h) =
@[simp]
theorem AlgebraicTopology.DoldKan.PInfty_comp_QInfty {C : Type u_1} [] :
CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty AlgebraicTopology.DoldKan.QInfty = 0
@[simp]
theorem AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f_assoc {C : Type u_1} [] (n : ) {Z : C} :
CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) h) =
@[simp]
theorem AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f {C : Type u_1} [] (n : ) :
CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n) (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) = 0
@[simp]
theorem AlgebraicTopology.DoldKan.QInfty_comp_PInfty_assoc {C : Type u_1} [] {Z : } :
CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.QInfty (CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty h) =
@[simp]
theorem AlgebraicTopology.DoldKan.QInfty_comp_PInfty {C : Type u_1} [] :
CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.QInfty AlgebraicTopology.DoldKan.PInfty = 0
@[simp]
theorem AlgebraicTopology.DoldKan.PInfty_add_QInfty {C : Type u_1} [] :
AlgebraicTopology.DoldKan.PInfty + AlgebraicTopology.DoldKan.QInfty =
theorem AlgebraicTopology.DoldKan.PInfty_f_add_QInfty_f {C : Type u_1} [] (n : ) :
HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n + HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n =
@[simp]
theorem AlgebraicTopology.DoldKan.natTransPInfty_app (C : Type u_1) [] :
∀ (x : ), = AlgebraicTopology.DoldKan.PInfty

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

Instances For
@[simp]
theorem AlgebraicTopology.DoldKan.natTransPInfty_f_app (C : Type u_1) [] (n : ) :
().app X = HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n
noncomputable def AlgebraicTopology.DoldKan.natTransPInfty_f (C : Type u_1) [] (n : ) :

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

Instances For
@[simp]
theorem AlgebraicTopology.DoldKan.map_PInfty_f {C : Type u_1} [] {D : Type u_2} [] (G : ) (n : ) :
HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n = G.map (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n)
theorem AlgebraicTopology.DoldKan.karoubi_PInfty_f {C : Type u_1} [] (n : ) :
(HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n).f = CategoryTheory.CategoryStruct.comp (Y.p.app ()) (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n)

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.