English
There is a monoidal category structure on PresheafOfModules(R) given by tensorObj and tensorHom with unit given by PresheafOfModules.unit.
Русский
Существует моноидальная структура на PresheafOfModules(R) с единицей и тензорным произведением.
LaTeX
$$$\\text{Monoidal structure: }(\\mathrm{tensorObj}, \\mathrm{tensorHom}, \\mathrm{unit}, \\alpha, \\lambda, \\rho).$$$
Lean4
noncomputable instance monoidalCategory : MonoidalCategory (PresheafOfModules.{u} (R ⋙ forget₂ _ _))
where
tensorHom_def _ _ := by ext1; apply tensorHom_def
id_tensorHom_id _ _ := by ext1; apply id_tensorHom_id
tensorHom_comp_tensorHom _ _ _ _ := by ext1; apply tensorHom_comp_tensorHom
whiskerLeft_id M₁
M₂ := by
ext1 X
apply MonoidalCategory.whiskerLeft_id (C := ModuleCat (R.obj X))
id_whiskerRight _
_ := by
ext1 X
apply MonoidalCategory.id_whiskerRight (C := ModuleCat (R.obj X))
associator_naturality _ _ _ := by ext1; apply associator_naturality
leftUnitor_naturality _ := by ext1; apply leftUnitor_naturality
rightUnitor_naturality _ := by ext1; apply rightUnitor_naturality
pentagon _ _ _ _ := by ext1; apply pentagon
triangle _ _ := by ext1; apply triangle
