## 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.codomains 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 propositionis_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: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