## Stream: maths

### Topic: Univariate polynomials

#### Kevin Buzzard (May 03 2018 at 18:34):

Here's another "canonical isomorphism" question. Johannes has implemented multivariate polynomials with variables in some index type sigma.

#### Kevin Buzzard (May 03 2018 at 18:34):

But the univariate theory (polynomials in one variable) is special

#### Kevin Buzzard (May 03 2018 at 18:35):

there are more theorems, for example; over a field these things form a Euclidean domain and a principal ideal domain etc

#### Kevin Buzzard (May 03 2018 at 18:35):

so there is probably an argument for developing the theory of polynomials in one variable further.

#### Kevin Buzzard (May 03 2018 at 18:35):

But one doesn't want to reprove everything

#### Kevin Buzzard (May 03 2018 at 18:36):

and for polynomials in one variable, Johannes' definition becomes (unit -> nat) ->_0 alpha

#### Kevin Buzzard (May 03 2018 at 18:36):

and unit -> nat is just canonically isomorphic to nat

#### Kevin Buzzard (May 03 2018 at 18:37):

so now we have a sort-of insane way of setting up univariate polys

#### Kevin Buzzard (May 03 2018 at 18:37):

and a sensible way

#### Kevin Buzzard (May 03 2018 at 18:38):

and one would imagine that the sensible way, nat ->_0 alpha, was the thing to use

#### Kevin Buzzard (May 03 2018 at 18:38):

but one wants to import all Johannes' work for free, like definitions and the proof that polynomials form a ring etc

#### Kevin Buzzard (May 03 2018 at 18:38):

so one first notes that there's an equiv between nat and (unit -> nat)

#### Kevin Buzzard (May 03 2018 at 18:39):

and then one wants to pull all of Johannes' definitions and theorems through this equiv

#### Kevin Buzzard (May 03 2018 at 18:40):

but currently in Lean this seems hard. Is that right?

#### Kevin Buzzard (May 03 2018 at 18:42):

I see. And this takes us back to exactly what we were thinking about a few days ago

#### Kevin Buzzard (May 03 2018 at 18:42):

whether ring is transportable

#### Kevin Buzzard (May 03 2018 at 18:42):

(and it should be)

#### Mario Carneiro (May 03 2018 at 18:47):

The short answer is yes, this is hard, but really it doesn't quite characterize the problem so well. We don't want to transfer the ring structure of (unit -> nat) ->_0 alpha to nat ->_0 alpha in the "naive way" because this would make all the operations filter through the equivalence which would make them hard to use

#### Kevin Buzzard (May 03 2018 at 18:49):

So if we need univariate polys

#### Kevin Buzzard (May 03 2018 at 18:49):

is the best idea currently just to re-implement them? :-/

#### Mario Carneiro (May 03 2018 at 18:49):

we would want instead to define the operations specially for univariate polys, but prove that the canonical equiv is a ring homomorphism and use that to prove that the other structure is a ring

#### Mario Carneiro (May 03 2018 at 18:50):

this is basically what transfer is intended to do

#### Mario Carneiro (May 03 2018 at 18:50):

You should check out num a bit to see how the process can work

#### Mario Carneiro (May 03 2018 at 18:51):

I define operations on num that act like corresponding operations on nat, prove that the map from nat to num preserves the operations, and use that to prove that num is a decidable_linear_ordered_semiring or whatever

#### Johan Commelin (May 03 2018 at 18:52):

Can't we have some meta code that automatically generates all the theorems and proof, given the equiv, so that it does the reimplementation for us? Together with transport statements that link the new implementation to the old one...

#### Kevin Buzzard (May 03 2018 at 18:52):

This approach is "better" than the one used to transfer proofs from multiplicative groups to additive groups, right?

#### Mario Carneiro (May 03 2018 at 18:52):

That's transfer

#### Kevin Buzzard (May 03 2018 at 18:52):

Because there the two types are themselves equivalent in a strong sense

#### Kevin Buzzard (May 03 2018 at 18:53):

so you can literally translate a proof that a group with multiplication as group law has some property, to the same proof that a group with addition as group law has some analogous property

#### Kevin Buzzard (May 03 2018 at 18:53):

but here unit -> nat is a different type to nat

#### Mario Carneiro (May 03 2018 at 18:54):

In some sense the equiv from add_group to group is "cheap"

#### Mario Carneiro (May 03 2018 at 18:55):

and the underlying carrier types are defeq, which helps a lot

#### Kevin Buzzard (May 03 2018 at 18:55):

and so the argument somehow relies on the fact that Johannes didn't do anything funny with his unit -> nat type which we can't also do with the nat type

#### Mario Carneiro (May 03 2018 at 18:56):

