Minimal polynomial over ℚ vs over ℤ

Stream: maths

[Riccardo Brasca]

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]

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]

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

[Johan Commelin]

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]

Yeah, now that is_scalar_tower exists, we should be able to get rid of the codomain trick.

[Riccardo Brasca]

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

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]

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

[Riccardo Brasca]

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]

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

[Riccardo Brasca]

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]

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]

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

[Reid Barton]

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]

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]

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]

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]

I guess R is redundant, since it's determined by S, but maybe it's nice to include it anyways

[Riccardo Brasca]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

at least, we can start with an ordinary proposition

[Riccardo Brasca]

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

[Reid Barton]

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

[Riccardo Brasca]

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]

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]

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.