The tensor product of quasi-coherent sheaves is quasi-coherent

Let R be a sheaf of commutative rings on a small site with pullbacks. If M and N are quasi-coherent sheaves of R-modules, then so is M ⊗ N: on a common refinement of covers on which M and N have presentations, the restriction of M ⊗ N is the tensor product of the restrictions of M and N (SheafOfModules.overTensorIso), which is presented by the tensor product of their presentations (SheafOfModules.Presentation.tensor). As the unit R is free on one generator, quasi-coherence is a monoidal property of sheaves of modules when the site also has binary products, and quasi-coherent sheaves of modules then form a monoidal full subcategory.

The same construction applied to finite presentations gives finite presentations, so finite presentation is a monoidal property as well when the site has binary products. Applied to presentations whose generating morphisms are isomorphisms, it gives presentations of the same kind; this is the local input for the tensor product of locally free sheaves.

Main declarations

• SheafOfModules.QuasicoherentData.tensor: quasi-coherent data for M ⊗ N built from quasi-coherent data for M and for N;
• TauCeti.SheafOfModules.isQuasicoherent_tensorObj: M ⊗ N is quasi-coherent when M and N are;
• TauCeti.SheafOfModules.isMonoidal_isQuasicoherent: quasi-coherence is an ObjectProperty.IsMonoidal;
• SheafOfModules.QuasicoherentData.isIso_tensor_presentation_generators_π: the tensor data presents M ⊗ N by free sheaves where the data for M and N do;
• TauCeti.SheafOfModules.isFinitePresentation_tensorObj and TauCeti.SheafOfModules.isMonoidal_isFinitePresentation: finite presentation is an ObjectProperty.IsMonoidal.

References

• The Stacks Project, Tag 01CE

noncomputable def SheafOfModules.QuasicoherentData.tensor {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} {M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (qM : M.QuasicoherentData) (qN : N.QuasicoherentData) : (CategoryTheory.MonoidalCategoryStruct.tensorObj M N).QuasicoherentData

Quasi-coherent data for M ⊗ N from quasi-coherent data for M and for N. Its cover is the common refinement of the two covers, and over each of its members the presentation is the tensor product of the restricted presentations of M and N.

Equations

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

@[simp]

theorem SheafOfModules.QuasicoherentData.tensor_X {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} {M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (qM : M.QuasicoherentData) (qN : N.QuasicoherentData) (a✝ : (⋯.commonRefinement ⋯).I) : (qM.tensor qN).X a✝ = (⋯.commonRefinement ⋯).X a✝

@[simp]

theorem SheafOfModules.QuasicoherentData.tensor_presentation {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} {M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (qM : M.QuasicoherentData) (qN : N.QuasicoherentData) (i : (⋯.commonRefinement ⋯).I) : (qM.tensor qN).presentation i = Presentation.ofIsIso (M.overTensorIso N ((⋯.commonRefinement ⋯).X i)).inv (((qM.ofRefinement (⋯.commonRefinement ⋯).X ⋯ (⋯.commonRefinement ⋯).leftIndex (⋯.commonRefinement ⋯).left).presentation i).tensor ((qN.ofRefinement (⋯.commonRefinement ⋯).X ⋯ (⋯.commonRefinement ⋯).rightIndex (⋯.commonRefinement ⋯).right).presentation i))

@[simp]

theorem SheafOfModules.QuasicoherentData.tensor_I {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} {M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (qM : M.QuasicoherentData) (qN : N.QuasicoherentData) : (qM.tensor qN).I = (⋯.commonRefinement ⋯).I

instance TauCeti.SheafOfModules.isQuasicoherent_tensorObj {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} {M N : SheafOfModules (ringCatSheaf R)} [M.IsQuasicoherent] [N.IsQuasicoherent] : (CategoryTheory.MonoidalCategoryStruct.tensorObj M N).IsQuasicoherent

The tensor product of two quasi-coherent sheaves of modules is quasi-coherent.

instance TauCeti.SheafOfModules.isMonoidal_isQuasicoherent {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} [CategoryTheory.Limits.HasBinaryProducts C] : (SheafOfModules.isQuasicoherent (ringCatSheaf R)).IsMonoidal

Quasi-coherence of sheaves of modules is a monoidal property: the unit is quasi-coherent and quasi-coherent sheaves are closed under tensor products. Hence quasi-coherent sheaves of modules form a monoidal full subcategory (ObjectProperty.fullMonoidalSubcategory).

theorem SheafOfModules.QuasicoherentData.isIso_tensor_presentation_generators_π {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} {M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (qM : M.QuasicoherentData) (qN : N.QuasicoherentData) (hM : ∀ (i : qM.I), CategoryTheory.IsIso (qM.presentation i).generators.π) (hN : ∀ (i : qN.I), CategoryTheory.IsIso (qN.presentation i).generators.π) (i : (qM.tensor qN).I) : CategoryTheory.IsIso ((qM.tensor qN).presentation i).generators.π

If quasi-coherent data for M and for N present them locally by free sheaves, that is, all their generating morphisms are isomorphisms, then so does their tensor product data for M ⊗ N.

instance TauCeti.SheafOfModules.instIsFinitePresentationTensor {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} {M N : SheafOfModules (ringCatSheaf R)} (qM : M.QuasicoherentData) (qN : N.QuasicoherentData) [qM.IsFinitePresentation] [qN.IsFinitePresentation] : (qM.tensor qN).IsFinitePresentation

The tensor product of finite quasi-coherent data is finite.

instance TauCeti.SheafOfModules.isFinitePresentation_tensorObj {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} {M N : SheafOfModules (ringCatSheaf R)} [M.IsFinitePresentation] [N.IsFinitePresentation] : (CategoryTheory.MonoidalCategoryStruct.tensorObj M N).IsFinitePresentation

The tensor product of two finitely presented sheaves of modules is finitely presented.

instance TauCeti.SheafOfModules.isMonoidal_isFinitePresentation {C : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J CommRingCat} [CategoryTheory.Limits.HasBinaryProducts C] : (SheafOfModules.isFinitePresentation (ringCatSheaf R)).IsMonoidal

Finite presentation of sheaves of modules is a monoidal property: the unit is finitely presented and finitely presented sheaves are closed under tensor products.