minpoly of algebraic integers

Stream: Is there code for X?

[Xavier Roblot]

I could not find the following:

import Mathlib

open NumberField

example {K : Type*} [Field K] [NumberField K] (x : 𝓞 K) : minpoly ℤ (x : K) = minpoly ℤ x := by
  sorry

What would be the most efficient way to prove that? and what would be the right generality to state the result?

[Xavier Roblot]

Ok, so one answer to the first question is:

import Mathlib

open NumberField

example {K : Type*} [Field K] [NumberField K] (x : 𝓞 K) : minpoly ℤ (x : K) = minpoly ℤ x := by
  apply Polynomial.map_injective _ <| (algebraMap ℤ ℚ).injective_int
  rw [← minpoly.isIntegrallyClosed_eq_field_fractions' _ x.isIntegral_coe,
    minpoly.isIntegrallyClosed_eq_field_fractions ℚ (L := K) x.isIntegral]

[Riccardo Brasca]

import Mathlib

open NumberField

example {K : Type*} [Field K] [NumberField K] (x : 𝓞 K) : minpoly ℤ (x : K) = minpoly ℤ x :=
  minpoly.algebraMap_eq RingOfIntegers.coe_injective x

[Xavier Roblot]

That's even better

[Riccardo Brasca]

not sure why exact? doesn't find it, probably because there is no algebraMap in your statement

[Xavier Roblot]

Do you think it's worth adding as a (simp) lemma?

[Riccardo Brasca]

Do we often write (x : K)?

[Xavier Roblot]

Well, I have at least one example :sweat_smile: But, I see your point. I'll inline the proof instead.

[Riccardo Brasca]

I mean, we should decide which is the canonical way of turning x into an element of K.

[Xavier Roblot]

I think coercion is the most natural way since we, or at least me, still see 𝓞 K as a subset of K even if it is not anymore.

[Xavier Roblot]

In my case, I needed the result because of docs#IsPrimitiveRoot.coe_toInteger where coercion is used

[Riccardo Brasca]

Yeah, I see there no simp normal form here. Anyway the minimal polynomial is so ubiquitous that having your lemma is probably fine.

[Xavier Roblot]

Ok, I'll add in the PR where I need it. Thanks!

[Kenny Lau]

Riccardo Brasca said:

there is no algebraMap in your statement

this sounds like a tricky situation, we can't probably have 10 lemmas whenever we mention algebraMap

[Kenny Lau]

i mean usually we try to keep algebraMap as the simpNF but that is clearly not the case for Int and Nat which is why actually every lemma does usually have a separate form for Nat.cast and Int.cast...

[Kenny Lau]

which is quite inefficient