Zulip Chat Archive

Stream: maths

Topic: Refactoring polynomials


view this post on Zulip Johan Commelin (Jan 27 2020 at 12:21):

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

view this post on Zulip Johan Commelin (Jan 27 2020 at 12:22):

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?

view this post on Zulip Johan Commelin (Jan 27 2020 at 12:23):

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

view this post on Zulip Johan Commelin (Jan 27 2020 at 12:24):

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

view this post on Zulip Johan Commelin (Jan 27 2020 at 12:24):

Is there any chance we can make that happen?

view this post on Zulip Johan Commelin (Jan 27 2020 at 12:29):

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

view this post on Zulip Kevin Buzzard (Jan 27 2020 at 12:31):

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.

view this post on Zulip Yury G. Kudryashov (Jan 27 2020 at 20:18):

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

view this post on Zulip Yury G. Kudryashov (Jan 27 2020 at 20:20):

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

view this post on Zulip Yury G. Kudryashov (Jan 27 2020 at 20:24):

@Johan Commelin We have fin.cons

view this post on Zulip Yury G. Kudryashov (Jan 27 2020 at 20:25):

It has the desired type but lacks notation.


Last updated: May 12 2021 at 07:17 UTC