Stream: maths

Topic: of_subring as a coercion

Jack J Garzella (May 15 2020 at 02:55):

It would sure be nice for to have polynomials in $\mathbb{Z}[X]$ automatically coerce to polynomials in $\mathbb{Q}[X]$. The conversion is implemented in the ring_theory folder, but it isn't made into a coercion, and I'm not sure if it's a technical obstacle or if I should make a PR. Is there anything preventing of_subring in ring_theory/polynomial.lean from having an instance of has_coe (polynomial T) (polynomial R)?

Johan Commelin (May 15 2020 at 03:39):

@Jack J Garzella But int is not a subring of rat, so that will not help you, right? But I think that at the moment the API for polynomials is quite "fragile" for lack of a better word (with eval, eval₂, map, etc) so I'm weary of putting in coercions.

Johan Commelin (May 15 2020 at 03:41):

Also, in practice it might be helpful to use bundled ring homs a lot. They read less nice, but they give a lot more power. I've head many many troubles with trying rw map_mul on map f (p * q) and lean complaining that it couldn't figure out why f was a is_semiring_hom.

Johan Commelin (May 15 2020 at 03:41):

If you use bundled homs, that problem completely vanishes.

Johan Commelin (May 15 2020 at 03:41):

But of course int.cast_ring_hom rat is very ugly, compared to "the invisible map"

Jack J Garzella (May 15 2020 at 03:42):

Yes, I realized this, I guess it could technically be #xy again. I can do what I want to do, I'm interested in discussing how we can get rid of int.cast_ring_hom rat everywhere though

Jack J Garzella (May 15 2020 at 03:43):

Do you think the polynomial api just needs to be used more before we can stabilize it and put some sugar/coercions in?

Johan Commelin (May 15 2020 at 03:44):

Yes, there seems to be room for improvement. But I don't see a good way forward atm that is also aesthetically pleasing :wink:

Johan Commelin (May 15 2020 at 03:45):

One solution is: do as much as possible for a generic ring hom f : R →+* S (possibly with hypothesis hf : injective f). Then everything looks good.

Johan Commelin (May 15 2020 at 03:45):

And then finally, at some point, apply it to int.cast_ring_hom rat. Then you have pushed all the uglyness in one little corner

Johan Commelin (May 15 2020 at 03:46):

So, speaking of #xy, what are your really trying to do? What is your bigger plan/goal.

Jack J Garzella (May 15 2020 at 03:46):

Oh, it's partly Eisenstein's criteron and partly proving that quadratic extensions are normal, though both need this type of thing

Johan Commelin (May 15 2020 at 03:47):

But neither need int?

Jack J Garzella (May 15 2020 at 03:49):

I am using int in my first example, but no, neither need int. I think the question I was asking was "what is the right way to do this for an arbitrary subring/injective hom?"

Johan Commelin (May 15 2020 at 03:49):

And for Eisenstein, it will probably be easier to go for https://en.wikipedia.org/wiki/Eisenstein%27s_criterion#Generalized_criterion

Jack J Garzella (May 15 2020 at 03:49):

Yes, I'm using that. It would be nice maybe to have a specialized "corollary" version of Eisenstein that has int and rat though

Johan Commelin (May 15 2020 at 03:50):

It turns out that with these sort of questions, the general case is often easier. Because you don't run into all these nasty issues with the specifics of int and rat

Johan Commelin (May 15 2020 at 03:50):

Yup, the specialisation can come afterwards, I agree

Jack J Garzella (May 15 2020 at 03:52):

But it would be nice, for example, to be able to say something like "this polynomial in $R[X]$ irreducible over the field of fractions" where the "over the field of fractions" has the injective ring hom tied into it and some polynomial coercion

Jack J Garzella (May 15 2020 at 03:54):

There's also a hiccup here in that when a mathematician thinks "I want to think about a polynomial over $R$ as one in bigger ring $S$", the first place they will look in the library is the subring structure--at the very least, I would like to write documentation showing that one should really think about the ring hom

Johan Commelin (May 15 2020 at 03:54):

But the field of fractions of int is not defeq to rat...

