C^dg: cochain complexes as a dg category

For a preadditive category A, the cochain complexes over A form a dg category whose Hom-complexes are Mathlib's CochainComplex.HomComplex.

Every field and every axiom is Mathlib's, not this repository's:

DGCategoryStruct	supplied by
dgHom	CochainComplex.HomComplex
dgId	Cochain.ofHom (𝟙 K)
dgComp	Cochain.comp
dgComp_assoc	Cochain.comp_assoc
dgId_comp, dgComp_id	Cochain.id_comp, Cochain.comp_id
dgId_cocycle	δ_ofHom
dgComp_leibniz	δ_comp

That the last row is a single lemma application rather than a sign argument is the payoff of ADR-0011 and of the convention correction that followed it. An earlier draft of DGCategoryStruct was ModuleCat k-valued, which did not typecheck against HomComplex at all; the draft after it stated the mirror Leibniz rule, which typechecked and was false here. Both were found by trying to write this file.

def CategoryTheory.Cdg (A : Type u) [Category.{v, u} A] [Preadditive A] : Type (max u v)

Cochain complexes over A, carrying their dg structure. A type synonym, so the instance does not attach itself to CochainComplex A ℤ globally.

Equations

• CategoryTheory.Cdg A = CochainComplex A ℤ

def CategoryTheory.Cdg.of (A : Type u) [Category.{v, u} A] [Preadditive A] (K : Cdg A) : CochainComplex A ℤ

The underlying cochain complex.

Equations

• CategoryTheory.Cdg.of A K = K

@[implicit_reducible]

instance CategoryTheory.Cdg.struct {A : Type u} [Category.{v, u} A] [Preadditive A] : DGCategoryStruct (Cdg A)

Equations

• One or more equations did not get rendered due to their size.

The three computation rules that unfold this instance. Each is rfl; they exist so simp can get from a DGCategoryStruct goal to a Cochain one, which is where every Mathlib lemma is stated.

@[simp]

theorem CategoryTheory.Cdg.dgHom_eq {A : Type u} [Category.{v, u} A] [Preadditive A] (K L : Cdg A) : DGCategoryStruct.dgHom K L = (of A K).HomComplex (of A L)

@[simp]

theorem CategoryTheory.Cdg.dgId_eq {A : Type u} [Category.{v, u} A] [Preadditive A] (K : Cdg A) : DGCategoryStruct.dgId K = CochainComplex.HomComplex.Cochain.ofHom (CategoryStruct.id (of A K))

theorem CategoryTheory.Cdg.dgComp_eq {A : Type u} [Category.{v, u} A] [Preadditive A] {K L M : Cdg A} (p q r : ℤ) (h : p + q = r) (f : ↑((DGCategoryStruct.dgHom K L).X p)) (g : ↑((DGCategoryStruct.dgHom L M).X q)) : ((DGCategoryStruct.dgComp p q r h) f) g = CochainComplex.HomComplex.Cochain.comp f g h

@[implicit_reducible]

instance CategoryTheory.Cdg.instDGCategory {A : Type u} [Category.{v, u} A] [Preadditive A] : DGCategory (Cdg A)

C^dg A is a dg category. Every axiom is a Mathlib lemma applied.

Equations

• CategoryTheory.Cdg.instDGCategory = { toDGCategoryStruct := CategoryTheory.Cdg.struct, dgComp_assoc := ⋯, dgId_comp := ⋯, dgComp_id := ⋯, dgId_cocycle := ⋯, dgComp_leibniz := ⋯ }