coe to monoid_algebra

Stream: Is there code for X?

[Antoine Labelle]

Hi,
I'm working with monoid_algebra and I realised that there is no coercion from G or k to monoid_algebra k G. Such coercions seems like a pretty natural useful thing to have if we want to define explicit elements of the monoid_algebra. Is there a reason they are not there or should I try adding them?

[Adam Topaz]

A monoid algebra should certainly have an algebra instance, so you should be able to use smul with elements of k. Maybe we should have notation for the canonical map from G? The usual math notation is [g]. Perhaps we can mimic that somehow

[Antoine Labelle]

Indeed I mainly want the coercion from G

[Adam Topaz]

@Eric Wieser would probably be able to tell us if this is a good idea

[Eric Wieser]

Having both is a bad idea because then things go wrong become ambiguous when k = G, and notation shouldn't be ambiguous

[Eric Wieser]

I assume you're aware of docs#monoid_algebra.of and just don't like writing of k G g?

[Adam Topaz]

Even worse, if G just so happens to have an action by k, you will need to use type ascription which will be more verbose than of. I think introducing some notation approximating [g] for of k G g, perhaps in a locale, is the right solution

[Eric Wieser]

We could drop the G since it's implied by g to make it slightly shorter

[Antoine Labelle]

Yeah, I just realized the existence of of after asking the question. That does what I want indeed even though it's a little bit more lengthy than just a coercion, but it's not a big deal. Adam's solution seems interesting though.