Johan Commelin (May 15 2020 at 03:55):

So you want to say K is a field of fractions of R, and hence...

Johan Commelin (May 15 2020 at 03:56):

There's a sequence of PRs going on about localisation (of monoids/ rings/ etc). That's certainly going to help here.

Johan Commelin (May 15 2020 at 03:56):

Before, we could only speak about "the" localisation. But you want to speak about "a" localisation, unique up to unique iso.

Johan Commelin (May 15 2020 at 03:57):

Field of fractions is of course a special case.

Jack J Garzella (May 15 2020 at 03:58):

ok I see, so probably the thing to do is to be explicit for now

Jack J Garzella (May 15 2020 at 04:00):

It seems based on what you're saying that depending on each special case to the mathematician's idea of an ambient/bigger ring, there might be a different "right way"

Johan Commelin (May 15 2020 at 04:01):

Jack J Garzella said:

ok I see, so probably the thing to do is to be explicit for now

And generalise.... generalise your problems away. (Remember the problems and issues that Patrick wrote about in the perfectoid paper!)

Johan Commelin (May 15 2020 at 04:08):

@Jack J Garzella What is the definition of "normal extension" that you wanted to use?

Jack J Garzella (May 15 2020 at 04:12):

It looks like this

@[class] def normal : Prop :=
∀ x : β, ∃ H : is_integral α x, polynomial.splits (algebra_map α β) (minimal_polynomial H)


I didn't write this though, I'm just using it (I believe this definition is due to @Kenny Lau )

Jack J Garzella (May 15 2020 at 04:13):

Right now I'm working on proving that $\mathbb{Q}[\sqrt{2}]$ is a normal extension (just to get myself familiar), then I'll move on to something slightly more complicated

Johan Commelin (May 15 2020 at 04:14):

Once again, I think you'll find the general case easier then this specific one.

Johan Commelin (May 15 2020 at 04:15):

Is that definition already in mathlib?

Jack J Garzella (May 15 2020 at 04:18):

I'll try out the general case.

Johan Commelin (May 15 2020 at 04:19):

Of course, you would need to think about how you formulate the general case...

Jack J Garzella (May 15 2020 at 04:20):

No, the definition isn't in mathlib, though I believe it may get PR'ed sometime. There's some Galois theory stuff that is on it's way to being PR'ed, but I think algebraic closure is a holdup a bunch of it.

Johan Commelin (May 15 2020 at 04:20):

But I would start with the following lemma: Let f be a polynomial over a ring R, of degree 2. Suppose that x is a root of f. Then f splits.

Mario Carneiro (May 15 2020 at 04:21):

wouldn't any degree above 1 work?

Johan Commelin (May 15 2020 at 04:21):

Mathlib name: polynomial.splits_of_degree_two_of_root

Johan Commelin (May 15 2020 at 04:22):

I think splits means "splits completely"

Johan Commelin (May 15 2020 at 04:22):

But I haven't seen the definition.

Jack J Garzella (May 15 2020 at 04:22):

It does mean "splits completely"

Jack J Garzella (May 15 2020 at 04:23):

it's in splitting_field.lean

Johan Commelin (May 15 2020 at 04:23):

Probably written by some guy called Mario

Johan Commelin (May 15 2020 at 04:24):

Two years ago in a hotel room in Orsay (-;

Mario Carneiro (May 15 2020 at 04:24):

actually, I think I was only tangentially involved in this part of the library. I think Chris and Kenny pulled this through

Jack J Garzella (May 15 2020 at 04:24):

The file says Chris

Chris Hughes (May 15 2020 at 16:49):

I wish I'd defined splits as monoid.closure {f | degree f \le 1}. This is a much more elegant definition.

Mario Carneiro (May 15 2020 at 16:49):

I think it can even be degree f = 1

Kevin Buzzard (May 15 2020 at 16:50):

Arguably a unit splits.

Chris Hughes (May 15 2020 at 16:50):

constant polys split I think. Then everything in an algebraically closed field splits.

Mario Carneiro (May 15 2020 at 16:51):

oh yeah, ignore me

Last updated: May 12 2021 at 06:14 UTC