Linearity of the tensor product of scheme-module sheaves

The sheafified tensor product is additive in each variable. It is also linear over the ring of global functions, for the Linear Γ(X, ⊤) X.Modules structure, and over the base field for a scheme over a field. Consequently Mathlib's tensorLeft and tensorRight functors inherit Linear instances.

The scalar calculation does not inspect sections of a sheafification. Multiplication by a global function is first identified with the canonical action of an endomorphism of the tensor unit. Monoidal coherence then proves compatibility in the left tensor variable. For the right variable, the objectwise symmetry before sheafification gives a private comparison isomorphism; its naturality reduces the result to the left-variable calculation. This does not assert a SymmetricCategory X.Modules instance: the hexagon laws for the sheafified associator are a separate contract.

No coherence, quasi-coherence, noetherianity, properness, or finite-dimensionality hypothesis enters. In particular, this file supplies the categorical linearity needed to upgrade tensor-Hom equivalences to linear equivalences, but it does not itself prove that any Hom space is finite.

Main results

• Scheme.Modules.modulesMonoidalPreadditive -- tensor is additive in both variables;
• Scheme.Modules.modulesMonoidalLinearGlobal -- tensor is linear over Γ(X, ⊤);
• Variety.modulesMonoidalLinear -- tensor is linear over the base field.

instance AlgebraicGeometry.Scheme.Modules.modulesMonoidalPreadditive {X : Scheme} : CategoryTheory.MonoidalPreadditive X.Modules

Scheme-module sheaves are monoidal preadditive.

Additivity holds before sheafification, objectwise on tensor products of modules. The forgetful functor to presheaves and module sheafification are additive, so the four identities descend to the sheafified tensor product.

theorem AlgebraicGeometry.Scheme.Modules.unitorConj_globalSectionSmul {X : Scheme} (M : X.Modules) (r : ↑(X.presheaf.obj (Opposite.op ⊤))) : M.unitorConj (Cohomology.globalSectionSmul (SheafOfModules.unit X.ringCatSheaf) r) = Cohomology.globalSectionSmul M r

Multiplication by a global function is the tensor-unit action.

The endomorphism of the unit is multiplication by r. Its value on 1 over an open is the restriction of r, so unitorConj_app identifies its canonical action on M with globalSectionSmul M r.

theorem AlgebraicGeometry.Scheme.Modules.tensorHom_id_globalSectionSmul {X : Scheme} (L M : X.Modules) (r : ↑(X.presheaf.obj (Opposite.op ⊤))) : tensorHom (CategoryTheory.CategoryStruct.id L) (Cohomology.globalSectionSmul M r) = Cohomology.globalSectionSmul (L.tensorObj M) r

Tensoring multiplication by a global function on the left factor is multiplication on the tensor product.

After unitorConj_globalSectionSmul, this is a formal monoidal-coherence identity.

instance AlgebraicGeometry.Scheme.Modules.modulesMonoidalLinearGlobal {X : Scheme} : CategoryTheory.MonoidalLinear (↑(X.presheaf.obj (Opposite.op ⊤))) X.Modules

The sheafified tensor product is linear over global functions in both variables.

This is the structure consumed by Mathlib's tensorLeft_linear and tensorRight_linear instances.

instance AlgebraicGeometry.Variety.modulesMonoidalLinear {k : Type u} [Field k] (Y : Scheme) [Y.Over (Spec (CommRingCat.of k))] : CategoryTheory.MonoidalLinear k Y.Modules

For a scheme over a field, tensoring module sheaves is linear over the base field.

The base-field action factors through k → Γ(Y, ⊤), so this is the global-function instance restricted along baseFieldToGlobalSections. No finite-type or separatedness hypothesis is needed.