Opposite differential graded categories

The opposite of a differential graded category is obtained from the opposite enriched category. Its Hom complex from op X to op Y is the original Hom complex from Y to X. Composition first uses the Koszul braiding to reverse the two homogeneous factors. Consequently, for degrees p and q, opposite composition is (-1)^(p*q) times the original composition in reversed order. These identifications let calculations in the opposite category use the same differential and the signed composition formulas of the original category.

Mathlib supplies the opposite of a category enriched in a braided monoidal category. The SymmetricCategory instance on cochain complexes and its Koszul sign are supplied by TauCeti.Algebra.Homology.Monoidal.Braiding.

References

• B. Keller, Deriving DG categories, Section 1.
• Mathlib.CategoryTheory.Enriched.Opposite, for the opposite enriched category.

@[simp]

theorem TauCeti.dgHomComplex_op (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : C) : dgHomComplex R (Opposite.op X) (Opposite.op Y) = dgHomComplex R Y X

The Hom complex from op X to op Y in the opposite DG category is the Hom complex from Y to X in the original category.

@[simp]

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

The differential in the opposite DG category is the original differential with source and target reversed.

@[simp]

theorem TauCeti.dgId_op (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : C) : dgId R (Opposite.op X) = dgId R X

The identity in the opposite DG category is the original identity.

theorem TauCeti.dgCompMap_op (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y Z : C) (p q n : ℤ) (h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = n) : dgCompMap R (Opposite.op X) (Opposite.op Y) (Opposite.op Z) p q n h = (p * q).negOnePow • CategoryTheory.CategoryStruct.comp (β_ ((dgHomComplex R Y X).X p) ((dgHomComplex R Z Y).X q)).hom (dgCompMap R Z Y X q p n ⋯)

On the bidegree-(p,q) summand, composition in the opposite DG category is composition in the original category after swapping the two factors with the Koszul sign.

@[simp]

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

Composition in the opposite DG category reverses the factors and contributes the Koszul sign. The sign is the value of the cochain-complex braiding on the bidegree-(p,q) summand.