[Merged by Bors] - feat(data/monoid_algebra): add missing has_coe_to_fun

[eric-wieser]

Also does the same for the additive version semimodule k (add_monoid_algebra k G).

---

has_coe_to_fun discussed at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Difficultly.20applying.20.60monoid_algebra.60/near/211594391

[gebner]

There is still a lot of lemma statements that break when removing the local attribute [reducible] monoid_algebra. Not sure if that should be fixed.

[eric-wieser]

Not sure if that should be fixed.

I'd rather not fix that in this PR, but you're probably right that it likely leads to lots of unhelpful lemmas.

[semorrison]

I'm not certain that has_coe_to_fun is a good idea. We very specifically do not copy over the has_coe_to_fun instance when we introduce polynomials, and instead introduce the coeff API.

I'm really not sure --- but would it be better to introduce coeff at this level instead?

[eric-wieser]

There are lemmas in this file like https://leanprover-community.github.io/mathlib_docs/find/monoid_algebra.mul_apply which are only useful if a has_coe_to_fun instance exists.

For #4321, I want a has_coe_to_fun so I can write grades x i to get the ith grade of x. I could instead declare a type alias there. Which approach makes more sense to you?

[eric-wieser]

I've moved all the algebra parts of this PR to a new PR, to make this one as simple as possible.

[jcommelin]

For #4321, I want a has_coe_to_fun so I can write grades x i to get the ith grade of x. I could instead declare a type alias there. Which approach makes more sense to you?

@eric-wieser Would that become much harder with coeff?

For polynomial I definitely wouldn't want the has_coe_to_fun. But for monoid_algebra I'm not so sure... maybe it can work. Still, I'm inclined to say that we shouldn't abuse that class, and only use if for things that we really think of as functions.

What ever option we choose, it would be good to have simp-lemmas that state how coe/coeff interacts with 0/1/+/etc.

[eric-wieser]

@eric-wieser Would that become much harder with coeff?

No, what I'd probably do is add a grade_result := add_monoid_algebra alias in that file and define has_coe_to_fun on that.

If we don't want has_coe_to_fun in this PR, then is

mathlib/src/algebra/monoid_algebra.lean

Lines 76 to 81 in 946ab02

	lemma mul_apply (f g : monoid_algebra k G) (x : G) :
	(f * g) x = (f.sum $ λa₁ b₁, g.sum $ λa₂ b₂, if a₁ * a₂ = x then b₁ * b₂ else 0) :=
	begin
	rw [mul_def],
	simp only [finsupp.sum_apply, single_apply],
	end

supposed to be a private lemma? It's not useable anywhere that doesn't have has_coe_to_fun, either via this PR or marking it as reducible.

[jcommelin]

Well, we either want coeff or has_coe_to_fun. Having neither seems very bad 😄
And so the mul_apply should be stated in terms of whatever we choose the API to be.

My intuition says: have coeff for a general (add_)monoid_algebra, and then do the has_coe_to_fun for the graded setting.

[eric-wieser]

I have no intuition at all about monoid_algebra, other than that they appear to be a superset of the behavior I want for my grading - so will defer to your decision on this.

[semorrison]

You're absolutely right that mul_apply reveals some poor design (mine, I think!).

My preference is definitely to introduce coeff. However I'm not going to do that myself in the near future, and if given the choice of no change, vs adding the has_coe_to_fun as a stopgap, I'd add has_coe_to_fun.

Do you want to have a go at introducing coeff for monoid_algebra? If not, let's get this merged, and perhaps create an issue to track the desire to introduce coeff later.

[jcommelin]

@eric-wieser @semorrison What shall we do here?

[eric-wieser]

I don't have any particular interest in developing monoid_algebra beyond what I need in #4321 - if the goal is to eventually add monoid_algebra.coeff, then that sounds like a refactor that should involve moving stuff from polynomial to monoid_algebra; something that should probably be done by someone who uses polynomial, not me.

As an argument for has_coe_to_fun - I quite like the model that monoid_algebra is "just finsupp but with convolutive multiplication". I suppose I could extract a conv_finsupp base class?

[eric-wieser]

Alternatively, since my only motivation here is #4321, we could close this PR and merge the two line change here as part of that PR, to make the motivation clear from the commit log.

[jcommelin]

@semorrison What do you think, shall we merge this for now (since mul_apply is already implicitly depending on this) and then refactor to use coeff at a later point?

[semorrison]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests