Total tensor products of complexes of scheme-module sheaves

The sheafified tensor product is additive in both variables -- Tensor/Linear.lean owns that instance -- and X.Modules has all coproducts. Mathlib's total-complex construction therefore promotes it to a bifunctor on unbounded cochain complexes. This is the underived complex-level input for K-flat localization.

noncomputable def AlgebraicGeometry.Scheme.Modules.totalTensor (X : Scheme) : CategoryTheory.Functor (CochainComplex X.Modules ℤ) (CategoryTheory.Functor (CochainComplex X.Modules ℤ) (CochainComplex X.Modules ℤ))

The total tensor product of two unbounded cochain complexes of module sheaves.

Equations

• AlgebraicGeometry.Scheme.Modules.totalTensor X = (CategoryTheory.MonoidalCategory.curriedTensor X.Modules).map₂CochainComplex

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.totalTensor_obj_obj (X : Scheme) (K L : CochainComplex X.Modules ℤ) : ((totalTensor X).obj K).obj L = HomologicalComplex.tensorObj K L