R-Mod

Stream: maths

[Reid Barton]

Has anyone made an attempt at defining the category of R-modules, now that the module refactor has landed?

[Johan Commelin]

No, but I think we should. And then we should define a monoidal structure on it (maybe on a branch of @Michael Jendrusch's repo). I think that would be a very good test case for the new modules, the tensor product, and monoidal categories.