Zulip Chat Archive

Stream: maths

Topic: Polynomials


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?

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

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!

Kenny Lau (Apr 04 2018 at 09:09):

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

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?

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.

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.

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

Sebastien Gouezel (Dec 01 2019 at 20:10):

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

Rob Lewis (Dec 01 2019 at 20:11):

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

Rob Lewis (Dec 01 2019 at 20:12):

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

Sebastien Gouezel (Dec 01 2019 at 20:13):

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

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.

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)

Rob Lewis (Dec 01 2019 at 20:19):

Oh, I see what you mean.

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.

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.

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.

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

Yury G. Kudryashov (Apr 10 2020 at 08:19):

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

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

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

Reid Barton (Apr 10 2020 at 13:03):

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

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.

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.

Yury G. Kudryashov (Apr 10 2020 at 18:25):

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

Kevin Buzzard (Apr 10 2020 at 18:25):

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

Johan Commelin (Apr 10 2020 at 18:26):

Why not?

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.

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

Kevin Buzzard (Apr 10 2020 at 18:27):

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

Kevin Buzzard (Apr 10 2020 at 18:27):

I know I can make it in maths.

Johan Commelin (Apr 10 2020 at 18:27):

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

Kevin Buzzard (Apr 10 2020 at 18:28):

Removing comm_ the definition still compiles.

Kevin Buzzard (Apr 10 2020 at 18:30):

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

Yury G. Kudryashov (Apr 10 2020 at 18:34):

These lines were already rewritten in my branch.

Yury G. Kudryashov (Apr 10 2020 at 18:34):

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

Yury G. Kudryashov (Apr 10 2020 at 18:35):

Currently all eval code is based on monoid_algebra.lift

Yury G. Kudryashov (Apr 10 2020 at 18:35):

(defined in a pending PR, to be updated)

Yury G. Kudryashov (Apr 10 2020 at 18:36):

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

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?

Kevin Buzzard (Apr 10 2020 at 19:39):

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

Yury G. Kudryashov (Apr 10 2020 at 19:42):

@Kevin Buzzard Sorry. @Reid Barton :up:

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.

Reid Barton (Apr 11 2020 at 01:37):

Is that going to be a big problem?

Yury G. Kudryashov (Apr 11 2020 at 04:11):

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

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: Dec 20 2023 at 11:08 UTC