For more general equivalences, equiv does the job

#### Mario Carneiro (May 03 2018 at 18:56):

the argument doesn't rely on anything more

#### Mario Carneiro (May 03 2018 at 18:56):

(but you do have to prove that the equiv respects the operations)

Stupid question

#### Kevin Buzzard (May 03 2018 at 18:57):

what is an example of something you can do in type theory for unit -> nat which you can't do for nat

#### Kevin Buzzard (May 03 2018 at 18:57):

I can't make that rigorous

#### Mario Carneiro (May 03 2018 at 18:57):

they are equiv, so nothing?

#### Mario Carneiro (May 03 2018 at 18:58):

In PL theory they are a bit different, since one is like a delayed computation and the other is a value, but I assume you are ignoring this distinction

yes

#### Kevin Buzzard (May 03 2018 at 18:58):

If equiv commutes with everything in dependent type theory

#### Kevin Buzzard (May 03 2018 at 18:59):

why isn't this transportable stuff just standard and built in?

Is it in Coq?

#### Mario Carneiro (May 03 2018 at 18:59):

Of course it doesn't commute with everything, but you can always lift operations by pre/post composing with it

right

#### Kevin Buzzard (May 03 2018 at 18:59):

and if you go from X to Y and then back to X you will have the identity

#### Mario Carneiro (May 03 2018 at 19:00):

you will have propositionally the identity, it's (probably) not defeq

oh boy

#### Mario Carneiro (May 03 2018 at 19:00):

that means that you may need to cast stuff across the equality

#### Kevin Buzzard (May 03 2018 at 19:00):

but can a computer construct the proof if it's not defeq?

#### Mario Carneiro (May 03 2018 at 19:00):

and those casts build up and get more complicated

#### Mario Carneiro (May 03 2018 at 19:01):

the proof is given, it's an equiv so that's part of the structure

#### Johan Commelin (May 03 2018 at 19:02):

Ouch, so this is going to break us up if we are somewhere deep down in the guts of formalising the proof of the Weil conjectures

#### Johan Commelin (May 03 2018 at 19:02):

Because you exceed max_transfers which was set to 1000 or something...

#### Mario Carneiro (May 03 2018 at 19:03):

just try to have a better way to say stuff than transferring some other statement when casts get involved

#### Johan Commelin (May 03 2018 at 19:03):

(Maybe I am blatantly displaying my ignorance...)

#### Mario Carneiro (May 03 2018 at 19:03):

mostly avoid too many dependent types

#### Kevin Buzzard (May 03 2018 at 19:03):

we don't care that the proofs can get complicated because they are irrelevant

right

#### Kevin Buzzard (May 03 2018 at 19:04):

if I want to define affine 1-space

#### Kevin Buzzard (May 03 2018 at 19:04):

Spec(R[x])

#### Kevin Buzzard (May 03 2018 at 19:04):

then in the definition of e.g. the local ring at some point

#### Kevin Buzzard (May 03 2018 at 19:04):

there will be casts everywhere

#### Johan Commelin (May 03 2018 at 19:04):

Mario, I am a bit afraid that this is not so easy to avoid... or the formalisation might become way more difficult then they "maths" proof

#### Mario Carneiro (May 03 2018 at 19:05):

just break stuff up into bite sized chunks and it's all doable

#### Kevin Buzzard (May 03 2018 at 19:05):

Is this the reason that all the big type theory proofs of maths theorems are proofs about objects like finite groups rather than locally Noetherian schemes?

problems pile up

#### Kevin Buzzard (May 03 2018 at 19:06):

and it's difficult to make them go away

#### Johan Commelin (May 03 2018 at 19:06):

Ok, then I misunderstood you. I thought that if you started combining these "modules" then some evil synergy would multiply their "badness of casts"

#### Mario Carneiro (May 03 2018 at 19:07):

Just have solid abstraction layers, as long as the informal math doesn't get notationally horrible the formal horribleness is bounded

#### Johan Commelin (May 03 2018 at 19:07):

Ok, I really hope so.

#### Mario Carneiro (May 03 2018 at 19:07):

The multiplying badness of casts happens when you try to do it in general over the whole theory

#### Johan Commelin (May 03 2018 at 19:08):

If Kevin is meeting all these problems in the definition of an affine scheme... then we want 1) all sorts of properties of morphisms of schemes, 2) topos theory, 3) derived categories, 4) etale cohomology, 5)... etc etc

#### Mario Carneiro (May 03 2018 at 19:08):

i.e. you write some tactic that just plows through the whole system to transfer any term across some equiv

#### Johan Commelin (May 03 2018 at 19:08):

before you can even sensibly formulate the Weil conjectures

