Differential graded categories

A differential graded category over a commutative ring R is a category enriched in cochain complexes of R-modules: every Hom object is a complex Hom(X, Y), and composition is a closed degree-zero map out of the tensor product of two Hom complexes.

This file fixes that definition and unpacks the enriched data into the calculus one actually computes with: the R-module DGHom R n X Y of morphisms of degree n, the differential raising the degree by one, the composition of two homogeneous morphisms, and the identity. The enriched axioms then become the associativity and unit laws for that composition, and the fact that composition is a chain map out of the tensor product becomes the graded Leibniz rule

d (dgComp f g) = dgComp (d f) g + (-1) ^ |f| • dgComp f (d g).

The factor order is Mathlib's: CategoryTheory.eComp composes Hom(X, Y) ⊗ Hom(Y, Z) ⟶ Hom(X, Z), so dgComp f g is f followed by g and the Leibniz sign is carried by the degree of the first argument, exactly as in CochainComplex.HomComplex.δ_comp.

The identity is a degree-zero cycle, so the closed degree-zero morphisms form an ordinary category; that category and its quotient by homotopy are not built here.

Main definitions

• TauCeti.DGCategory: a differential graded category over R.
• TauCeti.dgHomComplex: its Hom complex.
• TauCeti.DGHom: the R-module of morphisms of a fixed degree.
• TauCeti.dgDifferential: the differential of the Hom complex.
• TauCeti.dgComp: composition of two homogeneous morphisms.
• TauCeti.dgId: the identity, a degree-zero morphism.

Main results

• TauCeti.dgDifferential_dgComp: the graded Leibniz rule.
• TauCeti.dgComp_assoc: composition of homogeneous morphisms is associative.
• TauCeti.dgId_dgComp and TauCeti.dgComp_dgId: the identity is a two-sided unit.
• TauCeti.dgDifferential_dgId: the identity is a cycle.

References

• B. Keller, Deriving DG categories, Section 1.
• B. Keller, Introduction to A-infinity algebras and modules, Section 3.1, for the sign conventions.
• V. Drinfeld, DG quotients of DG categories, Section 2.

@[reducible, inline]

abbrev TauCeti.DGCategory (R : Type v) [CommRing R] (C : Type u) : Type (max (max u (v + 1)) v)

A differential graded category over a commutative ring R: a category enriched in cochain complexes of R-modules. Its Hom complexes are TauCeti.dgHomComplex, and the morphisms of a fixed degree, their differential, and their composition are TauCeti.DGHom, TauCeti.dgDifferential and TauCeti.dgComp.

Equations

• TauCeti.DGCategory R C = CategoryTheory.EnrichedCategory (CochainComplex (ModuleCat R) ℤ) C

@[reducible, inline]

abbrev TauCeti.dgHomComplex (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : C) : CochainComplex (ModuleCat R) ℤ

The Hom complex of a differential graded category.

Equations

• TauCeti.dgHomComplex R X Y = X ⟶[CochainComplex (ModuleCat R) ℤ] Y

@[reducible, inline]

abbrev TauCeti.DGHom (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (n : ℤ) (X Y : C) : Type v

The R-module of morphisms X ⟶ Y of degree n in a differential graded category.

Equations

• TauCeti.DGHom R n X Y = ↑((TauCeti.dgHomComplex R X Y).X n)

@[reducible, inline]

noncomputable abbrev TauCeti.dgDifferential (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} (n : ℤ) : DGHom R n X Y →ₗ[R] DGHom R (n + 1) X Y

The differential of a differential graded category, raising the degree of a morphism by one.

Equations

• TauCeti.dgDifferential R n = ModuleCat.Hom.hom ((TauCeti.dgHomComplex R X Y).d n (n + 1))

@[simp]

theorem TauCeti.dgDifferential_dgDifferential (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} {n : ℤ} (f : DGHom R n X Y) : (dgDifferential R (n + 1)) ((dgDifferential R n) f) = 0

The differential of a differential graded category squares to zero.

Composition

noncomputable def TauCeti.dgCompMap (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y Z : C) (p q n : ℤ) (h : p + q = n) : CategoryTheory.MonoidalCategoryStruct.tensorObj ((dgHomComplex R X Y).X p) ((dgHomComplex R Y Z).X q) ⟶ (dgHomComplex R X Z).X n

The bidegree-(p, q) component of the enriched composition of a differential graded category: it computes TauCeti.dgComp on a pure tensor.

Equations

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

theorem TauCeti.dgCompMap_def (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y Z : C) (p q n : ℤ) (h : p + q = n) : dgCompMap R X Y Z p q n h = CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj (dgHomComplex R X Y) (dgHomComplex R Y Z) p q n h) ((CategoryTheory.eComp (CochainComplex (ModuleCat R) ℤ) X Y Z).f n)

The bidegree component of enriched composition is the inclusion of that summand of the tensor product of the two Hom complexes, followed by the enriched composition.

