feat(data/monoid_algebra): k →+* monoid_algebra k G

[semorrison]

The ring homomorphism k →+* monoid_algebra k G, given by including in as functions supported at the multiplicative identity of G, and a few associated lemmas.

[abentkamp]

Looks nice!

Can't we use to_additive to prove the lemmas single_one.central and module_smul_eq for the additive counterpart?

I think single.add_monoid_hom already exists as lapply in linear_algebra/finsupp.lean. Maybe it's not ideal that finsupp is split into several files. I think this happened because we did not want dependencies of /data on /linear_algebra. Is that still something you want to keep up?

[semorrison]

Thanks! I hadn't known about lapply. I do think we should avoid piling too much maths into the data directory. In fact, now that we're building polynomials on top of monoid algebras, perhaps we should even be moving polynomials out entirely.

Let me have a think about how to connect up with lapply.

[semorrison]

Oh, no, they are quite different. lapply is the evaluation-at-a-point morphism, while single.add_monoid_hom is the include-as-functions-supported-at-a-point morphism,

[abentkamp]

Sorry, I meant single.linear_map and lapply are the same.

[semorrison]

And I'm pretty sure that we're well beyond the reach of to_additive by now. In [add_]monoid_algebra k G, the fact that k is usually a ring means that to_additive is hopelessly confused. There's no way to tell it that it's only the multiplications internal to G that we want to translate into additions: it gets distracted by the multiplications in k as well.

[abentkamp]

And I'm pretty sure that we're well beyond the reach of to_additive by now. In [add_]monoid_algebra k G, the fact that k is usually a ring means that to_additive is hopelessly confused. There's no way to tell it that it's only the multiplications internal to G that we want to translate into additions: it gets distracted by the multiplications in k as well.

Ok, I see.

[semorrison]

No, they're still not:

single.linear_map [ring γ] [add_comm_group β] [module γ β] (a : α) : β →ₗ[γ] (α →₀ β)

while

lapply [ring R] [add_comm_group M] [module R M] (a : α) : (α →₀ M) →ₗ[R] M

[abentkamp]

Oh no, I don't know what's wrong with me today :D. I meant lsingle and single.linear_map. Sorry about this!

[semorrison]

No worries. I didn't know the contents of that file at all, so this is very helpful! :-)

[semorrison]

It looks like an easy solution is to delete my finsupp.single.linear_map. I've added a pointer in the doc string of finsupp.single.add_monoid_hom to finsupp.lsingle.

If anyone wants to hold forth on naming conventions for these "functions bundled as an X" definitions, I'm happy to listen.

[abentkamp]

Concerning the comments in your proofs, I am afraid that I am not good enough at golfing to help you out there.

For me, it looks ready to merge now, but I do not have the power to approve :-).

[semorrison]

All good, someone will come by. :-) It's super helpful to have reviews from non-maintainers, too.

[semorrison]

It looks like this is largely duplicative with #2366. I'll probably close this in a moment.