The monoidal category structure on R-modules #
Mostly this uses existing machinery in
We just need to provide a few small missing pieces to build the
SymmetricCategory instance is in
to reduce imports.
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 construct the monoidal closed structure on
Module R in
If you're happy using the bundled
Module R, it may be possible to mostly
use this as an interface and not need to interact much with the implementation details.
(implementation) tensor product of morphisms R-modules
(implementation) the associator for R-modules
We give them some help by expressing the lemmas first non-categorically, then using
convert _aux using 1 to have the elaborator work as little as possible.