ModuleCat over Semiring?

Stream: mathlib4

[Kenny Lau]

Why is ModuleCat defined over a Ring instead of Semiring?

[Junyan Xu]

Things weren't set up in great generality in the old days (as you probably know), and many results were only recently generalized by myself from Ring to Semiring. It's certainly necessary to generalize ModuleCat if we want to study Morita theory over semirings (see also). I think we are also lacking APIs for AddCons preserved by SMul and quotients by them and finite presentation over semirings, and also there's a different notion of flatness over (Comm)Semirings.