#### Mario Carneiro (May 03 2018 at 19:09):

these kinds of tactics care nothing for abstraction

#### Johan Commelin (May 03 2018 at 19:09):

Hmmm, I'm still confused...

#### Johan Commelin (May 03 2018 at 19:10):

Do you think that in the end we can have automation help us with these transfers, and still have the modularity? Or does the automation mean that it will "plow through the system"?

#### Kevin Buzzard (May 03 2018 at 19:10):

When I started reading proofs in mathlib

#### Kevin Buzzard (May 03 2018 at 19:11):

I was really confused why people would create a new structure and then instantly write functions giving access to the things used to construct the structure

but

it's all part

#### Kevin Buzzard (May 03 2018 at 19:11):

of a solid abstraction layer

#### Johan Commelin (May 03 2018 at 19:11):

Hmm, that's a good example. A "mathematician" wouldn't (want) to do that.

#### Johan Commelin (May 03 2018 at 19:12):

Again, couldn't some automation do that for us?

#### Kevin Buzzard (May 03 2018 at 19:12):

Getting the code to run fast is not our problem :-)

#### Mario Carneiro (May 03 2018 at 19:12):

In theory, but it probably would need lots of tweaks

#### Kevin Buzzard (May 03 2018 at 19:12):

You just wait for either the CS people to write better tactics or for the engineers to write faster chips

#### Johan Commelin (May 03 2018 at 19:12):

If I write structure then Lean should immediately add those boilerplate things...

#### Kevin Buzzard (May 03 2018 at 19:13):

Sometimes the access to the constructor has a different name to the constructor

#### Kevin Buzzard (May 03 2018 at 19:13):

that happens with the proofs in equiv IIRC

#### Mario Carneiro (May 03 2018 at 19:13):

If you look closely you will notice that the "boilerplate" often differs in minor details like use of notation, binding explicitness,...

#### Mario Carneiro (May 03 2018 at 19:13):

The structure command already tries its best to give you theorems the way you want

#### Mario Carneiro (May 03 2018 at 19:14):

but it's using heuristics, and sometimes we want it different in a particular case

#### Johan Commelin (May 03 2018 at 19:14):

Yeah, I've seen that. So maybe we "mathematicians" should just learn to be more precise. (But we don't buy that mathematics isn't precise enough...)

#### Mario Carneiro (May 03 2018 at 19:15):

It's like how there are (natural language) grammar rules, but also exceptions

#### Kevin Buzzard (May 03 2018 at 19:15):

equiv.apply_inverse_apply

#### Kevin Buzzard (May 03 2018 at 19:16):

There's a solid abstraction layer in action

#### Kevin Buzzard (May 03 2018 at 19:21):

import data.equiv
example (X Y : Type) (e : equiv X Y) : e.apply_inverse_apply = e.right_inv := rfl


#### Kevin Buzzard (May 03 2018 at 22:08):

How about writing a regex which will replace all (sigma ->_0 nat) with (nat) and then make it all work again?

#### Kevin Buzzard (May 03 2018 at 22:08):

that sounds like an interesting challenge

#### Mario Carneiro (May 04 2018 at 02:02):

That sounds like it should wait for lean 4, when the parser is exposed to lean code

#### Johan Commelin (May 04 2018 at 06:35):

But we could just do an actual copy-paste-search-replace, right? The only thing that would remain is some theorems that say the result is isomorphic to what you started with.

#### Kevin Buzzard (May 04 2018 at 22:16):

https://github.com/johoelzl/mason-stother/blob/e6e1eb353d3dbea93571f761b408bc4900472179/poly_over_field.lean#L138

#### Kevin Buzzard (May 04 2018 at 22:17):

Johannes or his coauthor implemented polys in 1 variable already

#### Johan Commelin (May 05 2018 at 18:38):

Wow, there's already quite a lot there!

#### Scott Morrison (May 07 2018 at 01:29):

I'm not too up on univariate polynomials in Lean yet. Does anyone know if we have:
"evaluation of p : Z[x] at x : R is a ring homomorphism from Z[x] to R"?

#### Johan Commelin (May 07 2018 at 06:32):

@Scott Morrison Voila, but multivariate: https://github.com/leanprover/mathlib/blob/master/linear_algebra/multivariate_polynomial.lean#L171-L173

#### Johan Commelin (May 07 2018 at 06:34):

Ok, and they haven't made it a ring homomorphism, but they show that it is additive and multiplicative...

#### Patrick Massot (May 07 2018 at 07:28):

@Johannes Hölzl what is the status of https://github.com/johoelzl/mason-stother? I guess JWageM is your student or something like this? Will this be in mathlib at some point?

