Zulip Chat Archive

Stream: maths

Topic: Polynomials


view this post on Zulip Scott Morrison (Apr 04 2018 at 04:46):

Where can I find the following facts: Z[x] is a commutative ring, and evaluation at x = i is a ring homomorphism?

view this post on Zulip Mario Carneiro (Apr 04 2018 at 04:50):

I don't think we have specialized to univariate polynomials, but mv_polynomial and an evaluation operation on it are defined in multivariate_polynomial

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 09:07):

Scott -- Kenny has been working on adjoint functors of various forgetful functors, and I pointed out to him that the adjoint of the forgetful functor from commutative rings to sets would give both of the things you ask about for free. Are you back to an internet connection yet? He should talk to you about category theory!

view this post on Zulip Kenny Lau (Apr 04 2018 at 09:09):

@Kevin Buzzard https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/category.20theory.20libraries/near/124608241

view this post on Zulip Sebastien Gouezel (Dec 01 2019 at 19:39):

I opened polynomial.lean for the first time as I will need to show that the derivative of a polynomial (in the analytic sense) is given by the algebraic definition p.derivative. I was surprised to see that there is no coercion from polynomial K to K -> K: to evaluate a polynomial p on x, one should write p.eval x. Do you know the reason for this?

view this post on Zulip Johan Commelin (Dec 01 2019 at 19:57):

Initially the coercion was to p.coeff... So p n would be the nth coefficient of p. Indeed, coeff wasn't even defined.

view this post on Zulip Rob Lewis (Dec 01 2019 at 20:07):

I'm not sure how it is now, but we've had some complicated type class issues with polynomials in the past. Maybe the coercion wasn't used to avoid creating more problems.

view this post on Zulip Sebastien Gouezel (Dec 01 2019 at 20:09):

The coercion to p.coeff is still there, but only locally in the polynomial file

def coeff_coe_to_fun : has_coe_to_fun (polynomial α) :=
finsupp.has_coe_to_fun

local attribute [instance] finsupp.comm_semiring coeff_coe_to_fun

so, you think the lack of the natural coercion is only for historical reasons, and not because the coercion created some problems down the way?

Also, because of the order of variables in

/-- `eval x p` is the evaluation of the polynomial `p` at `x` -/
def eval : α  polynomial α  α

one can not talk of the function p.eval, only of (λx, p.eval x)... Anyway, this is good enough for what I have to do, and I don't know well enough the subtleties of this part of the library, so I am not going to try to improve this. A big warning in polynomial.lean might be helpful to those who, just like me, will assume from the start that the coercion should be there, and will try to debug their own code when it doesn't work :)

view this post on Zulip Sebastien Gouezel (Dec 01 2019 at 20:10):

I was answering @Johan Commelin , not @Rob Lewis here.

view this post on Zulip Rob Lewis (Dec 01 2019 at 20:11):

Why can't you talk about p.eval? That's definitely used in places.

view this post on Zulip Rob Lewis (Dec 01 2019 at 20:12):

e.g. https://github.com/leanprover-community/mathlib/blob/master/src/data/padics/hensel.lean#L435

view this post on Zulip Sebastien Gouezel (Dec 01 2019 at 20:13):

You can talk of p.eval x, but not of p.eval just by itself.

view this post on Zulip Sebastien Gouezel (Dec 01 2019 at 20:15):

So,

has_deriv_at p.eval (p.derivative.eval x) x

does not typecheck, but

has_deriv_at (λx, p.eval x) (p.derivative.eval x) x

does.

view this post on Zulip Sebastien Gouezel (Dec 01 2019 at 20:17):

This order of variables makes sense, though, as it makes it possible to write

instance eval.is_semiring_hom : is_semiring_hom (eval x)

view this post on Zulip Rob Lewis (Dec 01 2019 at 20:19):

Oh, I see what you mean.

view this post on Zulip Johan Commelin (Dec 01 2019 at 20:20):

This order of variables makes sense, though, as it makes it possible to write

instance eval.is_semiring_hom : is_semiring_hom (eval x)

I think that was the main reason to have this order of variables. Because p.eval usually doesn't have good algebraic properties.

view this post on Zulip Yury G. Kudryashov (Apr 10 2020 at 00:00):

I'm rewriting polynomials on top of #2303 and #2366 heavily using monoid_algebra. Writing here to avoid duplication of effort.

view this post on Zulip Yury G. Kudryashov (Apr 10 2020 at 00:02):

My main goals:

  1. Move many theorems to monoid_algebra to facilitate declaration of other types of (pseudo) polynomials.
  2. Use bundled homomorphisms.
  3. (probably in another PR): rewrite mv_polynomials using new lemmas in monoid_algebra.

