Zulip Chat Archive

Stream: maths

Topic: notation for mv_polynomial.aeval

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)$ . 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

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...

Kevin Buzzard (Jul 21 2020 at 14:39):

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

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.

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.

Kevin Buzzard (Jul 21 2020 at 14:52):

Can you coerce to a dependent function?

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.

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).

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).

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

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.

Anne Baanen (Jul 21 2020 at 15:23):

Oh yeah, that makes it even worse.

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.

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.

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...

Rob Lewis (Jul 21 2020 at 15:45):

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

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.

Johan Commelin (Jul 21 2020 at 16:01):

Yup... )-;

Anne Baanen (Jul 21 2020 at 16:03):

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

Last updated: Dec 20 2023 at 11:08 UTC