The monoidal category structure on presheaves of modules

Given a presheaf of commutative rings R : Cᵒᵖ ⥤ CommRingCat, we construct the monoidal category structure on the category of presheaves of modules PresheafOfModules (R ⋙ forget₂ _ _). The tensor product M₁ ⊗ M₂ is defined as the presheaf of modules which sends X : Cᵒᵖ to M₁.obj X ⊗ M₂.obj X.

Notes

This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

instance instCommRingCarrierObjOppositeRingCatCompCommRingCatForget₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (X : Cᵒᵖ) : CommRing ↑((R.comp (CategoryTheory.forget₂ CommRingCat RingCat)).obj X)

noncomputable def PresheafOfModules.Monoidal.tensorObjMap {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M₁ M₂ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) {X Y : Cᵒᵖ} (f : X ⟶ Y) : CategoryTheory.MonoidalCategoryStruct.tensorObj (M₁.obj X) (M₂.obj X) ⟶ (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (M₁.obj Y) (M₂.obj Y))

Auxiliary definition for tensorObj.

noncomputable def PresheafOfModules.Monoidal.tensorObj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M₁ M₂ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))

The tensor product of two presheaves of modules.

@[simp]

theorem PresheafOfModules.Monoidal.tensorObj_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M₁ M₂ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (X : Cᵒᵖ) : (tensorObj M₁ M₂).obj X = CategoryTheory.MonoidalCategoryStruct.tensorObj (M₁.obj X) (M₂.obj X)

@[simp]

theorem PresheafOfModules.Monoidal.tensorObj_map_tmul {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} {M₁ M₂ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {X Y : Cᵒᵖ} (f : X ⟶ Y) (m₁ : ↑(M₁.obj X)) (m₂ : ↑(M₂.obj X)) : (ModuleCat.Hom.hom ((tensorObj M₁ M₂).map f)) (m₁ ⊗ₜ[↑(R.obj X)] m₂) = (CategoryTheory.ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (CategoryTheory.ConcreteCategory.hom (M₂.map f)) m₂

noncomputable def PresheafOfModules.Monoidal.tensorHom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} {M₁ M₂ M₃ M₄ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (f : M₁ ⟶ M₂) (g : M₃ ⟶ M₄) : tensorObj M₁ M₃ ⟶ tensorObj M₂ M₄

The tensor product of two morphisms of presheaves of modules.

@[simp]

theorem PresheafOfModules.Monoidal.tensorHom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} {M₁ M₂ M₃ M₄ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (f : M₁ ⟶ M₂) (g : M₃ ⟶ M₄) (X : Cᵒᵖ) : (tensorHom f g).app X = CategoryTheory.MonoidalCategoryStruct.tensorHom (f.app X) (g.app X)

noncomputable instance PresheafOfModules.monoidalCategoryStruct {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} : CategoryTheory.MonoidalCategoryStruct (PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat)))

noncomputable instance PresheafOfModules.monoidalCategory {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} : CategoryTheory.MonoidalCategory (PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat)))