The primitive minimal polynomial over ℤ

For an element x of a division ring F of characteristic zero (typically a field), the primitive minimal polynomial F_x = primitiveMinpoly x ∈ ℤ[X] is obtained from minpoly ℚ x by clearing denominators and dividing by the content, with the sign chosen so that the leading coefficient a₀ is positive. For algebraic x it is the unique primitive irreducible integer polynomial with positive leading coefficient vanishing at x, and its image in ℚ[X] is a₀ • minpoly ℚ x. When x is transcendental over ℚ the junk value is 1.

This is the polynomial from which the classical size invariants of an algebraic number are read off: its naive height is the largest absolute value of a coefficient of F_x, and its Mahler measure is the Mahler measure of F_x. Unlike minpoly ℤ x, which vanishes at non-integral algebraic numbers, F_x is meaningful for every algebraic x, and its leading coefficient clears the denominator of x when F is a field.

Main definitions

• TauCeti.primitiveMinpoly x: the primitive minimal polynomial F_x ∈ ℤ[X] of x.

Main results

• TauCeti.map_primitiveMinpoly, TauCeti.coeff_primitiveMinpoly: the image of F_x in ℚ[X] is a₀ • minpoly ℚ x, so the n-th coefficient of F_x is a₀ times that of minpoly ℚ x.
• TauCeti.isPrimitive_primitiveMinpoly, TauCeti.leadingCoeff_primitiveMinpoly_pos, TauCeti.irreducible_primitiveMinpoly, TauCeti.aeval_primitiveMinpoly: F_x is primitive, has positive leading coefficient, and for algebraic x is irreducible and vanishes at x.
• TauCeti.rootSet_primitiveMinpoly: F_x and minpoly ℚ x have the same roots in every commutative domain that is a ℚ-algebra.
• TauCeti.primitiveMinpoly_dvd_iff: for algebraic x, F_x ∣ P in ℤ[X] iff P(x) = 0.
• TauCeti.primitiveMinpoly_eq_of_irreducible: the uniqueness characterisation of F_x.
• TauCeti.primitiveMinpoly_eq_minpoly_int: F_x = minpoly ℤ x for x integral over ℤ.
• TauCeti.primitiveMinpoly_ratCast: F_q = (den q) X - num q for q ∈ ℚ.
• TauCeti.primitiveMinpoly_map, TauCeti.primitiveMinpoly_eq_of_minpoly_eq: F_x depends only on minpoly ℚ x, so it is preserved by ring homomorphisms between division rings of characteristic zero (such as field embeddings) and shared by conjugates.
• TauCeti.coeff_zero_primitiveMinpoly_ne_zero: for nonzero x, the constant coefficient of F_x is nonzero.
• TauCeti.isIntegral_leadingCoeff_primitiveMinpoly_smul, TauCeti.natDenominator_dvd_leadingCoeff_primitiveMinpoly, TauCeti.leadingCoeff_primitiveMinpoly_le_natDenominator_pow: a₀ x is an algebraic integer, so in fields the denominator of x divides a₀, and conversely a₀ is at most the d-th power of the denominator.
• TauCeti.natDegree_minpoly_int_natDenominator_smul: in fields, D x for the denominator D of x has the same degree over ℤ as x has over ℚ.

References

• J.-H. Evertse, Diophantine Approximation, lecture notes (2019), ch. 3, §3.1 and Lemma 3.7; ch. 6, §6.1.

noncomputable def TauCeti.primitiveMinpoly {F : Type u_1} [DivisionRing F] [CharZero F] (x : F) : Polynomial ℤ

The primitive minimal polynomial F_x ∈ ℤ[X] of x over ℚ: the primitive integer multiple of minpoly ℚ x with positive leading coefficient. It is obtained by clearing the denominators of minpoly ℚ x, taking the primitive part and normalizing the sign.

For x transcendental over ℚ, minpoly ℚ x = 0 and the value is 1 (primitiveMinpoly_of_not_isAlgebraic).

theorem TauCeti.primitiveMinpoly_eq_of_minpoly_eq {F : Type u_1} [DivisionRing F] [CharZero F] {F' : Type u_2} [DivisionRing F'] [CharZero F'] {x : F} {y : F'} (h : minpoly ℚ x = minpoly ℚ y) : primitiveMinpoly x = primitiveMinpoly y

F_x depends only on minpoly ℚ x: elements with the same minimal polynomial over ℚ, for instance conjugates, possibly lying in different division rings, share their primitive minimal polynomial.

