# Zulip Chat Archive

## 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`

?

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

Certainly quadratic extensions don't

#### 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