Tensor products of differential graded categories

The tensor product of two differential graded categories C and D over R has the pairs (X, Y) as objects, and its Hom complex from (X, Y) to (X', Y') is the tensor product Hom(X, X') ⊗ Hom(Y, Y') of cochain complexes. It is the tensor product TauCeti.tensorEnrichedCategory of categories enriched in cochain complexes of R-modules, whose braiding is the Koszul braiding TauCeti.koszulBraidedCategory.

This file makes the structure explicit on homogeneous morphisms. For f : X ⟶ X' of degree p and g : Y ⟶ Y' of degree q, the morphism f ⊗ g : (X, Y) ⟶ (X', Y') of degree p + q is TauCeti.dgTensorHom f g. Every morphism of the tensor product is a sum of these, and

• d (f ⊗ g) = d f ⊗ g + (-1) ^ p • f ⊗ d g;
• dgComp (f ⊗ g) (f' ⊗ g') = (-1) ^ (q * p') • dgComp f f' ⊗ dgComp g g', where p' is the degree of f': composition moves g past f', with the Koszul sign;
• the identity of (X, Y) is 1_X ⊗ 1_Y.

Tensor products are how DG bimodules are compared with modules: a DG bimodule with a left action of A and a right action of B is a right DG module over the tensor product of the opposite of A with B.

Main definitions

• TauCeti.dgTensorHom: the tensor product of two homogeneous morphisms.

Main results

• TauCeti.dgTensorHom_induction: the tensor products of homogeneous morphisms span every R-module of morphisms of a fixed degree.
• TauCeti.dgDifferential_dgTensorHom: the differential of a tensor product of morphisms.
• TauCeti.dgCompMap_tensor: composition on a homogeneous summand of the tensor product.
• TauCeti.dgComp_dgTensorHom: composition of tensor products of morphisms, with its Koszul sign.
• TauCeti.dgId_tensor: identities are tensor products of identities.

References

• B. Keller, Deriving DG categories, Section 1.
• V. Drinfeld, DG quotients of DG categories, Section 2.
• G. M. Kelly, Basic concepts of enriched category theory, Section 1.4.

noncomputable def TauCeti.dgTensorHom (R : Type v) [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {X Y : C × D} {p q n : ℤ} (f : DGHom R p X.1 Y.1) (g : DGHom R q X.2 Y.2) (h : p + q = n) : DGHom R n X Y

The tensor product f ⊗ g : X ⟶ Y in the tensor product of two differential graded categories, of degree n = p + q, of a morphism f : X.1 ⟶ Y.1 of degree p and a morphism g : X.2 ⟶ Y.2 of degree q.

Equations

• TauCeti.dgTensorHom R f g h = (ModuleCat.Hom.hom (HomologicalComplex.ιTensorObj (TauCeti.dgHomComplex R X.1 Y.1) (TauCeti.dgHomComplex R X.2 Y.2) p q n h)) (f ⊗ₜ[R] g)

theorem TauCeti.dgTensorHom_def (R : Type v) [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {X Y : C × D} {p q n : ℤ} (f : DGHom R p X.1 Y.1) (g : DGHom R q X.2 Y.2) (h : p + q = n) : dgTensorHom R f g h = (ModuleCat.Hom.hom (HomologicalComplex.ιTensorObj (dgHomComplex R X.1 Y.1) (dgHomComplex R X.2 Y.2) p q n h)) (f ⊗ₜ[R] g)

The tensor product of two homogeneous morphisms is the image of f ⊗ₜ g under the inclusion of the bidegree-(p, q) summand of the tensor product of the two Hom complexes.

@[simp]

theorem TauCeti.zero_dgTensorHom {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {X Y : C × D} {p q n : ℤ} (g : DGHom R q X.2 Y.2) (h : p + q = n) : dgTensorHom R 0 g h = 0

@[simp]

theorem TauCeti.dgTensorHom_zero {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {X Y : C × D} {p q n : ℤ} (f : DGHom R p X.1 Y.1) (h : p + q = n) : dgTensorHom R f 0 h = 0

@[simp]

theorem TauCeti.add_dgTensorHom {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {X Y : C × D} {p q n : ℤ} (f f' : DGHom R p X.1 Y.1) (g : DGHom R q X.2 Y.2) (h : p + q = n) : dgTensorHom R (f + f') g h = dgTensorHom R f g h + dgTensorHom R f' g h

@[simp]

theorem TauCeti.dgTensorHom_add {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {X Y : C × D} {p q n : ℤ} (f : DGHom R p X.1 Y.1) (g g' : DGHom R q X.2 Y.2) (h : p + q = n) : dgTensorHom R f (g + g') h = dgTensorHom R f g h + dgTensorHom R f g' h

@[simp]

theorem TauCeti.neg_dgTensorHom {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {X Y : C × D} {p q n : ℤ} (f : DGHom R p X.1 Y.1) (g : DGHom R q X.2 Y.2) (h : p + q = n) : dgTensorHom R (-f) g h = -dgTensorHom R f g h

@[simp]

theorem TauCeti.dgTensorHom_neg {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {X Y : C × D} {p q n : ℤ} (f : DGHom R p X.1 Y.1) (g : DGHom R q X.2 Y.2) (h : p + q = n) : dgTensorHom R f (-g) h = -dgTensorHom R f g h

@[simp]

theorem TauCeti.smul_dgTensorHom {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {X Y : C × D} {p q n : ℤ} (r : R) (f : DGHom R p X.1 Y.1) (g : DGHom R q X.2 Y.2) (h : p + q = n) : dgTensorHom R (r • f) g h = r • dgTensorHom R f g h

@[simp]

theorem TauCeti.dgTensorHom_smul {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {X Y : C × D} {p q n : ℤ} (r : R) (f : DGHom R p X.1 Y.1) (g : DGHom R q X.2 Y.2) (h : p + q = n) : dgTensorHom R f (r • g) h = r • dgTensorHom R f g h

theorem TauCeti.dgTensorHom_induction (R : Type v) [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {X Y : C × D} {n : ℤ} {motive : DGHom R n X Y → Prop} (zero : motive 0) (tmul : ∀ (p q : ℤ) (h : p + q = n) (f : DGHom R p X.1 Y.1) (g : DGHom R q X.2 Y.2), motive (dgTensorHom R f g h)) (add : ∀ (x y : DGHom R n X Y), motive x → motive y → motive (x + y)) (x : DGHom R n X Y) : motive x

Induction on morphisms of a tensor product of differential graded categories: a property of the morphisms of degree n which holds for 0 and for every tensor product of homogeneous morphisms, and is closed under addition, holds for every morphism of degree n.

theorem TauCeti.dgDifferential_dgTensorHom (R : Type v) [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {X Y : C × D} {p q n : ℤ} (f : DGHom R p X.1 Y.1) (g : DGHom R q X.2 Y.2) (h : p + q = n) : (dgDifferential R n) (dgTensorHom R f g h) = dgTensorHom R ((dgDifferential R p) f) g ⋯ + p.negOnePow • dgTensorHom R f ((dgDifferential R q) g) ⋯

The differential of a tensor product of homogeneous morphisms differentiates each factor, with the Koszul sign (-1) ^ p of the degree p of the first factor on the second term.

theorem TauCeti.dgCompMap_tensor (R : Type v) [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] (X Y Z : C × D) (p q p' q' n n' m : ℤ) (h : p + q = n) (h' : p' + q' = n') (hm : n + n' = m) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (HomologicalComplex.ιTensorObj (dgHomComplex R X.1 Y.1) (dgHomComplex R X.2 Y.2) p q n h) (HomologicalComplex.ιTensorObj (dgHomComplex R Y.1 Z.1) (dgHomComplex R Y.2 Z.2) p' q' n' h')) (dgCompMap R X Y Z n n' m hm) = (q * p').negOnePow • CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ ((dgHomComplex R X.1 Y.1).X p) ((dgHomComplex R X.2 Y.2).X q) ((dgHomComplex R Y.1 Z.1).X p') ((dgHomComplex R Y.2 Z.2).X q')) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (dgCompMap R X.1 Y.1 Z.1 p p' (p + p') ⋯) (dgCompMap R X.2 Y.2 Z.2 q q' (q + q') ⋯)) (HomologicalComplex.ιTensorObj (dgHomComplex R X.1 Z.1) (dgHomComplex R X.2 Z.2) (p + p') (q + q') m ⋯))

Composition in the tensor product on the summand of bidegrees ((p, q), (p', q')): interchange the two middle factors, with the Koszul sign (-1) ^ (q * p'), then compose in each factor.

@[simp]

theorem TauCeti.dgComp_dgTensorHom (R : Type v) [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {X Y Z : C × D} {p q p' q' n n' m : ℤ} (f : DGHom R p X.1 Y.1) (g : DGHom R q X.2 Y.2) (f' : DGHom R p' Y.1 Z.1) (g' : DGHom R q' Y.2 Z.2) (h : p + q = n) (h' : p' + q' = n') (hm : n + n' = m) : dgComp R (dgTensorHom R f g h) (dgTensorHom R f' g' h') hm = (q * p').negOnePow • dgTensorHom R (dgComp R f f' ⋯) (dgComp R g g' ⋯) ⋯

Composition in a tensor product of differential graded categories. For homogeneous morphisms f, g, f', g' of degrees p, q, p', q', the composite of f ⊗ g and f' ⊗ g' is dgComp f f' ⊗ dgComp g g' up to the Koszul sign (-1) ^ (q * p') of moving g past f'.

theorem TauCeti.dgId_tensor (R : Type v) [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] (X : C × D) : dgId R X = dgTensorHom R (dgId R X.1) (dgId R X.2) ⋯

The identity of an object of the tensor product of two differential graded categories is the tensor product of the identities of its two components.