Zulip Chat Archive

Stream: maths

Topic: of_subring as a coercion


view this post on Zulip Jack J Garzella (May 15 2020 at 02:55):

It would sure be nice for to have polynomials in Z[X]\mathbb{Z}[X] automatically coerce to polynomials in Q[X]\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)?

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

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

view this post on Zulip Johan Commelin (May 15 2020 at 03:41):

If you use bundled homs, that problem completely vanishes.

view this post on Zulip Johan Commelin (May 15 2020 at 03:41):

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

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

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

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

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

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

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

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

view this post on Zulip Johan Commelin (May 15 2020 at 03:47):

But neither need int?

view this post on Zulip Johan Commelin (May 15 2020 at 03:47):

Certainly quadratic extensions don't

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

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

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

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

view this post on Zulip Johan Commelin (May 15 2020 at 03:50):

Yup, the specialisation can come afterwards, I agree

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

view this post on Zulip 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 RR as one in bigger ring SS", 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

view this post on Zulip Johan Commelin (May 15 2020 at 03:54):

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

view this post on Zulip Johan Commelin (May 15 2020 at 03:55):

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

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

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

view this post on Zulip Johan Commelin (May 15 2020 at 03:57):

Field of fractions is of course a special case.

view this post on Zulip Jack J Garzella (May 15 2020 at 03:58):

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

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

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

view this post on Zulip Johan Commelin (May 15 2020 at 04:08):

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

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

view this post on Zulip Jack J Garzella (May 15 2020 at 04:13):

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

view this post on Zulip Johan Commelin (May 15 2020 at 04:14):

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

view this post on Zulip Johan Commelin (May 15 2020 at 04:15):

Is that definition already in mathlib?

view this post on Zulip Jack J Garzella (May 15 2020 at 04:18):

I'll try out the general case.

view this post on Zulip Johan Commelin (May 15 2020 at 04:19):

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

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

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

view this post on Zulip Mario Carneiro (May 15 2020 at 04:21):

wouldn't any degree above 1 work?

view this post on Zulip Johan Commelin (May 15 2020 at 04:21):

Mathlib name: polynomial.splits_of_degree_two_of_root

view this post on Zulip Johan Commelin (May 15 2020 at 04:22):

I think splits means "splits completely"

view this post on Zulip Johan Commelin (May 15 2020 at 04:22):

But I haven't seen the definition.

view this post on Zulip Jack J Garzella (May 15 2020 at 04:22):

It does mean "splits completely"

view this post on Zulip Jack J Garzella (May 15 2020 at 04:23):

it's in splitting_field.lean

view this post on Zulip Johan Commelin (May 15 2020 at 04:23):

Probably written by some guy called Mario

view this post on Zulip Johan Commelin (May 15 2020 at 04:24):

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

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

view this post on Zulip Jack J Garzella (May 15 2020 at 04:24):

The file says Chris

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

view this post on Zulip Mario Carneiro (May 15 2020 at 16:49):

I think it can even be degree f = 1

view this post on Zulip Kevin Buzzard (May 15 2020 at 16:50):

Arguably a unit splits.

view this post on Zulip Chris Hughes (May 15 2020 at 16:50):

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

view this post on Zulip Mario Carneiro (May 15 2020 at 16:51):

oh yeah, ignore me


Last updated: May 12 2021 at 06:14 UTC