view this post on Zulip Johan Commelin (Apr 10 2020 at 05:15):

@Yury G. Kudryashov Cool, thanks! Are you first doing polynomial and postponing mv_polynomial? Or did I misunderstand you? Because another idea we had for a refactor was to redefine polynomial as mv_polynomial unit...

view this post on Zulip Yury G. Kudryashov (Apr 10 2020 at 08:19):

I want to have them separately but move all non-trivial lemmas to monoid_algebra.

view this post on Zulip Yury G. Kudryashov (Apr 10 2020 at 08:21):

And possibly add, e.g., quasi-polynomials eλkxPk(x)\sum e^{\lambda_k x}P_k(x).

view this post on Zulip Reid Barton (Apr 10 2020 at 13:02):

Oh, while you are in the area, are you planning to generalize the basic constructions to noncommutative rings? (Specifically, I once wanted R[x]R[x] where RR is noncommutative but xx is central.)

view this post on Zulip Reid Barton (Apr 10 2020 at 13:03):

From some comments of yours from long ago, I'm guessing/hoping the answer is yes

view this post on Zulip Yury G. Kudryashov (Apr 10 2020 at 18:24):

Currently I assume that R is commutative but aeval works on a non-commutative R-algebra.

view this post on Zulip Yury G. Kudryashov (Apr 10 2020 at 18:24):

I.e., R has coefficients in a commutative semiring and evaluates in a possibly non-commutative R-algebra.

view this post on Zulip Yury G. Kudryashov (Apr 10 2020 at 18:25):

Otherwise I don't know how to deal with f * g.

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 18:25):

Can we even make R[x]R[x] if RR is non-commutative?

view this post on Zulip Johan Commelin (Apr 10 2020 at 18:26):

Why not?

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 18:27):

If the machinery already lets us define this and also define the multiplication for free (assume xx commutes with the elements of RR) then we may as well include it, even if we have to assume RR commutative for most of the lemmas.

view this post on Zulip Johan Commelin (Apr 10 2020 at 18:27):

(aX+b)(cX+d)=acX2+(ad+bc)X+bd(aX + b)(cX + d) = acX^2 + (ad + bc)X + bd

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 18:27):

@Johan Commelin I just meant def polynomial (α : Type*) [comm_semiring α] := add_monoid_algebra α ℕ has comm in

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 18:27):

I know I can make it in maths.

view this post on Zulip Johan Commelin (Apr 10 2020 at 18:27):

Aah, mathlib can't do it, right now.

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 18:28):

Removing comm_ the definition still compiles.

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 18:30):

the first 180 lines of data.polynomial work fine if you remove a few comm_s

view this post on Zulip Yury G. Kudryashov (Apr 10 2020 at 18:34):

These lines were already rewritten in my branch.

view this post on Zulip Yury G. Kudryashov (Apr 10 2020 at 18:34):

I'll have to start with algebras over non-commutative semirings.

view this post on Zulip Yury G. Kudryashov (Apr 10 2020 at 18:35):

Currently all eval code is based on monoid_algebra.lift

view this post on Zulip Yury G. Kudryashov (Apr 10 2020 at 18:35):

(defined in a pending PR, to be updated)

view this post on Zulip Yury G. Kudryashov (Apr 10 2020 at 18:36):

This approach gives us a lot of properties for free without induction on p.

view this post on Zulip Yury G. Kudryashov (Apr 10 2020 at 19:36):

@Kevin Buzzard What kind of eval2 do you want in this case? I want aeval to be the main interface so it is easy to deal with f : R →+* S with a comm_semiring S or f : R →+* center S. Do you need f : R →+* centralizer x?

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 19:39):

I don't need anything, it was Reid who wanted noncommutative rings.

view this post on Zulip Yury G. Kudryashov (Apr 10 2020 at 19:42):

@Kevin Buzzard Sorry. @Reid Barton :up:

view this post on Zulip Reid Barton (Apr 11 2020 at 01:36):

Well, currently we don't have algebras over a noncommutative ring and I am not sure the concept makes sense.

view this post on Zulip Reid Barton (Apr 11 2020 at 01:37):

Is that going to be a big problem?

view this post on Zulip Yury G. Kudryashov (Apr 11 2020 at 04:11):

No, I've figured out how to do it.

view this post on Zulip Reid Barton (Apr 11 2020 at 04:16):

I could figure out what specifically I wanted to do with these noncommutative polynomials if it's still useful. It would just require recalling some things I last thought about a year or so ago.


Last updated: May 11 2021 at 15:12 UTC