Zulip Chat Archive

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

Mario Carneiro (May 03 2018 at 18:48):

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

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)

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

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

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

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?

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

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

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

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

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

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

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

I'm talking about terms

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

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

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

it will be unreadable

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

It's all about modularity

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?

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

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

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

but

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

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

Scott Morrison (May 08 2018 at 08:15):

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.

Johan Commelin (May 08 2018 at 08:20):

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

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

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.