Reid Barton (Nov 14 2018 at 22:50):
Has anyone made an attempt at defining the category of R-modules, now that the module refactor has landed?
Johan Commelin (Nov 15 2018 at 05:28):
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.
Last updated: May 14 2021 at 20:13 UTC