Refactoring polynomials

Stream: maths

[Johan Commelin]

I'm starting a new thread on this topic. For reference, @Yury G. Kudryashov wrote a proposal over here: #1864
A lot of previous discussion is over here: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Algebraic.20geometry.20course/near/186673407

[Johan Commelin]

One thing that I would really like to have is given f : polynomial R and r : R, that f r becomes f.eval r. I guess that is possible with coe_to_fun.
However... can we do a similar thing for mv polynomials, and maintain readability?

[Johan Commelin]

This would require some hackery, because it requires a linear ordering on σ

[Johan Commelin]

Suppose that f : mv_polynomial (fin 3) R. Then I would love to be able to write f [r₁, r₂, r₃].

[Johan Commelin]

Is there any chance we can make that happen?

[Johan Commelin]

Should we add special support for polynomials in n : ℕ variables?

[Kevin Buzzard]

I've been doing algebraic geometry and I'm just at the point where I want to talk about polynomials in n variables. I don't really know what to do. I know what theorems I want to prove but I'm still very confused about what exactly is being suggested. I would happily start refactoring mv_polynomial if someone said "here's the definitions, here are ten theorems, can you prove then?" but I don't know where to start if I don't have definitions.

[Yury G. Kudryashov]

I think, a good first step would be to move algebra below polynomials in the import chain. This means moving aeval to polynomials.

[Yury G. Kudryashov]

The next step is to define monoid_algebra (e.g., as finsupp or dfinsupp) and prove the universal property (is it already in finsupp?).

[Yury G. Kudryashov]

@Johan Commelin We have fin.cons

[Yury G. Kudryashov]

It has the desired type but lacks notation.