Zulip Chat Archive

Stream: maths

Topic: notation for mv_polynomial.aeval


view this post on Zulip Rob Lewis (Jul 21 2020 at 14:19):

@Johan Commelin has complained about the notation for aeval, evaluating a mv_polynomial in an algebra. aeval v f is morally just f(v)f(v). What do people think about introducing localized notation for this? And are there analogous notations in mathlib that I'm not aware of? One proposal, f ᵃ v:= aeval v f

view this post on Zulip Kevin Buzzard (Jul 21 2020 at 14:38):

I suppose a coercion to an algebra hom is out of the question? I guess we don't know the target...

view this post on Zulip Kevin Buzzard (Jul 21 2020 at 14:39):

What's wrong with f(v)? Is that overloaded? Can we do that in Lean 4?

view this post on Zulip Rob Lewis (Jul 21 2020 at 14:51):

Naively adding a coe_to_fn instance seems to loop. I'm a little skeptical about getting that to work.

view this post on Zulip Rob Lewis (Jul 21 2020 at 14:51):

f(v) is overloaded with normal function application, it would need to be handled by a coercion.

view this post on Zulip Kevin Buzzard (Jul 21 2020 at 14:52):

Can you coerce to a dependent function?

view this post on Zulip Rob Lewis (Jul 21 2020 at 15:04):

In principle yes, in this case I'm not sure how to do it without instance loops.

view this post on Zulip Johan Commelin (Jul 21 2020 at 15:12):

Kevin Buzzard said:

I suppose a coercion to an algebra hom is out of the question? I guess we don't know the target...

aeval v is an algebra hom (right now, in mathlib).

view this post on Zulip Johan Commelin (Jul 21 2020 at 15:13):

But aeval is an ugly combo of ascii characters, and in aeval v f the order of f and v is backwards from f(v).

view this post on Zulip Anne Baanen (Jul 21 2020 at 15:18):

coe_to_fn sounds problematic since we already have a coe_to_fn on finsupp that applies (which would give the coefficients), and polynomial is not irreducible

view this post on Zulip Rob Lewis (Jul 21 2020 at 15:20):

Even worse there's elaboration order fun, since it can't figure out from the polynomial what ring it's supposed to be an algebra over. I think this makes the coe_to_fn instance impossible and a has_coe instance still loops, it doesn't pick up the ring from the target type.

view this post on Zulip Anne Baanen (Jul 21 2020 at 15:23):

Oh yeah, that makes it even worse.

view this post on Zulip Anne Baanen (Jul 21 2020 at 15:24):

Do we need an eval apart from aeval anyway? There will always be an instance for [algebra R R], and any algebra_map arising from it will be simped away hopefully.

view this post on Zulip Anne Baanen (Jul 21 2020 at 15:26):

So we could delete eval (but not the lemmas?) and rename aeval to eval. If we don't add notation, that should clean up the situation.

view this post on Zulip Anne Baanen (Jul 21 2020 at 15:44):

A quick hack indicates yes: we can just get rid of eval and rename aeval to eval. But there is some painful refactoring to do in that case...

view this post on Zulip Rob Lewis (Jul 21 2020 at 15:45):

Hah, I was just typing. It sounds plausible but it's a huge refactor.

view this post on Zulip Anne Baanen (Jul 21 2020 at 15:49):

Ah, a first snag: we explicitly want R to be noncommutative here, but an R-algebra requires R to be commutative.

view this post on Zulip Johan Commelin (Jul 21 2020 at 16:01):

Yup... )-;

view this post on Zulip Anne Baanen (Jul 21 2020 at 16:03):

I put my experiment online here for anyone who wants to continue.


Last updated: May 10 2021 at 06:13 UTC