Colimits of tensor products of scheme-module sheaves

Presheaf tensor preserves colimits objectwise. The arbitrary-sheaf tensor/sheafification comparisons transfer that property to the sheafified tensor in both slots.

The main results are AlgebraicGeometry.Scheme.Modules.tensorLeft_preservesColimitsOfShape and AlgebraicGeometry.Scheme.Modules.tensorRight_preservesColimitsOfShape. Their index categories have the same universe as the underlying scheme site, matching the available presheaf tensor instance. The historical AlgebraicGeometry.Scheme.Modules.tensorLeftFunctor is the canonical tensorLeft, so its finite-colimit and additive instances and AlgebraicGeometry.Scheme.Modules.tensorLeftFreeIso follow here without an invertibility hypothesis.

theorem AlgebraicGeometry.Scheme.Modules.tensorLeft_preservesColimitsOfShape {X : Scheme} (L : X.Modules) (J : Type u) [CategoryTheory.Category.{u, u} J] : CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.MonoidalCategory.tensorLeft L)

Objectwise presheaf tensor preserves colimits, and the sheafification comparison identifies its image with tensoring a module sheaf. The sheafification adjunction then reflects this preservation back to sheaf modules.

theorem AlgebraicGeometry.Scheme.Modules.tensorRight_preservesColimitsOfShape {X : Scheme} (L : X.Modules) (J : Type u) [CategoryTheory.Category.{u, u} J] : CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.MonoidalCategory.tensorRight L)

The right-hand sheafification comparison gives the same colimit preservation without assuming a braided structure on module sheaves.

instance AlgebraicGeometry.Scheme.Modules.tensorLeftFunctor_preservesFiniteColimits {X : Scheme} (L : X.Modules) : CategoryTheory.Limits.PreservesFiniteColimits L.tensorLeftFunctor

Finite colimit preservation used by exact tensoring with an invertible sheaf follows from the all-shapes result, with no invertibility assumption.

instance AlgebraicGeometry.Scheme.Modules.tensorLeftFunctor_additive {X : Scheme} (L : X.Modules) : L.tensorLeftFunctor.Additive

Tensoring by any module sheaf is additive, since it preserves finite coproducts.

noncomputable def AlgebraicGeometry.Scheme.Modules.tensorLeftFreeIso {X : Scheme} (L : X.Modules) (I : Type u) : L.tensorObj (have this := SheafOfModules.free I; this) ≅ ∐ fun (x : I) => L

The free sheaf on any index type is a coproduct of units. Tensoring with a module sheaf preserves this coproduct, and the right unitor identifies each summand.

Equations

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