Tensor products and stalks of scheme-module sheaves

For a fixed sheaf of modules, taking a stalk commutes with the ordinary sheafified tensor product, naturally in the second sheaf. The fixed factor need not be flat or locally free.

Main definitions

• AlgebraicGeometry.Scheme.Modules.fixedLeftTensorStalkIso is the natural isomorphism from the tensor of stalks to the stalk of the sheaf tensor.

Main results

The natural isomorphism applies to every scheme, point and fixed module sheaf. It provides the ordinary tensor/stalk comparison used by the later derived pullback acyclicity argument.

Implementation notes

The objectwise comparison passes from bundled module stalks to germ stalks, uses the presheaf tensor/stalk equivalence, then returns through module sheafification. Naturality in the right input follows from the two existing natural comparisons and the pure-tensor naturality theorem.

References

PresheafOfModules.stalkTensorEquiv and PresheafOfModules.stalkTensorEquiv_naturality supply the presheaf comparison; AlgebraicGeometry.Scheme.Modules.presheafModuleStalkSheafificationIso supplies the sheafification comparison.

Tags

module sheaf, tensor product, stalk, natural isomorphism

noncomputable def AlgebraicGeometry.Scheme.Modules.fixedLeftTensorStalkIso (X : Scheme) (x : ↥X) (L : X.Modules) : (moduleStalkFunctor X x).comp (CategoryTheory.MonoidalCategory.tensorLeft ((moduleStalkFunctor X x).obj L)) ≅ (CategoryTheory.MonoidalCategory.tensorLeft L).comp (moduleStalkFunctor X x)

Compose the presheaf tensor/stalk equivalence with the stalk comparison for module sheafification. Both comparisons concern ordinary tensor products, so the fixed factor needs no flatness or local-freeness hypothesis.

Equations

• AlgebraicGeometry.Scheme.Modules.fixedLeftTensorStalkIso X x L = CategoryTheory.NatIso.ofComponents (fun (M : X.Modules) => AlgebraicGeometry.Scheme.Modules.component✝ X x L M) ⋯