Cochain complexes as a differential graded category

Cochain complexes in an R-linear preadditive category are enriched in cochain complexes of R-modules through TauCeti.linearHomComplex, so they form a differential graded category. This file evaluates the differential graded operations of TauCeti/CategoryTheory/DG/Basic.lean on that example: the degree-n morphisms are the degree-n cochains, the differential is Mathlib's signed CochainComplex.HomComplex.δ, the identity is the identity cochain, and composition is composition of cochains with the Koszul sign.

That sign is the whole content of the comparison. A differential graded category composes Hom(X, Y) ⊗ Hom(Y, Z) ⟶ Hom(X, Z) while composition of cochains is a closed map out of Hom(Y, Z) ⊗ Hom(X, Y), and interchanging the two factors of a tensor product of complexes is the Koszul braiding. Hence a degree-p cochain z₁ followed by a degree-q cochain z₂ composes to (-1) ^ (p * q) • z₁.comp z₂. This is the bridge between Mathlib's enriched factor order and Keller's untwisted operation m₂ (g, f) = g ∘ f, and it is what fixes the sign conventions of every later differential graded construction.

Main results

• TauCeti.dgDifferential_linearHomComplex, TauCeti.dgId_linearHomComplex and TauCeti.dgComp_linearHomComplex: the differential, identity and composition of this differential graded category.

References

• B. Keller, Introduction to A-infinity algebras and modules, Section 3.1.
• B. Keller, Deriving DG categories, Section 1.

@[simp]

theorem TauCeti.dgDifferential_linearHomComplex (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} (n : ℤ) (z : DGHom R n F G) : (dgDifferential R n) z = CochainComplex.HomComplex.δ n (n + 1) z

The differential of the differential graded category of cochain complexes is the signed differential δ of cochains.

@[simp]

theorem TauCeti.dgId_linearHomComplex (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (F : CochainComplex C ℤ) : dgId R F = CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id F)

The identity of the differential graded category of cochain complexes is the identity cochain.

@[simp]

theorem TauCeti.dgComp_linearHomComplex (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F G K : CochainComplex C ℤ} {p q n : ℤ} (z₁ : DGHom R p F G) (z₂ : DGHom R q G K) (h : p + q = n) : dgComp R z₁ z₂ h = (p * q).negOnePow • CochainComplex.HomComplex.Cochain.comp z₁ z₂ h

Composition in the differential graded category of cochain complexes is composition of cochains, carrying the Koszul sign which converts Mathlib's enriched factor order into Keller's untwisted operation.