Tensor products of sheaves of modules

Given a site (C, J) carrying a sheaf of commutative rings R, and two sheaves of R-modules M, N, we construct their tensor product M ⊗ N as a sheaf of modules: sectionwise one tensors the modules of sections over the rings of sections, and the resulting presheaf of modules is sheafified. Mathlib already provides the sectionwise symmetric monoidal structure on presheaves of modules over a presheaf of commutative rings (PresheafOfModules.Monoidal, contributed at the AIM workshop "Formalising algebraic geometry" of June 24–28, 2024, https://aimath.org/pastworkshops/alggeominlean.html); here that structure is transported to presheaves of modules over the sheaf of rings underlying R and combined with Mathlib's sheafification adjunction for presheaves of modules (PresheafOfModules.sheafification). Nothing here is specific to schemes.

Main declarations

• SheafOfModules.tensorProduct R M N is the sheafified tensor product of two sheaves of R-modules;
• SheafOfModules.tensorProductIso R M N is its defining identification with the sheafification of the sectionwise tensor product of the underlying presheaves of modules;
• SheafOfModules.tensorProductCongrLeft/right transport an isomorphism of one argument through the tensor product;
• SheafOfModules.tensorProductUnitIsoLeft/right identify R ⊗ M and M ⊗ R with M;
• SheafOfModules.tensorProductComm provides symmetry.

The site-level construction remains available on a scheme as SheafOfModules.tensorProduct X.sheaf; the canonical tensor notation M ⊗ N and symmetric monoidal structure on X.Modules are in TauCeti/AlgebraicGeometry/Modules/TensorProduct.lean.

@[instance_reducible]

noncomputable instance TauCeti.SheafOfModules.instMonoidalPresheafOfModulesRingCatSheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] (R : CategoryTheory.Sheaf J CommRingCat) : CategoryTheory.MonoidalCategory (PresheafOfModules (ringCatSheaf R).obj)

The monoidal category structure on presheaves of modules over the sheaf of rings underlying a sheaf of commutative rings, obtained from Mathlib's monoidal structure on presheaves of modules over a presheaf of commutative rings.

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.SheafOfModules.instSymmetricPresheafOfModulesRingCatSheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] (R : CategoryTheory.Sheaf J CommRingCat) : CategoryTheory.SymmetricCategory (PresheafOfModules (ringCatSheaf R).obj)

The symmetric category structure on presheaves of modules over the sheaf of rings underlying a sheaf of commutative rings, obtained from Mathlib's symmetric structure on presheaves of modules over a presheaf of commutative rings.

Equations

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

noncomputable def TauCeti.SheafOfModules.tensorProductRightFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J CommRingCat) (N : SheafOfModules (ringCatSheaf R)) : CategoryTheory.Functor (SheafOfModules (ringCatSheaf R)) (SheafOfModules (ringCatSheaf R))

The functor of sheafified tensor products with a fixed second argument: it sends M to M ⊗ N.

Equations

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

noncomputable def TauCeti.SheafOfModules.tensorProductLeftFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J CommRingCat) (M : SheafOfModules (ringCatSheaf R)) : CategoryTheory.Functor (SheafOfModules (ringCatSheaf R)) (SheafOfModules (ringCatSheaf R))

The functor of sheafified tensor products with a fixed first argument: it sends N to M ⊗ N.

Equations

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

noncomputable def TauCeti.SheafOfModules.tensorProduct {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J CommRingCat) (M N : SheafOfModules (ringCatSheaf R)) : SheafOfModules (ringCatSheaf R)

The tensor product of two sheaves of R-modules: the sectionwise tensor product of the underlying presheaves of modules, sheafified.

Equations

• TauCeti.SheafOfModules.tensorProduct R M N = (TauCeti.SheafOfModules.tensorProductRightFunctor R N).obj M

@[simp]

theorem TauCeti.SheafOfModules.tensorProduct_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J CommRingCat) (M N : SheafOfModules (ringCatSheaf R)) : (tensorProduct R M N).val = ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.val N.val)).val

noncomputable def TauCeti.SheafOfModules.tensorProductIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J CommRingCat) (M N : SheafOfModules (ringCatSheaf R)) : tensorProduct R M N ≅ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.val N.val)

The defining identification of the tensor product with the sheafification of the sectionwise tensor product of the underlying presheaves of modules.

Equations

• TauCeti.SheafOfModules.tensorProductIso R M N = CategoryTheory.Iso.refl (TauCeti.SheafOfModules.tensorProduct R M N)

noncomputable def TauCeti.SheafOfModules.tensorProductCongrLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J CommRingCat) {M M' N : SheafOfModules (ringCatSheaf R)} (e : M ≅ M') : tensorProduct R M N ≅ tensorProduct R M' N

An isomorphism of the first argument transports through the tensor product.

Equations

• TauCeti.SheafOfModules.tensorProductCongrLeft R e = (TauCeti.SheafOfModules.tensorProductRightFunctor R N).mapIso e

noncomputable def TauCeti.SheafOfModules.tensorProductCongrRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J CommRingCat) {M N N' : SheafOfModules (ringCatSheaf R)} (e : N ≅ N') : tensorProduct R M N ≅ tensorProduct R M N'

An isomorphism of the second argument transports through the tensor product.

Equations

• TauCeti.SheafOfModules.tensorProductCongrRight R e = (TauCeti.SheafOfModules.tensorProductLeftFunctor R M).mapIso e

noncomputable def TauCeti.SheafOfModules.tensorProductUnitIsoLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J CommRingCat) (M : SheafOfModules (ringCatSheaf R)) : tensorProduct R (SheafOfModules.unit (ringCatSheaf R)) M ≅ M

Tensoring with the sheaf of rings itself (on the left) does nothing.

Equations

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

noncomputable def TauCeti.SheafOfModules.tensorProductUnitIsoRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J CommRingCat) (M : SheafOfModules (ringCatSheaf R)) : tensorProduct R M (SheafOfModules.unit (ringCatSheaf R)) ≅ M

Tensoring with the sheaf of rings itself (on the right) does nothing.

Equations

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

noncomputable def TauCeti.SheafOfModules.tensorProductComm {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J CommRingCat) (M N : SheafOfModules (ringCatSheaf R)) : tensorProduct R M N ≅ tensorProduct R N M

Symmetry of the tensor product of sheaves of R-modules.

Equations

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