intMinpoly

Stream: mathlib4

[Fabrizio Barroero]

In Number Theory it is sometimes useful to talk about the minimal polynomial of an algebraic number x over $\mathbb{Z}$, that is, the unique irreducible primitive polynomial in $\mathbb{Z}[X]$ that has positive leading coefficient and vanishes at x. Let's call it intMinpoly x.
In Mathlib we have minpoly A x which the usual definition of minimal polynomial and works for any CommRing A.
Now, intMinpoly x can easily be obtained multiplying minpoly ℚ x by the lcm of the denominators of its coefficients.
Here is my attempt of formalizing this:

import Mathlib

namespace Polynomial

open Int

def lcmDen (p : ℚ[X]) : ℕ := p.support.lcm fun i ↦ (p.coeff i).den

def eraseDen (p : ℚ[X]) : ℤ[X] :=
  ofFn (p.natDegree + 1) (fun i ↦ (p.lcmDen) / (p.coeff i).den * (p.coeff i).num)

end Polynomial

namespace NumberField

variable {K : Type*} [Field K] [Algebra ℚ K]

open Polynomial

noncomputable def intMinpoly (x : K) : ℤ[X] := eraseDen (minpoly ℚ x)

end NumberField

I am not sure if this can be done in higher generality.
Any thoughts?

[Michael Stoll]

One could do that in principle for fields of fractions of UFDs (although one would probably need a normalization for the lcm), but I think doing this over the integers is at least a good start.
The main thing is to state and prove the defining properties:

• x is a root
• the polynomial is primitive (i.e., the coefficients generate the unit ideal)
• the leading coefficient is positive

And then something that is very relevant is to show that (assuming x generates K) the height of x equals the Mahler measure of its intMinpoly.

[Fabrizio Barroero]

Thanks for the feedback! :grinning:
Some time ago I tried to work in that generality but it was a bit painful and I wasn't sure doing so was useful enough to justify the pain.
I have already proofs of some of the things you are suggesting and I am working on the others.
As you probably imagine, relating the height of x with the Mahler measure of its intMinpoly is what motivated this definition.

[Junyan Xu]

The correct generality is probably NormalizedGCDMonoid (weaker than UFD); Finset.lcm that you use is defined for exactly them

[Fabrizio Barroero]

Here is a proposal for a general definition

import Mathlib

variable {R K : Type*} [DecidableEq R] [CommSemiring R] [CommMonoidWithZero R] [IsCancelMulZero R]
[NormalizedGCDMonoid R] [IsDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [DecidableEq K]

namespace Finset

variable (s : Finset K)

variable (R) in
noncomputable def lcmDen : R := s.lcm (fun x ↦
  let q := (IsLocalization.sec (nonZeroDivisors R) x)
  Classical.choose (GCDMonoid.gcd_dvd_right q.1 q.2))

I managed to prove

theorem foo (s : Finset ℚ) : s.lcmDen ℤ = s.lcm (fun x ↦ (x.den : ℤ))

but it was extremely painful. I am not really sure it is worth working is such generality.

[Justus Springer]

Note that we have docs#IsLocalization.integerNormalization. Does that give you what you want directly?

[Justus Springer]

Also, I have #34877 open, which changes the API slightly

[Fabrizio Barroero]

Thanks! I didn't know we had this. I think this only clears denominators in a way that works for any commutative rings and localizations. If one has GCDs then one can do it in a "minimal" way.
I guess one could take this and then its Polynomial.primPart.
I'm going to explore this road, thanks!