Minimal polynomials of algebraic integers

An algebraic integer x of a number field K has a minimal polynomial over ℤ, as an element of 𝓞 K, and a minimal polynomial over ℚ, as an element of K. Since ℤ is integrally closed, the second is the first with its coefficients cast to ℚ.

Main results

• NumberField.RingOfIntegers.minpoly_rat_coe: minpoly ℚ (x : K) = (minpoly ℤ x).map (algebraMap ℤ ℚ).
• TauCeti.NumberField.minpoly_rat_eq_of_mem_rootSet: a root in a commutative domain over ℚ has the same minimal polynomial over ℚ as x.
• TauCeti.NumberField.minpoly_two_mul_sub_one_of_minpoly_eq_X_sq_sub_X_add: an algebraic integer ω with minimal polynomial X² - X + c has 2ω - 1 with minimal polynomial X² - (1 - 4c).
• TauCeti.NumberField.minpoly_int_eq_of_coe_mem_rootSet: an algebraic integer in another number field that is a root has the same minimal polynomial over ℤ as x.

theorem NumberField.RingOfIntegers.minpoly_rat_coe {K : Type u_1} [Field K] [NumberField K] (x : RingOfIntegers K) : minpoly ℚ ↑x = Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ x)

The minimal polynomial over ℚ of an algebraic integer x, viewed in K, is its minimal polynomial over ℤ with the coefficients cast to ℚ.

theorem TauCeti.NumberField.aeval_minpoly_int_eq_zero_of_mem_rootSet {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {M : Type u_2} [CommRing M] [IsDomain M] [Algebra ℚ M] {β : M} (hβ : β ∈ (minpoly ℚ ↑θ).rootSet M) : (Polynomial.aeval β) (minpoly ℤ θ) = 0

A root in M of minpoly ℚ θ is a root of minpoly ℤ θ.

theorem TauCeti.NumberField.isIntegral_of_mem_rootSet {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {M : Type u_2} [CommRing M] [IsDomain M] [Algebra ℚ M] {β : M} (hβ : β ∈ (minpoly ℚ ↑θ).rootSet M) : IsIntegral ℤ β

A root in M of minpoly ℚ θ is an algebraic integer.

theorem TauCeti.NumberField.minpoly_rat_eq_of_mem_rootSet {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {M : Type u_2} [CommRing M] [IsDomain M] [Algebra ℚ M] {β : M} (hβ : β ∈ (minpoly ℚ ↑θ).rootSet M) : minpoly ℚ β = minpoly ℚ ↑θ

A root in M of minpoly ℚ θ has that polynomial as its minimal polynomial over ℚ.

theorem TauCeti.NumberField.minpoly_int_eq_of_coe_mem_rootSet {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {M : Type u_2} [Field M] [NumberField M] {β : NumberField.RingOfIntegers M} (hβ : ↑β ∈ (minpoly ℚ ↑θ).rootSet M) : minpoly ℤ β = minpoly ℤ θ

An algebraic integer of a number field M that is a root of minpoly ℚ θ has the same minimal polynomial over ℤ as θ.

theorem TauCeti.NumberField.minpoly_two_mul_sub_one_of_minpoly_eq_X_sq_sub_X_add {K : Type u_1} [Field K] [NumberField K] {ω : NumberField.RingOfIntegers K} {c : ℤ} (hmin : minpoly ℤ ω = Polynomial.X ^ 2 - Polynomial.X + Polynomial.C c) : minpoly ℤ (2 * ω - 1) = Polynomial.X ^ 2 - Polynomial.C (1 - 4 * c)

For an algebraic integer ω with minimal polynomial X² - X + c over ℤ, the element 2ω - 1 is a square root of 1 - 4c: its minimal polynomial over ℤ is X² - (1 - 4c). This converts the half-integer presentation of a quadratic field back into the radicand presentation.