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

source
theorem AlgebraicTopology.DoldKan.P_is_eventually_constant {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} {q : ℕ} {n : ℕ} (hqn : n ≤ q) :
HomologicalComplex.Hom.f (AlgebraicTopology.DoldKan.P (q + 1)) n = HomologicalComplex.Hom.f (AlgebraicTopology.DoldKan.P q) n
source
theorem AlgebraicTopology.DoldKan.Q_is_eventually_constant {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} {q : ℕ} {n : ℕ} (hqn : n ≤ q) :
HomologicalComplex.Hom.f (AlgebraicTopology.DoldKan.Q (q + 1)) n = HomologicalComplex.Hom.f (AlgebraicTopology.DoldKan.Q q) n
source
noncomputable def AlgebraicTopology.DoldKan.PInfty {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} :
AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ AlgebraicTopology.AlternatingFaceMapComplex.obj X

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

Instances For
    source
    noncomputable def AlgebraicTopology.DoldKan.QInfty {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} :
    AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ AlgebraicTopology.AlternatingFaceMapComplex.obj X

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

    Instances For
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.PInfty_f_0 {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} :
      HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty 0 = CategoryTheory.CategoryStruct.id (HomologicalComplex.X (AlgebraicTopology.AlternatingFaceMapComplex.obj X) 0)
      source
      theorem AlgebraicTopology.DoldKan.PInfty_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (n : ℕ) :
      HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n = HomologicalComplex.Hom.f (AlgebraicTopology.DoldKan.P n) n
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.QInfty_f_0 {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} :
      HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty 0 = 0
      source
      theorem AlgebraicTopology.DoldKan.QInfty_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (n : ℕ) :
      HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n = HomologicalComplex.Hom.f (AlgebraicTopology.DoldKan.Q n) n
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.PInfty_f_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℕ) {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) {Z : C} (h : HomologicalComplex.X (AlgebraicTopology.AlternatingFaceMapComplex.obj Y) n ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) (CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) h)
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.PInfty_f_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℕ) {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) :
      CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) (f.app (Opposite.op (SimplexCategory.mk n)))
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.QInfty_f_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℕ) {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) {Z : C} (h : HomologicalComplex.X (AlgebraicTopology.AlternatingFaceMapComplex.obj Y) n ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n) (CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) h)
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.QInfty_f_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℕ) {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) :
      CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n) (f.app (Opposite.op (SimplexCategory.mk n)))
      source
      @[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 : HomologicalComplex.X (AlgebraicTopology.AlternatingFaceMapComplex.obj X) n ⟶ Z) :
      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
      source
      @[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 (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) = HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.PInfty_idem_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} {Z : ChainComplex C ℕ} (h : AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ Z) :
      CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty (CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty h) = CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty h
      source
      @[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
      source
      @[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 : HomologicalComplex.X (AlgebraicTopology.AlternatingFaceMapComplex.obj X) n ⟶ Z) :
      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
      source
      @[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 (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n) (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n) = HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.QInfty_idem_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} {Z : ChainComplex C ℕ} (h : AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ Z) :
      CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.QInfty (CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.QInfty h) = CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.QInfty h
      source
      @[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
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (n : ℕ) {Z : C} (h : HomologicalComplex.X (AlgebraicTopology.AlternatingFaceMapComplex.obj X) n ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n) h) = CategoryTheory.CategoryStruct.comp 0 h
      source
      @[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 (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n) = 0
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.PInfty_comp_QInfty_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} {Z : ChainComplex C ℕ} (h : AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ Z) :
      CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty (CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.QInfty h) = CategoryTheory.CategoryStruct.comp 0 h
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.PInfty_comp_QInfty {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.QInfty = 0
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (n : ℕ) {Z : C} (h : HomologicalComplex.X (AlgebraicTopology.AlternatingFaceMapComplex.obj X) n ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) h) = CategoryTheory.CategoryStruct.comp 0 h
      source
      @[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 (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n) (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n) = 0
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.QInfty_comp_PInfty_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} {Z : ChainComplex C ℕ} (h : AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ Z) :
      CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.QInfty (CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty h) = CategoryTheory.CategoryStruct.comp 0 h
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.QInfty_comp_PInfty {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.PInfty = 0
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.PInfty_add_QInfty {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} :
      AlgebraicTopology.DoldKan.PInfty + AlgebraicTopology.DoldKan.QInfty = CategoryTheory.CategoryStruct.id (AlgebraicTopology.AlternatingFaceMapComplex.obj X)
      source
      theorem AlgebraicTopology.DoldKan.PInfty_f_add_QInfty_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (n : ℕ) :
      HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n + HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.QInfty n = CategoryTheory.CategoryStruct.id (HomologicalComplex.X (AlgebraicTopology.AlternatingFaceMapComplex.obj X) n)
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.natTransPInfty_app (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :
      ∀ (x : CategoryTheory.SimplicialObject C), (AlgebraicTopology.DoldKan.natTransPInfty C).app x = AlgebraicTopology.DoldKan.PInfty
      source
      noncomputable def AlgebraicTopology.DoldKan.natTransPInfty (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :
      AlgebraicTopology.alternatingFaceMapComplex C ⟶ AlgebraicTopology.alternatingFaceMapComplex C

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

      Instances For
        source
        @[simp]
        theorem AlgebraicTopology.DoldKan.natTransPInfty_f_app (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℕ) (X : CategoryTheory.SimplicialObject C) :
        (AlgebraicTopology.DoldKan.natTransPInfty_f C n).app X = HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n
        source
        noncomputable def AlgebraicTopology.DoldKan.natTransPInfty_f (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℕ) :
        CategoryTheory.Functor.comp (AlgebraicTopology.alternatingFaceMapComplex C) (HomologicalComplex.eval C (ComplexShape.down ℕ) n) ⟶ CategoryTheory.Functor.comp (AlgebraicTopology.alternatingFaceMapComplex C) (HomologicalComplex.eval C (ComplexShape.down ℕ) n)

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

        Instances For
          source
          @[simp]
          theorem AlgebraicTopology.DoldKan.map_PInfty_f {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] (G : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive G] (X : CategoryTheory.SimplicialObject C) (n : ℕ) :
          HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n = G.map (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n)
          source
          theorem AlgebraicTopology.DoldKan.karoubi_PInfty_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {Y : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)} (n : ℕ) :
          (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty n).f = CategoryTheory.CategoryStruct.comp (Y.p.app (Opposite.op (SimplexCategory.mk n))) (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.