Feature request: MulAction for Module (MonoidAlgebra k M) V

Stream: mathlib4

[Mitchell Lee]

Let M be a monoid and let V be an M-module (that is, the class Module (MonoidAlgebra k M) V is instantiated).

Currently, it does not seem that I can use • to multiply a term m : M by a term v : V, unless I separately instantiate MulAction M V. Would it be possible to add the ability to do this?

[Junyan Xu]

I would just open MonoidAlgebra and write of g • m. If you want the MulAction M V temporarily you might make a local instance with docs#MonoidAlgebra.of and docs#MulAction.compHom. If you make it a global instance, it might not be defeq with an existing MulAction M V instance, but maybe this is less common than an existing Module k V instance ... Note that in the file containing docs#LinearMap.conjugate etc. the author opt to assume both Module k V and Module (MonoidAlgebra k M) V plus IsScalarTower, while docs#groupCohomology is using docs#Rep rather than Module.

[Mitchell Lee]

Thank you for the response. I see the potential issues with making a global instance here. I think I'll just use a Representation instead of a Module instance for my particular use case.