of_subring as a coercion

Stream: maths

[Jack J Garzella]

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]

@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]

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]

If you use bundled homs, that problem completely vanishes.

[Johan Commelin]

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

[Jack J Garzella]

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]

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]

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]

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]

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]

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

[Jack J Garzella]

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

[Johan Commelin]

But neither need int?

[Johan Commelin]

Certainly quadratic extensions don't

[Jack J Garzella]

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]

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

[Jack J Garzella]

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]

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]

Yup, the specialisation can come afterwards, I agree

[Jack J Garzella]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

Field of fractions is of course a special case.

[Jack J Garzella]

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

[Jack J Garzella]

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]

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]

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

[Jack J Garzella]

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]

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]

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

[Johan Commelin]

Is that definition already in mathlib?

[Jack J Garzella]

I'll try out the general case.

[Johan Commelin]

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

[Jack J Garzella]

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]

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]

wouldn't any degree above 1 work?

[Johan Commelin]

Mathlib name: polynomial.splits_of_degree_two_of_root

[Johan Commelin]

I think splits means "splits completely"

[Johan Commelin]

But I haven't seen the definition.

[Jack J Garzella]

It does mean "splits completely"

[Jack J Garzella]

it's in splitting_field.lean

[Johan Commelin]

Probably written by some guy called Mario

[Johan Commelin]

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

[Mario Carneiro]

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]

The file says Chris

[Chris Hughes]

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

[Mario Carneiro]

I think it can even be degree f = 1

[Kevin Buzzard]

Arguably a unit splits.

[Chris Hughes]

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

[Mario Carneiro]

oh yeah, ignore me