The opposite dg category

The sign convention, and why this one

The opposite of a dg category reverses composition and inserts a Koszul sign:

f ∘ᵒᵖ g = (-1) ^ (|f| * |g|) • (g ∘ f).

Without the sign, associativity still holds but the Leibniz rule does not, so the sign is forced rather than chosen. Both checks are recorded here because a sign convention that is only implicit is the usual way two dg developments come to disagree without either noticing.

Associativity. With |f| = p, |g| = q, |h| = r:

• (f ∘ᵒᵖ g) ∘ᵒᵖ h carries (-1) ^ ((p + q) * r + p * q)
• f ∘ᵒᵖ (g ∘ᵒᵖ h) carries (-1) ^ (p * (q + r) + q * r)

and (p + q) * r + p * q = p * (q + r) + q * r.

Leibniz. Under the convention of DerivedAlgGeo.Algebra.Homology.DGCategory/Basic.lean — Mathlib's, δ (f · g) = f · (δg) + (-1) ^ q • (δf) · g — the two sides carry (-1) ^ (p * q) on g · (δf) and (-1) ^ (p * q + p) on (δg) · f, on both sides, once p * (q + 1) = p * q + p and q + (p + 1) * q = p * q + 2 * q are used and (-1) ^ (2 * q) = 1 is discharged. The Koszul sign is unchanged from the earlier draft, which used the mirror convention: only the term-matching moved.

The units live in ℤˣ via Int.negOnePow, matching Mathlib's convention in CochainComplex.HomComplex rather than introducing a second one.

@[implicit_reducible]

instance CategoryTheory.DGCategory.opStruct (C : Type u) [DGCategory C] : DGCategoryStruct Cᵒᵖ

The opposite of a dg category: the same objects, Hom-complexes reversed, composition reversed with a Koszul sign.

Equations

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

theorem CategoryTheory.DGCategory.op_dgComp_apply {C : Type u} [DGCategory C] {X Y Z : Cᵒᵖ} (p q r : ℤ) (h : p + q = r) (f : ↑((DGCategoryStruct.dgHom (Opposite.unop Y) (Opposite.unop X)).X p)) (g : ↑((DGCategoryStruct.dgHom (Opposite.unop Z) (Opposite.unop Y)).X q)) : ((DGCategoryStruct.dgComp p q r h) f) g = (p * q).negOnePow • ((DGCategoryStruct.dgComp q p r ⋯) g) f

@[simp]

theorem CategoryTheory.DGCategory.op_dgHom {C : Type u} [DGCategory C] (X Y : Cᵒᵖ) : DGCategoryStruct.dgHom X Y = DGCategoryStruct.dgHom (Opposite.unop Y) (Opposite.unop X)

@[simp]

theorem CategoryTheory.DGCategory.op_dgId {C : Type u} [DGCategory C] (X : Cᵒᵖ) : DGCategoryStruct.dgId X = DGCategoryStruct.dgId (Opposite.unop X)

theorem CategoryTheory.DGCategory.dgComp_units_smul_left {C : Type u} [DGCategory C] {X Y Z : C} (p q r : ℤ) (h : p + q = r) (c : ℤˣ) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) (g : ↑((DGCategoryStruct.dgHom Y Z).X q)) : ((DGCategoryStruct.dgComp p q r h) (c • f)) g = c • ((DGCategoryStruct.dgComp p q r h) f) g

dgComp is ℤˣ-equivariant in its first argument, because it is additive and the ℤˣ action factors through ℤ.

theorem CategoryTheory.DGCategory.dgComp_units_smul_right {C : Type u} [DGCategory C] {X Y Z : C} (p q r : ℤ) (h : p + q = r) (c : ℤˣ) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) (g : ↑((DGCategoryStruct.dgHom Y Z).X q)) : ((DGCategoryStruct.dgComp p q r h) f) (c • g) = c • ((DGCategoryStruct.dgComp p q r h) f) g

dgComp is ℤˣ-equivariant in its second argument.

theorem CategoryTheory.DGCategory.hom_units_smul {M N : AddCommGrpCat} (φ : M ⟶ N) (c : ℤˣ) (x : ↑M) : (AddCommGrpCat.Hom.hom φ) (c • x) = c • (AddCommGrpCat.Hom.hom φ) x

A morphism of AddCommGrpCat commutes with the ℤˣ action, which factors through ℤ. Stated so the sign bookkeeping below can stay in ℤˣ instead of dropping to ℤ and back.

@[implicit_reducible]

instance CategoryTheory.DGCategory.op {C : Type u} [DGCategory C] : DGCategory Cᵒᵖ

The opposite dg category.

Equations

• CategoryTheory.DGCategory.op = { toDGCategoryStruct := CategoryTheory.DGCategory.opStruct C, dgComp_assoc := ⋯, dgId_comp := ⋯, dgComp_id := ⋯, dgId_cocycle := ⋯, dgComp_leibniz := ⋯ }