Zulip Chat Archive

Stream: maths

Topic: Minimal polynomial over ℚ vs over ℤ


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

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

view this post on Zulip Johan Commelin (Nov 17 2020 at 14:12):

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

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

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

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

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

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

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

view this post on Zulip Riccardo Brasca (Nov 17 2020 at 17:37):

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

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

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

view this post on Zulip Reid Barton (Nov 28 2020 at 14:33):

I guess is_localization would still be an ordinary proposition and not an instance?

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

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

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

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

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

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

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

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

view this post on Zulip Reid Barton (Nov 28 2020 at 14:45):

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

view this post on Zulip Reid Barton (Nov 28 2020 at 14:45):

at least, we can start with an ordinary proposition

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

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

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

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

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