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

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

• One or more equations did not get rendered due to their size.
• AlgebraicTopology.DoldKan.P 0 = CategoryTheory.CategoryStruct.id (AlgebraicTopology.AlternatingFaceMapComplex.obj X)

theorem AlgebraicTopology.DoldKan.P_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} : P 0 = CategoryTheory.CategoryStruct.id (AlternatingFaceMapComplex.obj X)

theorem AlgebraicTopology.DoldKan.P_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) : P (q + 1) = CategoryTheory.CategoryStruct.comp (P q) (CategoryTheory.CategoryStruct.id (AlternatingFaceMapComplex.obj X) + Hσ q)

@[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 : ℕ) : (P q).f 0 = CategoryTheory.CategoryStruct.id ((AlternatingFaceMapComplex.obj X).X 0)

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

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

Q q is the complement projection associated to P q

Equations

• AlgebraicTopology.DoldKan.Q q = CategoryTheory.CategoryStruct.id (AlgebraicTopology.AlternatingFaceMapComplex.obj X) - AlgebraicTopology.DoldKan.P q

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 : ℕ) : P q + Q q = CategoryTheory.CategoryStruct.id (AlternatingFaceMapComplex.obj X)

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 : ℕ) : (P q).f n + (Q q).f n = CategoryTheory.CategoryStruct.id (X.obj (Opposite.op (SimplexCategory.mk n)))

@[simp]

theorem AlgebraicTopology.DoldKan.Q_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} : Q 0 = 0

theorem AlgebraicTopology.DoldKan.Q_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (q : ℕ) : Q (q + 1) = Q q - CategoryTheory.CategoryStruct.comp (P q) (Hσ q)

@[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 : ℕ) : (Q q).f 0 = 0

All the Q q coincide with 0 in degree 0.

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 : ℕ) : HigherFacesVanish q ((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

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 : HigherFacesVanish q φ) : CategoryTheory.CategoryStruct.comp φ ((P q).f (n + 1)) = φ

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 : HigherFacesVanish q φ) {Z : C} (h : (AlternatingFaceMapComplex.obj X).X (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp ((P q).f (n + 1)) h) = CategoryTheory.CategoryStruct.comp φ h

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 φ ((P q).f (n + 1)) = φ ↔ HigherFacesVanish q φ

@[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 ((P q).f n) ((P q).f n) = (P q).f n

@[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 : (AlternatingFaceMapComplex.obj X).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((P q).f n) (CategoryTheory.CategoryStruct.comp ((P q).f n) h) = CategoryTheory.CategoryStruct.comp ((P q).f n) h

@[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 ((Q q).f n) ((Q q).f n) = (Q q).f n

@[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 : (AlternatingFaceMapComplex.obj X).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((Q q).f n) (CategoryTheory.CategoryStruct.comp ((Q q).f n) h) = CategoryTheory.CategoryStruct.comp ((Q q).f n) h

@[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 (P q) (P q) = P q

@[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 : AlternatingFaceMapComplex.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (P q) (CategoryTheory.CategoryStruct.comp (P q) h) = CategoryTheory.CategoryStruct.comp (P q) h

@[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 (Q q) (Q q) = Q q

@[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 : AlternatingFaceMapComplex.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (Q q) (CategoryTheory.CategoryStruct.comp (Q q) h) = CategoryTheory.CategoryStruct.comp (Q q) h

def AlgebraicTopology.DoldKan.natTransP {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (q : ℕ) : alternatingFaceMapComplex C ⟶ alternatingFaceMapComplex C

For each q, P q is a natural transformation.

Equations

• AlgebraicTopology.DoldKan.natTransP q = { app := fun (x : CategoryTheory.SimplicialObject C) => AlgebraicTopology.DoldKan.P q, naturality := ⋯ }

@[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) : (natTransP q).app x✝ = P q

@[simp]

theorem AlgebraicTopology.DoldKan.P_f_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (q n : ℕ) {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) ((P q).f n) = CategoryTheory.CategoryStruct.comp ((P q).f n) (f.app (Opposite.op (SimplexCategory.mk n)))

@[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 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 ((P q).f n) h) = CategoryTheory.CategoryStruct.comp ((P q).f n) (CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) h)

@[simp]

theorem AlgebraicTopology.DoldKan.Q_f_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (q n : ℕ) {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) ((Q q).f n) = CategoryTheory.CategoryStruct.comp ((Q q).f n) (f.app (Opposite.op (SimplexCategory.mk n)))

@[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 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 ((Q q).f n) h) = CategoryTheory.CategoryStruct.comp ((Q q).f n) (CategoryTheory.CategoryStruct.comp (f.app (Opposite.op (SimplexCategory.mk n))) h)

def AlgebraicTopology.DoldKan.natTransQ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (q : ℕ) : alternatingFaceMapComplex C ⟶ alternatingFaceMapComplex C

For each q, Q q is a natural transformation.

Equations

• AlgebraicTopology.DoldKan.natTransQ q = { app := fun (x : CategoryTheory.SimplicialObject C) => AlgebraicTopology.DoldKan.Q q, naturality := ⋯ }

@[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) : (natTransQ q).app x✝ = Q q

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) [G.Additive] (X : CategoryTheory.SimplicialObject C) (q n : ℕ) : G.map ((P q).f n) = (P q).f n

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) [G.Additive] (X : CategoryTheory.SimplicialObject C) (q n : ℕ) : G.map ((Q q).f n) = (Q q).f n