Zulip Chat Archive

Stream: maths

Topic: Univariate polynomials


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:34):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:35):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:35):

But one doesn't want to reprove everything

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:36):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:36):

and unit -> nat is just canonically isomorphic to nat

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:37):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:37):

and a sensible way

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:38):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:38):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:39):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:40):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:42):

whether ring is transportable

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:42):

(and it should be)

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 03 2018 at 18:48):

(not to mention inefficient, not sure if we are deciding to care about this here)

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:49):

So if we need univariate polys

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:49):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 03 2018 at 18:50):

this is basically what transfer is intended to do

view this post on Zulip Mario Carneiro (May 03 2018 at 18:50):

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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (May 03 2018 at 18:52):

That's transfer

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:52):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:53):

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

view this post on Zulip Mario Carneiro (May 03 2018 at 18:54):

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

view this post on Zulip Mario Carneiro (May 03 2018 at 18:55):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 03 2018 at 18:56):

For more general equivalences, equiv does the job

view this post on Zulip Mario Carneiro (May 03 2018 at 18:56):

the argument doesn't rely on anything more

view this post on Zulip Mario Carneiro (May 03 2018 at 18:56):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:57):

Stupid question

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:57):

I can't make that rigorous

view this post on Zulip Mario Carneiro (May 03 2018 at 18:57):

they are equiv, so nothing?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:58):

yes

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:58):

If equiv commutes with everything in dependent type theory

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:59):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:59):

Is it in Coq?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 03 2018 at 18:59):

right

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 03 2018 at 19:00):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 19:00):

oh boy

view this post on Zulip Mario Carneiro (May 03 2018 at 19:00):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 19:00):

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

view this post on Zulip Mario Carneiro (May 03 2018 at 19:00):

and those casts build up and get more complicated

view this post on Zulip Mario Carneiro (May 03 2018 at 19:01):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 03 2018 at 19:02):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 03 2018 at 19:03):

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

view this post on Zulip Mario Carneiro (May 03 2018 at 19:03):

mostly avoid too many dependent types

view this post on Zulip Kevin Buzzard (May 03 2018 at 19:03):

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

view this post on Zulip Mario Carneiro (May 03 2018 at 19:03):

I'm talking about terms

view this post on Zulip Kevin Buzzard (May 03 2018 at 19:03):

right

view this post on Zulip Kevin Buzzard (May 03 2018 at 19:04):

if I want to define affine 1-space

view this post on Zulip Kevin Buzzard (May 03 2018 at 19:04):

Spec(R[x])

view this post on Zulip Kevin Buzzard (May 03 2018 at 19:04):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 19:04):

there will be casts everywhere

view this post on Zulip Kevin Buzzard (May 03 2018 at 19:04):

it will be unreadable

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 03 2018 at 19:05):

It's all about modularity

view this post on Zulip Mario Carneiro (May 03 2018 at 19:05):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 03 2018 at 19:06):

problems pile up

view this post on Zulip Kevin Buzzard (May 03 2018 at 19:06):

and it's difficult to make them go away

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 03 2018 at 19:07):

Ok, I really hope so.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 03 2018 at 19:08):

before you can even sensibly formulate the Weil conjectures

view this post on Zulip Mario Carneiro (May 03 2018 at 19:09):

these kinds of tactics care nothing for abstraction

view this post on Zulip Johan Commelin (May 03 2018 at 19:09):

Hmmm, I'm still confused...

view this post on Zulip 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"?

view this post on Zulip Kevin Buzzard (May 03 2018 at 19:10):

When I started reading proofs in mathlib

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 03 2018 at 19:11):

but

view this post on Zulip Kevin Buzzard (May 03 2018 at 19:11):

it's all part

view this post on Zulip Kevin Buzzard (May 03 2018 at 19:11):

of a solid abstraction layer

view this post on Zulip Johan Commelin (May 03 2018 at 19:11):

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

view this post on Zulip Johan Commelin (May 03 2018 at 19:12):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 19:12):

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

view this post on Zulip Mario Carneiro (May 03 2018 at 19:12):

In theory, but it probably would need lots of tweaks

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 03 2018 at 19:12):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 19:13):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 19:13):

that happens with the proofs in equiv IIRC

view this post on Zulip 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,...

view this post on Zulip Mario Carneiro (May 03 2018 at 19:13):

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

view this post on Zulip Mario Carneiro (May 03 2018 at 19:14):

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

view this post on Zulip 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...)

view this post on Zulip Mario Carneiro (May 03 2018 at 19:15):

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

view this post on Zulip Kevin Buzzard (May 03 2018 at 19:15):

equiv.apply_inverse_apply

view this post on Zulip Kevin Buzzard (May 03 2018 at 19:16):

There's a solid abstraction layer in action

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 03 2018 at 22:08):

that sounds like an interesting challenge

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 04 2018 at 22:16):

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

view this post on Zulip Kevin Buzzard (May 04 2018 at 22:17):

Johannes or his coauthor implemented polys in 1 variable already

view this post on Zulip Johan Commelin (May 05 2018 at 18:38):

Wow, there's already quite a lot there!

view this post on Zulip 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"?

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 07 2018 at 07:35):

I think someone did Euclidean domains recently

view this post on Zulip Patrick Massot (May 07 2018 at 07:35):

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

view this post on Zulip 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

view this post on Zulip Johannes Hölzl (May 07 2018 at 07:37):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 08 2018 at 05:46):

Does that make sense?

view this post on Zulip 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

view this post on Zulip Scott Morrison (May 08 2018 at 08:15):

Looks promising!

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 08 2018 at 08:20):

Ok cool!

view this post on Zulip Johan Commelin (May 08 2018 at 08:21):

I didn't know that

view this post on Zulip Johan Commelin (May 08 2018 at 08:21):

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

view this post on Zulip Johan Commelin (May 08 2018 at 08:21):

What do you think of that?

view this post on Zulip Johan Commelin (May 08 2018 at 08:21):

And then f.eval becomes a ring hom

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 08 2018 at 08:22):

Right?

view this post on Zulip Johan Commelin (May 08 2018 at 08:22):

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

view this post on Zulip Johan Commelin (May 08 2018 at 08:23):

/me is still learning new things every minute

view this post on Zulip 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.

view this post on Zulip 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 (-;

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 08 2018 at 08:33):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johannes Hölzl (May 08 2018 at 08:35):

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

view this post on Zulip Johan Commelin (May 08 2018 at 08:39):

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

view this post on Zulip Johannes Hölzl (May 08 2018 at 08:45):

Yeah, just change it back how it was before.

view this post on Zulip Johan Commelin (May 08 2018 at 08:59):

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

view this post on Zulip Johannes Hölzl (May 08 2018 at 10:12):

why do you remove eval_zero?

view this post on Zulip Johan Commelin (May 08 2018 at 11:08):

Because it follows from eval_C...

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 08 2018 at 11:26):

Hmmm, my bad...

view this post on Zulip Johan Commelin (May 08 2018 at 11:27):

I'll fix it

view this post on Zulip Johan Commelin (May 08 2018 at 11:31):

https://github.com/jcommelin/mathlib/commit/fa1710d88ff007cd947645136dd6c8986028430d
Voila


Last updated: May 18 2021 at 06:15 UTC