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 PresheafOfModulesOfCommRing R. 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.

noncomputable def PresheafOfModulesOfCommRing.Monoidal.tensorObjMap {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M₁ M₂ : PresheafOfModulesOfCommRing R) {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.

Equations

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

noncomputable def PresheafOfModulesOfCommRing.Monoidal.tensorObj {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M₁ M₂ : PresheafOfModulesOfCommRing R) : PresheafOfModulesOfCommRing R

The tensor product of two presheaves of modules.

Equations

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

@[simp]

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

@[simp]

theorem PresheafOfModulesOfCommRing.Monoidal.tensorObj_map_tmul {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} {M₁ M₂ : PresheafOfModulesOfCommRing R} {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 PresheafOfModulesOfCommRing.Monoidal.tensorHom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} {M₁ M₂ M₃ M₄ : PresheafOfModulesOfCommRing R} (f : M₁ ⟶ M₂) (g : M₃ ⟶ M₄) : tensorObj M₁ M₃ ⟶ tensorObj M₂ M₄

The tensor product of two morphisms of presheaves of modules.

Equations

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

@[simp]

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

@[instance_reducible]

noncomputable instance PresheafOfModulesOfCommRing.monoidalCategoryStruct {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} : CategoryTheory.MonoidalCategoryStruct (PresheafOfModulesOfCommRing R)

Equations

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

@[instance_reducible]

noncomputable instance PresheafOfModulesOfCommRing.monoidalCategory {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} : CategoryTheory.MonoidalCategory (PresheafOfModulesOfCommRing R)

Equations

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

@[instance_reducible]

noncomputable instance PresheafOfModulesOfCommRing.symmetricCategory {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} : CategoryTheory.SymmetricCategory (PresheafOfModulesOfCommRing R)

Equations

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

theorem PresheafOfModulesOfCommRing.tensorObj_obj {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M₁ M₂ : PresheafOfModulesOfCommRing R) (X : Cᵒᵖ) : (CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂).obj X = CategoryTheory.MonoidalCategoryStruct.tensorObj (M₁.obj X) (M₂.obj X)

@[simp]

theorem PresheafOfModulesOfCommRing.whiskerLeft_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M₁ : PresheafOfModulesOfCommRing R) {M₂ M₃ : PresheafOfModulesOfCommRing R} (f : M₂ ⟶ M₃) (X : Cᵒᵖ) : PresheafOfModules.Hom.app' (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M₁ f) X = CategoryTheory.MonoidalCategoryStruct.whiskerLeft (M₁.obj X) (PresheafOfModules.Hom.app' f X)

@[simp]

theorem PresheafOfModulesOfCommRing.whiskerRight_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} {M₁ M₂ : PresheafOfModulesOfCommRing R} (f : M₁ ⟶ M₂) (M₃ : PresheafOfModulesOfCommRing R) (X : Cᵒᵖ) : PresheafOfModules.Hom.app' (CategoryTheory.MonoidalCategoryStruct.whiskerRight f M₃) X = CategoryTheory.MonoidalCategoryStruct.whiskerRight (PresheafOfModules.Hom.app' f X) (M₃.obj X)

@[simp]

theorem PresheafOfModulesOfCommRing.tensorHom_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} {M₁ M₂ M₃ M₄ : PresheafOfModulesOfCommRing R} (f : M₁ ⟶ M₂) (g : M₃ ⟶ M₄) (X : Cᵒᵖ) : PresheafOfModules.Hom.app' (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) X = CategoryTheory.MonoidalCategoryStruct.tensorHom (PresheafOfModules.Hom.app' f X) (PresheafOfModules.Hom.app' g X)

@[simp]

theorem PresheafOfModulesOfCommRing.leftUnitor_hom_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M₁ : PresheafOfModulesOfCommRing R) (X : Cᵒᵖ) : PresheafOfModules.Hom.app' (CategoryTheory.MonoidalCategoryStruct.leftUnitor M₁).hom X = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (M₁.obj X)).hom

@[simp]

theorem PresheafOfModulesOfCommRing.leftUnitor_inv_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M₁ : PresheafOfModulesOfCommRing R) (X : Cᵒᵖ) : PresheafOfModules.Hom.app' (CategoryTheory.MonoidalCategoryStruct.leftUnitor M₁).inv X = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (M₁.obj X)).inv

@[simp]

theorem PresheafOfModulesOfCommRing.rightUnitor_hom_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M₁ : PresheafOfModulesOfCommRing R) (X : Cᵒᵖ) : PresheafOfModules.Hom.app' (CategoryTheory.MonoidalCategoryStruct.rightUnitor M₁).hom X = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (M₁.obj X)).hom

@[simp]

theorem PresheafOfModulesOfCommRing.rightUnitor_inv_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M₁ : PresheafOfModulesOfCommRing R) (X : Cᵒᵖ) : PresheafOfModules.Hom.app' (CategoryTheory.MonoidalCategoryStruct.rightUnitor M₁).inv X = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (M₁.obj X)).inv

@[simp]

theorem PresheafOfModulesOfCommRing.associator_hom_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M₁ M₂ M₃ : PresheafOfModulesOfCommRing R) (X : Cᵒᵖ) : PresheafOfModules.Hom.app' (CategoryTheory.MonoidalCategoryStruct.associator M₁ M₂ M₃).hom X = (CategoryTheory.MonoidalCategoryStruct.associator (M₁.obj X) (M₂.obj X) (M₃.obj X)).hom

@[simp]

theorem PresheafOfModulesOfCommRing.associator_inv_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M₁ M₂ M₃ : PresheafOfModulesOfCommRing R) (X : Cᵒᵖ) : PresheafOfModules.Hom.app' (CategoryTheory.MonoidalCategoryStruct.associator M₁ M₂ M₃).inv X = (CategoryTheory.MonoidalCategoryStruct.associator (M₁.obj X) (M₂.obj X) (M₃.obj X)).inv

@[simp]

theorem PresheafOfModulesOfCommRing.braiding_hom_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M₁ M₂ : PresheafOfModulesOfCommRing R) (X : Cᵒᵖ) : PresheafOfModules.Hom.app' (β_ M₁ M₂).hom X = (β_ (M₁.obj X) (M₂.obj X)).hom

@[simp]

theorem PresheafOfModulesOfCommRing.braiding_inv_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M₁ M₂ : PresheafOfModulesOfCommRing R) (X : Cᵒᵖ) : PresheafOfModules.Hom.app' (β_ M₁ M₂).inv X = (β_ (M₁.obj X) (M₂.obj X)).inv

instance PresheafOfModulesOfCommRing.instPreservesColimitsOfSizeTensorLeft {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (F : PresheafOfModulesOfCommRing R) : CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u_1, max u u_1, max (max (u + 1) u_1) v_1, max (max (u + 1) u_1) v_1} (CategoryTheory.MonoidalCategory.tensorLeft F)

instance PresheafOfModulesOfCommRing.instPreservesColimitsOfSizeTensorRight {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (F : PresheafOfModulesOfCommRing R) : CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u_1, max u u_1, max (max (u + 1) u_1) v_1, max (max (u + 1) u_1) v_1} (CategoryTheory.MonoidalCategory.tensorRight F)