@[simp]

theorem TauCeti.primitiveMinpoly_map {F : Type u_1} [DivisionRing F] [CharZero F] {F' : Type u_2} [DivisionRing F'] [CharZero F'] (f : F →+* F') (x : F) : primitiveMinpoly (f x) = primitiveMinpoly x

Ring homomorphisms between division rings (for instance field embeddings) preserve the primitive minimal polynomial.

@[simp]

theorem TauCeti.primitiveMinpoly_of_not_isAlgebraic {F : Type u_1} [DivisionRing F] [CharZero F] {x : F} (hx : ¬IsAlgebraic ℚ x) : primitiveMinpoly x = 1

The junk value: F_x = 1 for x transcendental over ℚ.

theorem TauCeti.isPrimitive_primitiveMinpoly {F : Type u_1} [DivisionRing F] [CharZero F] (x : F) : (primitiveMinpoly x).IsPrimitive

The primitive minimal polynomial is primitive.

@[simp]

theorem TauCeti.primitiveMinpoly_ne_zero {F : Type u_1} [DivisionRing F] [CharZero F] (x : F) : primitiveMinpoly x ≠ 0

The primitive minimal polynomial is nonzero, also for transcendental x.

theorem TauCeti.leadingCoeff_primitiveMinpoly_pos {F : Type u_1} [DivisionRing F] [CharZero F] (x : F) : 0 < (primitiveMinpoly x).leadingCoeff

The leading coefficient a₀ of the primitive minimal polynomial is positive.

theorem TauCeti.map_primitiveMinpoly {F : Type u_1} [DivisionRing F] [CharZero F] {x : F} (hx : IsAlgebraic ℚ x) : Polynomial.map (Int.castRingHom ℚ) (primitiveMinpoly x) = Polynomial.C ↑(primitiveMinpoly x).leadingCoeff * minpoly ℚ x

For algebraic x, the image of F_x in ℚ[X] is a₀ • minpoly ℚ x, where a₀ is the leading coefficient of F_x.

theorem TauCeti.coeff_primitiveMinpoly {F : Type u_1} [DivisionRing F] [CharZero F] {x : F} (hx : IsAlgebraic ℚ x) (n : ℕ) : ↑((primitiveMinpoly x).coeff n) = ↑(primitiveMinpoly x).leadingCoeff * (minpoly ℚ x).coeff n

For algebraic x, the coefficients of F_x are those of minpoly ℚ x scaled by the leading coefficient a₀ of F_x.

@[simp]

theorem TauCeti.aeval_primitiveMinpoly {F : Type u_1} [DivisionRing F] [CharZero F] {x : F} (hx : IsAlgebraic ℚ x) : (Polynomial.aeval x) (primitiveMinpoly x) = 0

For algebraic x, the primitive minimal polynomial vanishes at x.

theorem TauCeti.coeff_zero_primitiveMinpoly_ne_zero {F : Type u_1} [DivisionRing F] [CharZero F] {x : F} (hx0 : x ≠ 0) : (primitiveMinpoly x).coeff 0 ≠ 0

For nonzero x, the constant coefficient of the primitive minimal polynomial is nonzero. For transcendental x the primitive minimal polynomial is the junk value 1.

@[simp]

theorem TauCeti.rootSet_primitiveMinpoly {F : Type u_1} [DivisionRing F] [CharZero F] (x : F) (K : Type u_3) [CommRing K] [IsDomain K] [Algebra ℚ K] : (primitiveMinpoly x).rootSet K = (minpoly ℚ x).rootSet K

The primitive minimal polynomial has the same roots as minpoly ℚ x in every commutative domain that is a ℚ-algebra: for algebraic x its image in ℚ[X] is a nonzero multiple of minpoly ℚ x, and for transcendental x both root sets are empty.

@[simp]

theorem TauCeti.natDegree_primitiveMinpoly {F : Type u_1} [DivisionRing F] [CharZero F] (x : F) : (primitiveMinpoly x).natDegree = (minpoly ℚ x).natDegree

The primitive minimal polynomial has the degree of x over ℚ. For transcendental x both sides are 0.

theorem TauCeti.irreducible_primitiveMinpoly {F : Type u_1} [DivisionRing F] [CharZero F] {x : F} (hx : IsAlgebraic ℚ x) : Irreducible (primitiveMinpoly x)

For algebraic x, the primitive minimal polynomial is irreducible in ℤ[X].

