Module structures on groups over semirings

Stream: mathlib4

[Oliver Nash]

I recently became aware that in some parts of the library we have lemmas like docs#Submodule.comap_map_eq which cater for a setup such as:

variable (R M : Type*) [Semiring R] [AddCommGroup M] [Module R M]

Is this something we want to support?

I vote no unless someone has a good example. For one thing a term of type Submodule R M under these hypotheses does not carry AddCommGroup.

[Eric Wieser]

I think this setup is what is used for positive cones?

[Yaël Dillies]

Yes, the point is to restrict to nonnegative scalars, in which case you get a subsemiring of the original ring.

[Oliver Nash]

Thanks, I get it now!

[Eric Wieser]

There are still probably plenty of cases where this generality is nonsense though

[Eric Rodriguez]

Regardless of the generality being usually nonsense in most of those cases, it's nice to have lemmas that are as general as possible in that sort of direction. Syntactic generality usually frees you up a lot. The one thing that is worth taking care about is that we avoid them when there's a "seesaw" effect, i.e. Ring+ACM vs Semiring+ACG