Smul actions on submodules

Stream: mathlib4

[Brendan Seamas Murphy]

In mathlib we currently have the instances

Submodule.hasSMul' {R M} [CommSemiring R] [AddCommMonoid M] [Module R M] :
  SMul (Ideal R) (Submodule R M)

Submodule.pointwiseDistribMulAction {α R M} [Semiring R] [AddCommMonoid M]
  [Module R M] [Monoid α] [DistribMulAction α M] [SMulCommClass α R M] :
  DistribMulAction α (Submodule R M)

Submodule.pointwiseSetSMul {R M} [Semiring R] {S} [Monoid S] [AddCommMonoid M]
  [Module R M] [DistribMulAction S M] : SMul (Set S) (Submodule R M)

This is kind of a mess. In particular it's seems very strange that Submodule.hasSMul' requires that R is commutative when Ideal R has a coercion to Set R and Submodule.pointwiseSetSMul has no commutativity assumption! This requirement exists because the action of ideals on submodules is defined by I • N = Submodule.map₂ (LinearMap.lsmul R M) I N whenmap₂ and lsmul both depend on commutativity (because bilinear maps work a lot better over commutative rings). In the case of a commutative ring the three actions SMul R (Submodule R M), SMul (Set R) (Submodule R M), and SMul (Ideal R) (Submodule R M) are all roughly the same thing: acting by an ideal is the same as acting by its underlying set, acting by a set is the same as acting by its span and is the same as the supremum of the actions of each element, and acting by an element is the same as acting by the (span of the) singleton set containing that element. This leads to a lot of code duplication. At the moment it's hard to tell which lemmas apply to which action by their name (e.g. why is map_smul'' about ideals acting and not sets?) and the APIs for each action aren't equally mature.

I wanted to add a new smul action for lists of elements, because we write e.g. rM a lot when doing commutative algebra for a sequence of elements r, but I'm worried that doing so right now would just make things messier. It would be really great if we could define all these actions as a special case of one thing, but I don't know that that's possible. At least the ideal and set case could be unified, and it would be nice if the ring element case could be handled similarly (i.e. we always coerce to a set and go through that) but this last action is a special case of Submodule.pointwiseDistribMulAction, which in full generality can't be defined in terms of a coercion to Set R (although I guess it does still have a coercion to Set (Module.End R M) and this does fit into Submodule.pointwiseSetSMul ?).

Does anyone have thoughts on how these actions could be unified/simplified?

[Eric Wieser]

My take on this is that all the actions that derive SMul (F R) (G M) from SMul R M are in some sense evil, as they are incompatible with the actions that derive SMul (F R) M from SMul R M (and often even incompatible with themselves); and so really only the second instance is kosher here, and the other two are begrudging permitted in mathlib out of pragmatism.

[Eric Wieser]

Can you be a little clearer about exactly what instance you want to define? Is it SMul (List S) (Submodule R M)?

[Brendan Seamas Murphy]

Yeah, that's what I had in mind

[Brendan Seamas Murphy]

Er, I was even just thinking SMul (List R) (Submodule R M) (but it might as well be in the generality you said)