# 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 `n`

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

- Move many theorems to
`monoid_algebra`

to facilitate declaration of other types of (pseudo) polynomials. - Use bundled homomorphisms.
- (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 $\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]$ where $R$ is noncommutative but $x$ 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]$ if $R$ 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 $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 (Apr 10 2020 at 18:27):

$(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: May 11 2021 at 15:12 UTC