noncomputable def TauCeti.dgComp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} {p q n : ℤ} (f : DGHom R p X Y) (g : DGHom R q Y Z) (h : p + q = n) : DGHom R n X Z

Composition of a morphism of degree p from X to Y with a morphism of degree q from Y to Z, in Mathlib's enriched factor order: dgComp f g is f followed by g.

Equations

• TauCeti.dgComp R f g h = (ModuleCat.Hom.hom (TauCeti.dgCompMap R X Y Z p q n h)) (f ⊗ₜ[R] g)

@[simp]

theorem TauCeti.dgCompMap_tmul (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} {p q n : ℤ} (h : p + q = n) (f : DGHom R p X Y) (g : DGHom R q Y Z) : (ModuleCat.Hom.hom (dgCompMap R X Y Z p q n h)) (f ⊗ₜ[R] g) = dgComp R f g h

@[simp]

theorem TauCeti.zero_dgComp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} {p q n : ℤ} (g : DGHom R q Y Z) (h : p + q = n) : dgComp R 0 g h = 0

@[simp]

theorem TauCeti.dgComp_zero (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} {p q n : ℤ} (f : DGHom R p X Y) (h : p + q = n) : dgComp R f 0 h = 0

@[simp]

theorem TauCeti.add_dgComp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} {p q n : ℤ} (f f' : DGHom R p X Y) (g : DGHom R q Y Z) (h : p + q = n) : dgComp R (f + f') g h = dgComp R f g h + dgComp R f' g h

@[simp]

theorem TauCeti.dgComp_add (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} {p q n : ℤ} (f : DGHom R p X Y) (g g' : DGHom R q Y Z) (h : p + q = n) : dgComp R f (g + g') h = dgComp R f g h + dgComp R f g' h

@[simp]

theorem TauCeti.neg_dgComp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} {p q n : ℤ} (f : DGHom R p X Y) (g : DGHom R q Y Z) (h : p + q = n) : dgComp R (-f) g h = -dgComp R f g h

@[simp]

theorem TauCeti.dgComp_neg (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} {p q n : ℤ} (f : DGHom R p X Y) (g : DGHom R q Y Z) (h : p + q = n) : dgComp R f (-g) h = -dgComp R f g h

@[simp]

theorem TauCeti.smul_dgComp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} {p q n : ℤ} (r : R) (f : DGHom R p X Y) (g : DGHom R q Y Z) (h : p + q = n) : dgComp R (r • f) g h = r • dgComp R f g h

@[simp]

theorem TauCeti.dgComp_smul (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} {p q n : ℤ} (r : R) (f : DGHom R p X Y) (g : DGHom R q Y Z) (h : p + q = n) : dgComp R f (r • g) h = r • dgComp R f g h

The Leibniz rule

theorem TauCeti.dgDifferential_dgComp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} {p q n : ℤ} (f : DGHom R p X Y) (g : DGHom R q Y Z) (h : p + q = n) : (dgDifferential R n) (dgComp R f g h) = dgComp R ((dgDifferential R p) f) g ⋯ + p.negOnePow • dgComp R f ((dgDifferential R q) g) ⋯

The graded Leibniz rule in a differential graded category: the differential of a composite differentiates each factor, with the Koszul sign carried by the degree of the first factor.

Associativity

theorem TauCeti.dgComp_assoc (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {W X Y Z : C} {p q r pq qr n : ℤ} (f : DGHom R p W X) (g : DGHom R q X Y) (k : DGHom R r Y Z) (hpq : p + q = pq) (hqr : q + r = qr) (hn : p + q + r = n) : dgComp R (dgComp R f g hpq) k ⋯ = dgComp R f (dgComp R g k hqr) ⋯

Composition of homogeneous morphisms in a differential graded category is associative.

The identity

noncomputable def TauCeti.dgId (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : C) : DGHom R 0 X X

The identity morphism of an object of a differential graded category: the degree-zero morphism named by the enriched identity, that is, the image of 1 under the degree-zero component of CategoryTheory.eId.

Equations

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

theorem TauCeti.dgId_def (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : C) : dgId R X = (ModuleCat.Hom.hom ((CategoryTheory.eId (CochainComplex (ModuleCat R) ℤ) X).f 0)) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R))).inv) 1)

The identity is the image of 1 under the degree-zero component of the enriched identity.

@[simp]

theorem TauCeti.dgDifferential_dgId (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : C) : (dgDifferential R 0) (dgId R X) = 0

The identity of a differential graded category is a cycle, so it is a morphism of the underlying category of closed degree-zero morphisms.

@[simp]

theorem TauCeti.dgId_dgComp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} {q : ℤ} (g : DGHom R q X Y) : dgComp R (dgId R X) g ⋯ = g

The identity is a left unit for composition.

@[simp]

theorem TauCeti.dgComp_dgId (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} {p : ℤ} (f : DGHom R p X Y) : dgComp R f (dgId R Y) ⋯ = f

The identity is a right unit for composition.