Polynomials

Stream: maths

[Scott Morrison]

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

[Mario Carneiro]

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]

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]

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

[Sebastien Gouezel]

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]

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]

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]

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]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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]

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]

Oh, I see what you mean.

[Johan Commelin]

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]

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

[Yury G. Kudryashov]

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]

@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]

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

[Yury G. Kudryashov]

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

[Reid Barton]

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

[Reid Barton]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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

[Johan Commelin]

Why not?

[Kevin Buzzard]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I know I can make it in maths.

[Johan Commelin]

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

[Kevin Buzzard]

Removing comm_ the definition still compiles.

[Kevin Buzzard]

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

[Yury G. Kudryashov]

These lines were already rewritten in my branch.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

Currently all eval code is based on monoid_algebra.lift

[Yury G. Kudryashov]

(defined in a pending PR, to be updated)

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

@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]

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

[Yury G. Kudryashov]

@Kevin Buzzard Sorry. @Reid Barton :up:

[Reid Barton]

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

[Reid Barton]

Is that going to be a big problem?

[Yury G. Kudryashov]

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

[Reid Barton]

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.