theorem TauCeti.primitiveMinpoly_dvd_iff {F : Type u_1} [DivisionRing F] [CharZero F] {x : F} (hx : IsAlgebraic ℚ x) {P : Polynomial ℤ} : primitiveMinpoly x ∣ P ↔ (Polynomial.aeval x) P = 0

For algebraic x, the integer polynomials vanishing at x are exactly the multiples of F_x in ℤ[X].

theorem TauCeti.minpoly_eq_of_aeval_primitiveMinpoly_eq_zero {F : Type u_1} [DivisionRing F] [CharZero F] {F' : Type u_2} [DivisionRing F'] [CharZero F'] {x : F} {y : F'} (h : (Polynomial.aeval y) (primitiveMinpoly x) = 0) : minpoly ℚ x = minpoly ℚ y

If the primitive minimal polynomial of x vanishes at y, possibly in another division ring, then x and y are conjugate: they have the same minimal polynomial over ℚ. (For transcendental x the hypothesis is never satisfied.)

theorem TauCeti.primitiveMinpoly_inv_dvd_reverse {F : Type u_1} [DivisionRing F] [CharZero F] {x : F} (hx0 : x ≠ 0) : primitiveMinpoly x⁻¹ ∣ (primitiveMinpoly x).reverse

Reversing a primitive defining polynomial gives a multiple of the primitive minimal polynomial of the inverse root. For transcendental x the latter is the junk value 1.

theorem TauCeti.primitiveMinpoly_eq_of_irreducible {F : Type u_1} [DivisionRing F] [CharZero F] {x : F} {P : Polynomial ℤ} (hirr : Irreducible P) (hlc : 0 < P.leadingCoeff) (hPx : (Polynomial.aeval x) P = 0) : primitiveMinpoly x = P

The uniqueness characterisation: an irreducible P ∈ ℤ[X] with positive leading coefficient vanishing at x is the primitive minimal polynomial of x. Such a P is automatically nonconstant, hence primitive.

theorem TauCeti.primitiveMinpoly_eq_minpoly_int {F : Type u_1} [DivisionRing F] [CharZero F] {x : F} (hx : IsIntegral ℤ x) : primitiveMinpoly x = minpoly ℤ x

For x integral over ℤ, the primitive minimal polynomial is the minimal polynomial over ℤ.

@[simp]

theorem TauCeti.primitiveMinpoly_ratCast {F : Type u_1} [DivisionRing F] [CharZero F] (q : ℚ) : primitiveMinpoly ↑q = Polynomial.C ↑q.den * Polynomial.X - Polynomial.C q.num

The primitive minimal polynomial of a rational number q is (den q) X - num q.

theorem TauCeti.isIntegral_leadingCoeff_primitiveMinpoly_smul {F : Type u_1} [DivisionRing F] [CharZero F] {x : F} (hx : IsAlgebraic ℚ x) : IsIntegral ℤ ((primitiveMinpoly x).leadingCoeff • x)

For algebraic x, the element a₀ x is integral over ℤ, where a₀ is the leading coefficient of F_x (Evertse, Lemma 3.7).

theorem TauCeti.natDenominator_dvd_leadingCoeff_primitiveMinpoly {K : Type u_3} [Field K] [CharZero K] {x : K} (hx : IsAlgebraic ℚ x) : ↑(Algebra.natDenominator x) ∣ (primitiveMinpoly x).leadingCoeff

For algebraic x, the denominator of x divides the leading coefficient of F_x.

theorem TauCeti.natDegree_minpoly_int_natDenominator_smul {K : Type u_3} [Field K] [CharZero K] {x : K} (hx : IsAlgebraic ℚ x) : (minpoly ℤ (Algebra.natDenominator x • x)).natDegree = (minpoly ℚ x).natDegree

For algebraic x, the integral multiple D x of x by its denominator D has the same degree over ℤ as x has over ℚ: it generates the same field.

theorem TauCeti.leadingCoeff_primitiveMinpoly_le_natDenominator_pow {K : Type u_3} [Field K] [CharZero K] (x : K) : (primitiveMinpoly x).leadingCoeff ≤ ↑(Algebra.natDenominator x) ^ (minpoly ℚ x).natDegree

The leading coefficient of F_x is at most D ^ d, where D is the denominator of x and d its degree. Together with natDenominator_dvd_leadingCoeff_primitiveMinpoly, which gives D ≤ a₀ for algebraic x, this bounds a₀ between D and D ^ d. For transcendental x, F_x = 1 and d = 0.

Examples