The tensor product of 𝒪ₓ-modules on a scheme

The site-level symmetric monoidal structure on sheaves of modules (TauCeti/Algebra/Category/ModuleCat/Sheaf/TensorProduct/Monoidal.lean) specializes to a scheme X by taking the sheaf of commutative rings to be the structure sheaf of X, so the tensor product of 𝒪ₓ-modules is M ⊗ N.

Main declarations

• AlgebraicGeometry.Scheme.Modules.instMonoidalCategory and AlgebraicGeometry.Scheme.Modules.instSymmetricCategory make X.Modules a symmetric monoidal category, with unit 𝒪ₓ; they are the site-level structures TauCeti.SheafOfModules.monoidalCategory and TauCeti.SheafOfModules.symmetricCategory;
• AlgebraicGeometry.Scheme.Modules.instMonoidalClosed makes tensoring an 𝒪ₓ-module on the left adjoint to its internal Hom functor;
• AlgebraicGeometry.Scheme.Modules.isQuasicoherent_tensorObj and AlgebraicGeometry.Scheme.Modules.isMonoidal_isQuasicoherent: tensor products of quasi-coherent 𝒪ₓ-modules are quasi-coherent, so quasi-coherence is a monoidal property of 𝒪ₓ-modules;
• TauCeti.AlgebraicGeometry.isQuasicoherent_unit and TauCeti.AlgebraicGeometry.isQuasicoherent_structureSheaf: the structure sheaf, viewed as a module over itself, is quasi-coherent in monoidal-unit and explicit-unit notation.

@[instance_reducible]

noncomputable instance AlgebraicGeometry.Scheme.Modules.instMonoidalCategory (X : Scheme) : CategoryTheory.MonoidalCategory X.Modules

The monoidal category structure on 𝒪ₓ-modules: the tensor product sheafifies the sectionwise tensor product, and the unit is the structure sheaf.

Equations

• AlgebraicGeometry.Scheme.Modules.instMonoidalCategory X = TauCeti.SheafOfModules.monoidalCategory X.sheaf

@[instance_reducible]

noncomputable instance AlgebraicGeometry.Scheme.Modules.instSymmetricCategory (X : Scheme) : CategoryTheory.SymmetricCategory X.Modules

The symmetric structure on the monoidal category of 𝒪ₓ-modules.

Equations

• AlgebraicGeometry.Scheme.Modules.instSymmetricCategory X = TauCeti.SheafOfModules.symmetricCategory X.sheaf

@[instance_reducible]

noncomputable instance AlgebraicGeometry.Scheme.Modules.instMonoidalClosed (X : Scheme) : CategoryTheory.MonoidalClosed X.Modules

The closed monoidal structure on 𝒪ₓ-modules: tensoring on the left is adjoint to the internal Hom functor.

Equations

• AlgebraicGeometry.Scheme.Modules.instMonoidalClosed X = TauCeti.SheafOfModules.monoidalClosed X.sheaf

instance AlgebraicGeometry.Scheme.Modules.isQuasicoherent_tensorObj (X : Scheme) (M N : X.Modules) [SheafOfModules.IsQuasicoherent M] [SheafOfModules.IsQuasicoherent N] : SheafOfModules.IsQuasicoherent (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)

The tensor product of two quasi-coherent 𝒪ₓ-modules is quasi-coherent.

instance AlgebraicGeometry.Scheme.Modules.isMonoidal_isQuasicoherent (X : Scheme) : (SheafOfModules.isQuasicoherent X.ringCatSheaf).IsMonoidal

Quasi-coherence is a monoidal property of 𝒪ₓ-modules, so quasi-coherent 𝒪ₓ-modules form a monoidal full subcategory of X.Modules.

instance TauCeti.AlgebraicGeometry.isQuasicoherent_unit (X : AlgebraicGeometry.Scheme) : SheafOfModules.IsQuasicoherent (CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules)

The structure sheaf, viewed as a module over itself, is quasicoherent.

instance TauCeti.AlgebraicGeometry.isQuasicoherent_structureSheaf (X : AlgebraicGeometry.Scheme) : (SheafOfModules.unit X.ringCatSheaf).IsQuasicoherent

The explicit structure-sheaf module is quasicoherent. This instance also supports goals that do not use monoidal-unit notation.

def AlgebraicGeometry.Scheme.Modules.sectionsFunctor {X : Scheme} (U : X.Opens) : CategoryTheory.Functor X.Modules (ModuleCat ↑(X.presheaf.obj (Opposite.op U)))

The sections over an open U of 𝒪ₓ-modules, as a functor to Γ(X, U)-modules. It is the evaluation at U of the underlying presheaves of modules, and it is lax braided monoidal: its tensor map Γ(M, U) ⊗[Γ(X, U)] Γ(N, U) ⟶ Γ(M ⊗ N, U) is induced by the unit of sheafification (TauCeti.SheafOfModules.forget_μ). The image of M is definitionally Γ(M, U).

Equations

• AlgebraicGeometry.Scheme.Modules.sectionsFunctor U = (SheafOfModules.forget X.ringCatSheaf).comp (TauCeti.PresheafOfModulesOfCommRing.evaluation (Opposite.op U))

@[instance_reducible]

noncomputable instance AlgebraicGeometry.Scheme.Modules.sectionsFunctorLaxBraided {X : Scheme} (U : X.Opens) : (sectionsFunctor U).LaxBraided

Sections over an open are lax braided monoidal, as the composite of the lax braided inclusion of sheaves of modules into presheaves of modules with the braided evaluation at the open.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.sectionsFunctor_obj {X : Scheme} (U : X.Opens) (M : X.Modules) : (sectionsFunctor U).obj M = M.val.obj (Opposite.op U)

The image of an 𝒪ₓ-module under the sections functor is its module of sections over U.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.sectionsFunctor_map {X : Scheme} (U : X.Opens) {M N : X.Modules} (φ : M ⟶ N) : (sectionsFunctor U).map φ = φ.val.app (Opposite.op U)

The sections functor sends a morphism of 𝒪ₓ-modules to its component over U.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.sectionsFunctor_ε {X : Scheme} (U : X.Opens) : CategoryTheory.Functor.LaxMonoidal.ε (sectionsFunctor U) = CategoryTheory.CategoryStruct.id ↧↑(X.presheaf.obj (Opposite.op U))

The unit comparison of the sections functor is the identity on regular functions.