#### Johannes Hölzl (May 07 2018 at 07:34):

Yes, @Jens Wagemaker is currently writing his Bachelor thesis on Mason-Stother. The theory itself is finished, and now he is writing the thesis itself. When this is finished we will port most parts of the developed theory to mathlib. Most parts, as we assume that polynomials over a field form a unique factorization domain, so everything from there on will need to wait until this is done. And there is quiet some divergence between the mathlib version Jens used and the current one, so there is some merging to be done.

#### Patrick Massot (May 07 2018 at 07:35):

I think someone did Euclidean domains recently

#### Patrick Massot (May 07 2018 at 07:35):

https://github.com/leanprover/mathlib/blob/d5c73c0b372d1181ca386e3264497e2c56077d93/algebra/euclidean_domain.lean

#### Patrick Massot (May 07 2018 at 07:37):

So it shouldn't be too hard to get UFD for polynomials with one variable over a field

#### Johannes Hölzl (May 07 2018 at 07:37):

No, it shouldn't be hard. Just needs to be done.

#### Johan Commelin (May 08 2018 at 05:46):

It seems to me that maybe eval should take its arguments in the opposite order. Then one can curry it, and get a (semi)-ring homomorphism.

#### Johan Commelin (May 08 2018 at 05:46):

Does that make sense?

#### Johan Commelin (May 08 2018 at 07:41):

Here is a commit that swaps the order of the arguments, and also proves that eval f is a ring homomorphism:
https://github.com/jcommelin/mathlib/commit/b0d0ca6d2892c902c5feffdfa58d3e3be2b013b2

Looks promising!

#### Johannes Hölzl (May 08 2018 at 08:20):

@Johan Commelin chaning the argument order of eval is a good idea. But is there a reason why you changed the applications from p.eval f to eval f p? Even with the changed order the p.eval f syntax should work. Lean figures out that p is a polynomial and looks up mv_polynomial.eval, inserting p at the appropriate place.

Ok cool!

#### Johan Commelin (May 08 2018 at 08:21):

I didn't know that

#### Johan Commelin (May 08 2018 at 08:21):

But then, maybe I actually prefer f.eval (p+q) etc...

#### Johan Commelin (May 08 2018 at 08:21):

What do you think of that?

#### Johan Commelin (May 08 2018 at 08:21):

And then f.eval becomes a ring hom

#### Johan Commelin (May 08 2018 at 08:22):

Aah, but that won't work, I guess... because then it doens't know where to find eval

Right?

#### Johan Commelin (May 08 2018 at 08:22):

There is some namespacing-magic going on, and that is why p.eval does work?

#### Johan Commelin (May 08 2018 at 08:23):

/me is still learning new things every minute

#### Johan Commelin (May 08 2018 at 08:28):

@Johannes Hölzl I think I prefer the eval f p notation. Even better would be some sort of eval_f p.

#### Johan Commelin (May 08 2018 at 08:29):

Also, as a mathematician I always write f for polynomials, and p or x for the map \sigma \to \alpha. So that was pretty confusing (-;

#### Johannes Hölzl (May 08 2018 at 08:31):

Well I would write f for the polynomial function (i.e. a function which can be represented as a polynomial) but I write p, q etc for the syntactic object.

#### Johan Commelin (May 08 2018 at 08:33):

Yeah, I get that. (I only work with the syntactic objects... not the functions.)

#### Johannes Hölzl (May 08 2018 at 08:34):

Also, f.eval p doesn't work as f is in the function space, which AFAIK doesn't work with this syntax mechanism.

#### Johannes Hölzl (May 08 2018 at 08:35):

I prefer p.eval f as eval is a very generic name, and we will surely have multiple instances in different namespaces. p.eval makes it clear that we are referring to the polynomial one.

#### Johannes Hölzl (May 08 2018 at 08:35):

It is not necessary in mv_polynomial, but might be in other cases.

#### Johan Commelin (May 08 2018 at 08:39):

Ok, whichever you prefer. Should I change it and PR it?

#### Johannes Hölzl (May 08 2018 at 08:45):

Yeah, just change it back how it was before.

#### Johan Commelin (May 08 2018 at 08:59):

Oh my, it looks like I overdid it: https://github.com/jcommelin/mathlib/commit/2f63d86718e9e00ea55f67cb22f0f306fe8fcde3

#### Johannes Hölzl (May 08 2018 at 10:12):

why do you remove eval_zero?

#### Johan Commelin (May 08 2018 at 11:08):

Because it follows from eval_C...

#### Johannes Hölzl (May 08 2018 at 11:14):

But the simplifier doesn't see that 0 = C 0! This is the reason for eval_zero: it is a @[simp] rule.