Documentation

Mathlib.AlgebraicTopology.DoldKan.Projections

Construction of projections for the Dold-Kan correspondence #

In this file, we construct endomorphisms P q : K[X] ⟶ K[X] for all q : ℕ. We study how they behave with respect to face maps with the lemmas HigherFacesVanish.of_P, HigherFacesVanish.comp_P_eq_self and comp_P_eq_self_iff.

Then, we show that they are projections (see P_f_idem and P_idem). They are natural transformations (see natTransP and P_f_naturality) and are compatible with the application of additive functors (see map_P).

By passing to the limit, these endomorphisms P q shall be used in PInfty.lean in order to define PInfty : K[X] ⟶ K[X].

(See Equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)

source
noncomputable def AlgebraicTopology.DoldKan.P {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)

This is the inductive definition of the projections P q : K[X] ⟶ K[X], with P 0 := 𝟙 _ and P (q+1) := P q ≫ (𝟙 _ + Hσ q).

Equations
Instances For
    source
    theorem AlgebraicTopology.DoldKan.P_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} :
    AlgebraicTopology.DoldKan.P 0 = CategoryTheory.CategoryStruct.id (AlgebraicTopology.AlternatingFaceMapComplex.obj X)
    source
    theorem AlgebraicTopology.DoldKan.P_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) :
    AlgebraicTopology.DoldKan.P (q + 1) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.P q) (CategoryTheory.CategoryStruct.id (AlgebraicTopology.AlternatingFaceMapComplex.obj X) + AlgebraicTopology.DoldKan.Hσ q)
    source
    @[simp]
    theorem AlgebraicTopology.DoldKan.P_f_0_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) :
    (AlgebraicTopology.DoldKan.P q).f 0 = CategoryTheory.CategoryStruct.id ((AlgebraicTopology.AlternatingFaceMapComplex.obj X).X 0)

    All the P q coincide with 𝟙 _ in degree 0.

    source
    def AlgebraicTopology.DoldKan.Q {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) :
    AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ AlgebraicTopology.AlternatingFaceMapComplex.obj X

    Q q is the complement projection associated to P q

    Equations
    Instances For
      source
      theorem AlgebraicTopology.DoldKan.P_add_Q {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) :
      AlgebraicTopology.DoldKan.P q + AlgebraicTopology.DoldKan.Q q = CategoryTheory.CategoryStruct.id (AlgebraicTopology.AlternatingFaceMapComplex.obj X)
      source
      theorem AlgebraicTopology.DoldKan.P_add_Q_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) (n : ℕ) :
      (AlgebraicTopology.DoldKan.P q).f n + (AlgebraicTopology.DoldKan.Q q).f n = CategoryTheory.CategoryStruct.id (X.obj (Opposite.op (SimplexCategory.mk n)))
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.Q_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} :
      AlgebraicTopology.DoldKan.Q 0 = 0
      source
      theorem AlgebraicTopology.DoldKan.Q_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) :
      AlgebraicTopology.DoldKan.Q (q + 1) = AlgebraicTopology.DoldKan.Q q - CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.P q) (AlgebraicTopology.DoldKan.Hσ q)
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.Q_f_0_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) :
      (AlgebraicTopology.DoldKan.Q q).f 0 = 0

      All the Q q coincide with 0 in degree 0.

      source
      theorem AlgebraicTopology.DoldKan.HigherFacesVanish.of_P {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) (n : ℕ) :
      AlgebraicTopology.DoldKan.HigherFacesVanish q ((AlgebraicTopology.DoldKan.P q).f (n + 1))

      This lemma expresses the vanishing of (P q).f (n+1) ≫ X.δ k : X _[n+1] ⟶ X _[n] when k≠0 and k≥n-q+2

      source
      theorem AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} {Y : C} {n : ℕ} {q : ℕ} {φ : Y ⟶ X.obj (Opposite.op (SimplexCategory.mk (n + 1)))} (v : AlgebraicTopology.DoldKan.HigherFacesVanish q φ) {Z : C} (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X (n + 1) ⟶ Z) :
      CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P q).f (n + 1)) h) = CategoryTheory.CategoryStruct.comp φ h
      source
      theorem AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} {Y : C} {n : ℕ} {q : ℕ} {φ : Y ⟶ X.obj (Opposite.op (SimplexCategory.mk (n + 1)))} (v : AlgebraicTopology.DoldKan.HigherFacesVanish q φ) :
      CategoryTheory.CategoryStruct.comp φ ((AlgebraicTopology.DoldKan.P q).f (n + 1)) = φ
      source
      theorem AlgebraicTopology.DoldKan.comp_P_eq_self_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} {Y : C} {n : ℕ} {q : ℕ} {φ : Y ⟶ X.obj (Opposite.op (SimplexCategory.mk (n + 1)))} :
      CategoryTheory.CategoryStruct.comp φ ((AlgebraicTopology.DoldKan.P q).f (n + 1)) = φ ↔ AlgebraicTopology.DoldKan.HigherFacesVanish q φ
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.P_f_idem_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) (n : ℕ) {Z : C} (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X n ⟶ Z) :
      CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P q).f n) (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P q).f n) h) = CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P q).f n) h
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.P_f_idem {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) (n : ℕ) :
      CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P q).f n) ((AlgebraicTopology.DoldKan.P q).f n) = (AlgebraicTopology.DoldKan.P q).f n
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.Q_f_idem_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) (n : ℕ) {Z : C} (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj X).X n ⟶ Z) :
      CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Q q).f n) (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Q q).f n) h) = CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Q q).f n) h
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.Q_f_idem {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) (n : ℕ) :
      CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Q q).f n) ((AlgebraicTopology.DoldKan.Q q).f n) = (AlgebraicTopology.DoldKan.Q q).f n
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.P_idem_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) {Z : ChainComplex C ℕ} (h : AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.P q) (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.P q) h) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.P q) h
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.P_idem {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) :
      CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.P q) (AlgebraicTopology.DoldKan.P q) = AlgebraicTopology.DoldKan.P q
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.Q_idem_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) {Z : ChainComplex C ℕ} (h : AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Q q) (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Q q) h) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Q q) h
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.Q_idem {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) :
      CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Q q) (AlgebraicTopology.DoldKan.Q q) = AlgebraicTopology.DoldKan.Q q
      source
      @[simp]
      theorem AlgebraicTopology.DoldKan.natTransP_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (q : ℕ) (X : CategoryTheory.SimplicialObject C) :
      (AlgebraicTopology.DoldKan.natTransP q).app X = AlgebraicTopology.DoldKan.P q
      source
      def AlgebraicTopology.DoldKan.natTransP {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (q : ℕ) :
      AlgebraicTopology.alternatingFaceMapComplex C ⟶ AlgebraicTopology.alternatingFaceMapComplex C

      For each q, P q is a natural transformation.

      Equations
      Instances For
        source
        @[simp]
        theorem AlgebraicTopology.DoldKan.P_f_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (q : ℕ) (n : ℕ) {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) {Z : C} (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj Y).X n ⟶ Z) :
        CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P q).f n) h) = CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P q).f n) (CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) h)
        source
        @[simp]
        theorem AlgebraicTopology.DoldKan.P_f_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (q : ℕ) (n : ℕ) {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) :
        CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) ((AlgebraicTopology.DoldKan.P q).f n) = CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P q).f n) (f.app (Opposite.op (SimplexCategory.mk n)))
        source
        @[simp]
        theorem AlgebraicTopology.DoldKan.Q_f_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (q : ℕ) (n : ℕ) {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) {Z : C} (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj Y).X n ⟶ Z) :
        CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Q q).f n) h) = CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Q q).f n) (CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) h)
        source
        @[simp]
        theorem AlgebraicTopology.DoldKan.Q_f_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (q : ℕ) (n : ℕ) {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) :
        CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) ((AlgebraicTopology.DoldKan.Q q).f n) = CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Q q).f n) (f.app (Opposite.op (SimplexCategory.mk n)))
        source
        @[simp]
        theorem AlgebraicTopology.DoldKan.natTransQ_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (q : ℕ) (X : CategoryTheory.SimplicialObject C) :
        (AlgebraicTopology.DoldKan.natTransQ q).app X = AlgebraicTopology.DoldKan.Q q
        source
        def AlgebraicTopology.DoldKan.natTransQ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (q : ℕ) :
        AlgebraicTopology.alternatingFaceMapComplex C ⟶ AlgebraicTopology.alternatingFaceMapComplex C

        For each q, Q q is a natural transformation.

        Equations
        Instances For
          source
          theorem AlgebraicTopology.DoldKan.map_P {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) (q : ℕ) (n : ℕ) :
          G.map ((AlgebraicTopology.DoldKan.P q).f n) = (AlgebraicTopology.DoldKan.P q).f n
          source
          theorem AlgebraicTopology.DoldKan.map_Q {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) (q : ℕ) (n : ℕ) :
          G.map ((AlgebraicTopology.DoldKan.Q q).f n) = (AlgebraicTopology.DoldKan.Q q).f n