# Zulip Chat Archive

## Stream: maths

### Topic: Minimal polynomial over ℚ vs over ℤ

#### Riccardo Brasca (Nov 17 2020 at 13:50):

In #5006 I proved that the minimal polynomial over any GCD domain is the same as the minimal polynomial over its field of fractions. Now I want to use it to say that the minimal polynomial of an algebraic integer, over `ℤ`

, is the same as the minimal polynomial over `ℚ`

. Something like in the following code (there is a `sorry`

in `gcd_domain_eq_field_fractions`

because it needs other results, but in #5006 it is proved. If you are wondering why the `@is_integral...`

is because without that it doesn't work)

```
import field_theory.minimal_polynomial
import ring_theory.localization
import analysis.complex.basic
variables (z : ℂ) (hint : is_integral ℤ z) (halg : is_integral ℚ z)
lemma gcd_domain_eq_field_fractions {α : Type*} {β : Type*} {γ : Type*} [integral_domain α]
[gcd_monoid α] [field β] [integral_domain γ] (f : fraction_map α β) [algebra f.codomain γ]
[algebra α γ] [is_scalar_tower α f.codomain γ] {x : γ} (hx : is_integral α x) : minimal_polynomial
(@is_integral_of_is_scalar_tower α f.codomain γ _ _ _ _ _ _ _ x hx) = ((minimal_polynomial hx).map
(localization_map.to_ring_hom f)) :=
begin
sorry
end
lemma test : polynomial.map (int.cast_ring_hom ℚ) (minimal_polynomial hint) =
minimal_polynomial halg :=
begin
have h := @gcd_domain_eq_field_fractions ℤ ℚ ℂ _ _ _ _
fraction_map.int.fraction_map _ _ _ z hint,
end
```

It seems that the second lemma should be an immediate consequence of the first one, but I am not able to prove it. I want to prove it using `fraction_map.int.fraction_map`

, but Leans complains with

```
failed to synthesize type class instance for
z : ℂ,
hint : is_integral ℤ z,
halg : is_integral ℚ z
⊢ algebra (localization_map.codomain fraction_map.int.fraction_map) ℂ
```

I see that at some point I have to prove some compatibility between `polynomial.map (int.cast_ring_hom ℚ)`

and ```
polynomial.map
(localization_map.to_ring_hom fraction_map.int.fraction_map)
```

but I am stuck before getting to it: I do not know how to say that `localization_map.codomain fraction_map.int.fraction_map`

is`ℚ`

, so we have the required algebra structure on `ℂ`

.

Any help is appreciated, thank you!

#### Anne Baanen (Nov 17 2020 at 14:07):

Does something like this work:

```
lemma test : polynomial.map (int.cast_ring_hom ℚ) (minimal_polynomial hint) =
minimal_polynomial halg :=
begin
letI : algebra (localization_map.codomain fraction_map.int.fraction_map) ℂ :=
show algebra ℚ ℂ, from infer_instance,
have h := @gcd_domain_eq_field_fractions ℤ ℚ ℂ _ _ _ _
fraction_map.int.fraction_map _ _ _ z hint,
end
```

#### Johan Commelin (Nov 17 2020 at 14:12):

I think this might show that we've been using too much bundling for localization maps?

#### Johan Commelin (Nov 17 2020 at 14:13):

If `is_localization`

were a predicate assuming `[algebra R A]`

, then we wouldn't have those `g.codomain`

s that throw sand in the type class inference machine.

#### Anne Baanen (Nov 17 2020 at 14:17):

Yeah, now that `is_scalar_tower`

exists, we should be able to get rid of the `codomain`

trick.

#### Riccardo Brasca (Nov 17 2020 at 14:28):

@Anne Baanen Now it asks to prove `scalar_tower`

, that should follow from `is_scalar_tower.int`

. I am trying to understand what you wrote to prove this.

#### Riccardo Brasca (Nov 17 2020 at 14:40):

I tried with

```
lemma test : polynomial.map (int.cast_ring_hom ℚ) (minimal_polynomial hint) =
minimal_polynomial halg :=
begin
letI : algebra (localization_map.codomain fraction_map.int.fraction_map) ℂ :=
show algebra ℚ ℂ, from infer_instance,
letI : is_scalar_tower ℤ (localization_map.codomain fraction_map.int.fraction_map) ℂ,
{ exact is_scalar_tower.int (localization_map.codomain fraction_map.int.fraction_map) ℂ },
have h := gcd_domain_eq_field_fractions fraction_map.int.fraction_map hint,
end
```

But it says

```
failed to synthesize type class instance for
z : ℂ,
hint : is_integral ℤ z,
halg : is_integral ℚ z,
_inst : algebra (localization_map.codomain fraction_map.int.fraction_map) ℂ :=
show algebra ℚ ℂ, from infer_instance,
_inst_1 : is_scalar_tower ℤ (localization_map.codomain fraction_map.int.fraction_map) ℂ :=
is_scalar_tower.int (localization_map.codomain fraction_map.int.fraction_map) ℂ
⊢ is_scalar_tower ℤ (localization_map.codomain fraction_map.int.fraction_map) ℂ
state:
z : ℂ,
hint : is_integral ℤ z,
halg : is_integral ℚ z,
_inst : algebra (localization_map.codomain fraction_map.int.fraction_map) ℂ :=
show algebra ℚ ℂ, from infer_instance,
_inst_1 : is_scalar_tower ℤ (localization_map.codomain fraction_map.int.fraction_map) ℂ :=
is_scalar_tower.int (localization_map.codomain fraction_map.int.fraction_map) ℂ
⊢ polynomial.map (int.cast_ring_hom ℚ) (minimal_polynomial hint) = minimal_polynomial halg
```

I guess I will just prove it by hand, without using the general result :D

#### Johan Commelin (Nov 17 2020 at 14:58):

@Riccardo Brasca Really, we should try to fix the library so that you can apply the general result in a 1-liner.

#### Riccardo Brasca (Nov 17 2020 at 15:15):

I agree that having a proposition `is_localization`

for an algebra is much more close to what I have in mind, but I don't know how much work it requires.

#### Riccardo Brasca (Nov 17 2020 at 17:37):

By the way, I would be very happy to help in doing this!

#### Riccardo Brasca (Nov 25 2020 at 17:23):

If someone is still interested in this I managed to make it working. This should be useful to at least understand what can be improved in `ring_theory/localization`

.

```
import field_theory.minimal_polynomial
import ring_theory.localization
open polynomial
variables {K : Type*} [field K] [char_zero K]
variables (z : K) (hint : is_integral ℤ z) (halg : is_integral ℚ z)
lemma gcd_domain_eq_field_fractions {α : Type*} {β : Type*} {γ : Type*} [integral_domain α]
[gcd_monoid α] [field β] [integral_domain γ] (f : fraction_map α β) [algebra f.codomain γ]
[algebra α γ] (hto : is_scalar_tower α f.codomain γ) {x : γ} (hx : is_integral α x) :
minimal_polynomial (@is_integral_of_is_scalar_tower α f.codomain γ _ _ _ _ _ _ _ x hx) =
((minimal_polynomial hx).map (localization_map.to_ring_hom f)) :=
begin
sorry
end
lemma test : map (int.cast_ring_hom ℚ) (minimal_polynomial hint) =
minimal_polynomial halg :=
begin
have h₁ : localization_map.to_ring_hom fraction_map.int.fraction_map = int.cast_ring_hom ℚ,
{ refl },
rw ←h₁,
symmetry,
refine gcd_domain_eq_field_fractions fraction_map.int.fraction_map _ hint,
split,
intros x y z,
repeat {rw algebra.smul_def _ _},
simp only [ring_hom.eq_int_cast, ring_hom.map_int_cast, ring_hom.map_mul],
ring
end
```

Note that `is_scalar_tower`

in the first lemma is now an assumption rather than an instance, so I can use `refine`

(I tried all the various `letI`

`haveI`

, but they don't work).

I think that the main problem using the codomain trick is that lean uses `fraction_map.int.fraction_map`

to consider `ℚ`

a `ℤ`

-algebra in the lemma, but use the obvious structure otherwise. This leads to very confusing things to prove, for example at some point I had to prove `(x • y) • z = x • y • z`

and I managed to prove `(x • y) • z = x • y • z`

... except that the `•`

where not the same... and `set_option pp.implicit true`

produced a gigantic practically unreadable output.

Note that the result `localization_map.to_ring_hom fraction_map.int.fraction_map = int.cast_ring_hom ℚ`

and should probably be added, the problem with the algebra structure would not be solved simply by this.

#### Reid Barton (Nov 28 2020 at 14:31):

So what exactly is the suggestion here? Rather than `localization_map`

, we want to say that an `algebra`

instance is a localization? How do we relate it to the set `S`

?

#### Reid Barton (Nov 28 2020 at 14:33):

I guess `is_localization`

would still be an ordinary proposition and not an instance?

#### Reid Barton (Nov 28 2020 at 14:36):

In the non-additive setting, we still have `is_scalar_tower`

but nothing like `algebra`

I guess. Also, `localization_map`

makes sense even for `R`

(and `S`

) noncommutative but we don't have `algebra`

in that situation either.

#### Riccardo Brasca (Nov 28 2020 at 14:37):

I think we should refactor `localization`

in such a way that `is_localization`

is a proposition for an `algebra`

. If you look in the source code there is this trick with `codomain`

that I don't understand completely. I am thinking about it, but it is the first time I try to do something like that (instead of proving a "normal" theorem), so I am (very) slow and I would appreciate any suggestion :)

#### Reid Barton (Nov 28 2020 at 14:38):

I've been (also very slowly) working on generalizing localization to Ore localization and handling localization of modules, so this will intersect what I'm doing at some point.

#### Reid Barton (Nov 28 2020 at 14:40):

It seems like we can write something like `is_localization R A S : Prop`

to mean that `algebra_map`

from `R`

to `A`

can be made into a `localization_map`

at `S`

, right?

#### Reid Barton (Nov 28 2020 at 14:41):

I guess `R`

is redundant, since it's determined by `S`

, but maybe it's nice to include it anyways

#### Riccardo Brasca (Nov 28 2020 at 14:43):

I am still in the process of reading the source code (that also use localization for monoids) to decide what to do.

#### Reid Barton (Nov 28 2020 at 14:43):

Currently `localization_map`

extends `ring_hom`

by some propositional fields, so we could split those propositional fields into a new `is_localization_map`

and define `is_localization`

for algebras by applying that to `algebra_map`

#### Riccardo Brasca (Nov 28 2020 at 14:44):

I think at the end what we need is something like a proposition`is_localization (R A M: Type*) [comm_ring R] [comm_ring A] [algebra R A] (M : submonoid R)`

#### Reid Barton (Nov 28 2020 at 14:45):

And just an ordinary proposition, not a class, right?

#### Reid Barton (Nov 28 2020 at 14:45):

at least, we can start with an ordinary proposition

#### Riccardo Brasca (Nov 28 2020 at 14:45):

To be honest I have no idea about this kind of details, my plan was to ask here :D

#### Reid Barton (Nov 28 2020 at 14:46):

For special cases like "is the fraction field of", maybe it makes sense to have a class

#### Riccardo Brasca (Nov 28 2020 at 15:00):

Defining the proposition is really easy, as you said it suffices to use `algebra_map`

. It is the part of working with classes/structures/instances that scares me a little bit.

#### Johan Commelin (Nov 28 2020 at 16:00):

It might make sense to do this for `ring_hom`

instead of `algebra_map`

. (I'm maybe still too biased towards comm. algebra)

#### Riccardo Brasca (Nov 28 2020 at 16:52):

You mean defining `is_localization (R A M: Type*) [comm_ring R] [comm_ring A] (M : submonoid R) (f : R →+* S)`

? This is exactly the kind of questions I have no idea how to answer, in my head this and `is_localization (R A M: Type*) [comm_ring R] [comm_ring A] [algebra R A] (M : submonoid R)`

are exactly the same thing.

Last updated: May 12 2021 at 08:14 UTC