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) :
(P (q + 1)).f n = (P q).f 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) :
(Q (q + 1)).f n = (Q q).f 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} :
AlternatingFaceMapComplex.obj X ⟶ AlternatingFaceMapComplex.obj X

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
    source
    noncomputable def AlgebraicTopology.DoldKan.QInfty {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} :
    AlternatingFaceMapComplex.obj X ⟶ AlternatingFaceMapComplex.obj X

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

    Equations
    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} :
      PInfty.f 0 = CategoryTheory.CategoryStruct.id ((AlternatingFaceMapComplex.obj X).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 : ℕ) :
      PInfty.f n = (P n).f 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} :
      QInfty.f 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 : ℕ) :
      QInfty.f n = (Q n).f n
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.PInfty_f_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℕ) {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) :
      CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) (PInfty.f n) = CategoryTheory.CategoryStruct.comp (PInfty.f n) (f.app (Opposite.op (SimplexCategory.mk 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 Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) {Z : C} (h : (AlternatingFaceMapComplex.obj Y).X n ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) (CategoryTheory.CategoryStruct.comp (PInfty.f n) h) = CategoryTheory.CategoryStruct.comp (PInfty.f 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 Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) :
      CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) (QInfty.f n) = CategoryTheory.CategoryStruct.comp (QInfty.f 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 Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) {Z : C} (h : (AlternatingFaceMapComplex.obj Y).X n ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) (CategoryTheory.CategoryStruct.comp (QInfty.f n) h) = CategoryTheory.CategoryStruct.comp (QInfty.f n) (CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk 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 (PInfty.f n) (PInfty.f n) = PInfty.f 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 : (AlternatingFaceMapComplex.obj X).X n ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (PInfty.f n) (CategoryTheory.CategoryStruct.comp (PInfty.f n) h) = CategoryTheory.CategoryStruct.comp (PInfty.f n) 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 PInfty PInfty = PInfty
      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 : AlternatingFaceMapComplex.obj X ⟶ Z) :
      CategoryTheory.CategoryStruct.comp PInfty (CategoryTheory.CategoryStruct.comp PInfty h) = CategoryTheory.CategoryStruct.comp PInfty 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 (QInfty.f n) (QInfty.f n) = QInfty.f n
      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 : (AlternatingFaceMapComplex.obj X).X n ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (QInfty.f n) (CategoryTheory.CategoryStruct.comp (QInfty.f n) h) = CategoryTheory.CategoryStruct.comp (QInfty.f n) 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 QInfty QInfty = QInfty
      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 : AlternatingFaceMapComplex.obj X ⟶ Z) :
      CategoryTheory.CategoryStruct.comp QInfty (CategoryTheory.CategoryStruct.comp QInfty h) = CategoryTheory.CategoryStruct.comp QInfty 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 (PInfty.f n) (QInfty.f n) = 0
      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 : (AlternatingFaceMapComplex.obj X).X n ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (PInfty.f n) (CategoryTheory.CategoryStruct.comp (QInfty.f n) 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 PInfty QInfty = 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 : AlternatingFaceMapComplex.obj X ⟶ Z) :
      CategoryTheory.CategoryStruct.comp PInfty (CategoryTheory.CategoryStruct.comp QInfty 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 (QInfty.f n) (PInfty.f n) = 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 : (AlternatingFaceMapComplex.obj X).X n ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (QInfty.f n) (CategoryTheory.CategoryStruct.comp (PInfty.f n) 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 QInfty PInfty = 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 : AlternatingFaceMapComplex.obj X ⟶ Z) :
      CategoryTheory.CategoryStruct.comp QInfty (CategoryTheory.CategoryStruct.comp PInfty h) = CategoryTheory.CategoryStruct.comp 0 h
      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} :
      PInfty + QInfty = CategoryTheory.CategoryStruct.id (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 : ℕ) :
      PInfty.f n + QInfty.f n = CategoryTheory.CategoryStruct.id ((AlternatingFaceMapComplex.obj X).X n)
      source
      noncomputable def AlgebraicTopology.DoldKan.natTransPInfty (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] :
      alternatingFaceMapComplex C ⟶ alternatingFaceMapComplex C

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

      Equations
      Instances For
        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) :
        (natTransPInfty C).app x✝ = PInfty
        source
        noncomputable def AlgebraicTopology.DoldKan.natTransPInfty_f (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (n : ℕ) :
        (alternatingFaceMapComplex C).comp (HomologicalComplex.eval C (ComplexShape.down ℕ) n) ⟶ (alternatingFaceMapComplex C).comp (HomologicalComplex.eval C (ComplexShape.down ℕ) n)

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

        Equations
        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) :
          (natTransPInfty_f C n).app X = PInfty.f n
          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) [G.Additive] (X : CategoryTheory.SimplicialObject C) (n : ℕ) :
          PInfty.f n = G.map (PInfty.f 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 : ℕ) :
          (PInfty.f n).f = CategoryTheory.CategoryStruct.comp (Y.p.app (Opposite.op (SimplexCategory.mk n))) (PInfty.f 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.