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 instCommRingαRingObjOppositeRingCatCompCommRingCatForget₂ {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)

Equations

• instCommRingαRingObjOppositeRingCatCompCommRingCatForget₂ X = inferInstanceAs (CommRing ↑(R.obj X))

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

Auxiliary definition for tensorObj.

Equations

• PresheafOfModules.Monoidal.tensorObjMap M₁ M₂ f = ModuleCat.MonoidalCategory.tensorLift (fun (m₁ : ↑(M₁.obj X)) (m₂ : ↑(M₂.obj X)) => (M₁.map f) m₁ ⊗ₜ[↑(R.obj Y)] (M₂.map f) m₂) ⋯ ⋯ ⋯ ⋯

@[simp]

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

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

The tensor product of two presheaves of modules.

Equations

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

@[simp]

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

@[simp]

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

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

The tensor product of two morphisms of presheaves of modules.

Equations

• PresheafOfModules.Monoidal.tensorHom f g = { app := fun (X : Cᵒᵖ) => CategoryTheory.MonoidalCategory.tensorHom (f.app X) (g.app X), naturality := ⋯ }

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)))

Equations

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

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)))

Equations

• PresheafOfModules.monoidalCategory = CategoryTheory.MonoidalCategory.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