feat(algebra/category/Module): monoidal_preadditive (#12607)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/category/Module/monoidal.lean

@@ -8,6 +8,7 @@ import category_theory.closed.monoidal
 import algebra.category.Module.basic
 import linear_algebra.tensor_product
 import category_theory.linear.yoneda
+import category_theory.monoidal.preadditive
 
 /-!
 # The symmetric monoidal category structure on R-modules
@@ -16,6 +17,10 @@ Mostly this uses existing machinery in `linear_algebra.tensor_product`.
 We just need to provide a few small missing pieces to build the
 `monoidal_category` instance and then the `symmetric_category` instance.
 
+Note the universe level of the modules must be at least the universe level of the ring,
+so that we have a monoidal unit.
+For now, we simplify by insisting both universe levels are the same.
+
 We then construct the monoidal closed structure on `Module R`.
 
 If you're happy using the bundled `Module R`, it may be possible to mostly
@@ -262,6 +267,12 @@ end monoidal_category
 
 open opposite
 
+instance : monoidal_preadditive (Module.{u} R) :=
+{ tensor_zero' := by { intros, ext, simp, },
+  zero_tensor' := by { intros, ext, simp, },
+  tensor_add' := by { intros, ext, simp [tensor_product.tmul_add], },
+  add_tensor' := by { intros, ext, simp [tensor_product.add_tmul], }, }
+
 /--
 Auxiliary definition for the `monoidal_closed` instance on `Module R`.
 (This is only a separate definition in order to speed up typechecking. )

src/category_theory/monoidal/preadditive.lean

@@ -23,7 +23,7 @@ open category_theory.monoidal_category
 variables (C : Type*) [category C] [preadditive C] [monoidal_category C]
 
 /--
-A category is `monoidal_preadditive` if tensoring is linear in both factors.
+A category is `monoidal_preadditive` if tensoring is additive in both factors.
 
 Note we don't `extend preadditive C` here, as `abelian C` already extends it,
 and we'll need to have both typeclasses sometimes.