mathlib documentation

field_theory.minpoly

Minimal polynomials #

This file defines the minimal polynomial of an element x of an A-algebra B, under the assumption that x is integral over A.

After stating the defining property we specialize to the setting of field extensions and derive some well-known properties, amongst which the fact that minimal polynomials are irreducible, and uniquely determined by their defining property.

def minpoly (A : Type u_1) {B : Type u_2} [comm_ring A] [ring B] [algebra A B] (x : B) :

Let B be an A-algebra, and x an element of B that is integral over A so we have some term hx : is_integral A x. The minimal polynomial minpoly A x of x is a monic polynomial of smallest degree that has x as its root. For instance, if V is a K-vector space for some field K, and f : V →ₗ[K] V then the minimal polynomial of f is minpoly f.is_integral.

Equations
theorem minpoly.monic {A : Type u_1} {B : Type u_2} [comm_ring A] [ring B] [algebra A B] {x : B} (hx : is_integral A x) :

A minimal polynomial is monic.

theorem minpoly.ne_zero {A : Type u_1} {B : Type u_2} [comm_ring A] [ring B] [algebra A B] {x : B} [nontrivial A] (hx : is_integral A x) :
minpoly A x 0

A minimal polynomial is nonzero.

theorem minpoly.eq_zero {A : Type u_1} {B : Type u_2} [comm_ring A] [ring B] [algebra A B] {x : B} (hx : ¬is_integral A x) :
minpoly A x = 0
@[simp]
theorem minpoly.aeval (A : Type u_1) {B : Type u_2} [comm_ring A] [ring B] [algebra A B] (x : B) :

An element is a root of its minimal polynomial.

theorem minpoly.mem_range_of_degree_eq_one (A : Type u_1) {B : Type u_2} [comm_ring A] [ring B] [algebra A B] (x : B) (hx : (minpoly A x).degree = 1) :
theorem minpoly.min (A : Type u_1) {B : Type u_2} [comm_ring A] [ring B] [algebra A B] (x : B) {p : polynomial A} (pmonic : p.monic) (hp : (polynomial.aeval x) p = 0) :

The defining property of the minimal polynomial of an element x: it is the monic polynomial with smallest degree that has x as its root.

theorem minpoly.degree_le_of_monic (A : Type u_1) {B : Type u_2} [comm_ring A] [ring B] [algebra A B] (x : B) {p : polynomial A} (hmonic : p.monic) (hp : (polynomial.aeval x) p = 0) :

If an element x is a root of a nonzero monic polynomial p, then the degree of p is at least the degree of the minimal polynomial of x.

theorem minpoly.nat_degree_pos {A : Type u_1} {B : Type u_2} [integral_domain A] [ring B] [algebra A B] [nontrivial B] {x : B} (hx : is_integral A x) :

The degree of a minimal polynomial, as a natural number, is positive.

theorem minpoly.degree_pos {A : Type u_1} {B : Type u_2} [integral_domain A] [ring B] [algebra A B] [nontrivial B] {x : B} (hx : is_integral A x) :
0 < (minpoly A x).degree

The degree of a minimal polynomial is positive.

theorem minpoly.eq_X_sub_C_of_algebra_map_inj {A : Type u_1} {B : Type u_2} [integral_domain A] [ring B] [algebra A B] [nontrivial B] [nontrivial A] (a : A) (hf : function.injective (algebra_map A B)) :

If B/A is an injective ring extension, and a is an element of A, then the minimal polynomial of algebra_map A B a is X - C a.

theorem minpoly.not_is_unit (A : Type u_1) {B : Type u_2} [integral_domain A] [ring B] [algebra A B] [nontrivial B] (x : B) :

A minimal polynomial is not a unit.

theorem minpoly.aeval_ne_zero_of_dvd_not_unit_minpoly {A : Type u_1} {B : Type u_2} [integral_domain A] [domain B] [algebra A B] {x : B} {a : polynomial A} (hx : is_integral A x) (hamonic : a.monic) (hdvd : dvd_not_unit a (minpoly A x)) :

If a strictly divides the minimal polynomial of x, then x cannot be a root for a.

theorem minpoly.irreducible {A : Type u_1} {B : Type u_2} [integral_domain A] [domain B] [algebra A B] {x : B} (hx : is_integral A x) :

A minimal polynomial is irreducible.

theorem minpoly.degree_le_of_ne_zero (A : Type u_1) {B : Type u_2} [field A] [ring B] [algebra A B] (x : B) {p : polynomial A} (pnz : p 0) (hp : (polynomial.aeval x) p = 0) :

If an element x is a root of a nonzero polynomial p, then the degree of p is at least the degree of the minimal polynomial of x.

theorem minpoly.unique (A : Type u_1) {B : Type u_2} [field A] [ring B] [algebra A B] (x : B) {p : polynomial A} (pmonic : p.monic) (hp : (polynomial.aeval x) p = 0) (pmin : ∀ (q : polynomial A), q.monic(polynomial.aeval x) q = 0p.degree q.degree) :
p = minpoly A x

The minimal polynomial of an element x is uniquely characterized by its defining property: if there is another monic polynomial of minimal degree that has x as a root, then this polynomial is equal to the minimal polynomial of x.

theorem minpoly.dvd (A : Type u_1) {B : Type u_2} [field A] [ring B] [algebra A B] (x : B) {p : polynomial A} (hp : (polynomial.aeval x) p = 0) :
minpoly A x p

If an element x is a root of a polynomial p, then the minimal polynomial of x divides p.

theorem minpoly.dvd_map_of_is_scalar_tower (A : Type u_1) (K : Type u_2) {R : Type u_3} [comm_ring A] [field K] [comm_ring R] [algebra A K] [algebra A R] [algebra K R] [is_scalar_tower A K R] (x : R) :
theorem minpoly.unique' {A : Type u_1} {B : Type u_2} [field A] [ring B] [algebra A B] {x : B} [nontrivial B] {p : polynomial A} (hx : is_integral A x) (hp1 : irreducible p) (hp2 : (polynomial.aeval x) p = 0) (hp3 : p.monic) :
p = minpoly A x
theorem minpoly.eq_of_algebra_map_eq {K : Type u_1} {S : Type u_2} {T : Type u_3} [field K] [comm_ring S] [comm_ring T] [algebra K S] [algebra K T] [algebra S T] [is_scalar_tower K S T] (hST : function.injective (algebra_map S T)) {x : S} {y : T} (hx : is_integral K x) (h : y = (algebra_map S T) x) :
minpoly K x = minpoly K y

If y is the image of x in an extension, their minimal polynomials coincide.

We take h : y = algebra_map L T x as an argument because rw h typically fails since is_integral R y depends on y.

For GCD domains, the minimal polynomial over the ring is the same as the minimal polynomial over the fraction field.

theorem minpoly.over_int_eq_over_rat {A : Type u_1} [integral_domain A] {x : A} [hℚA : algebra A] (hx : is_integral x) :

The minimal polynomial over is the same as the minimal polynomial over .

theorem minpoly.gcd_domain_dvd {A : Type u_1} {K : Type u_2} {R : Type u_3} [integral_domain A] [gcd_monoid A] [field K] [integral_domain R] (f : fraction_map A K) [algebra (localization_map.codomain f) R] [algebra A R] [is_scalar_tower A (localization_map.codomain f) R] {x : R} (hx : is_integral A x) {P : polynomial A} (hprim : P.is_primitive) (hroot : (polynomial.aeval x) P = 0) :
minpoly A x P

For GCD domains, the minimal polynomial divides any primitive polynomial that has the integral element as root.

theorem minpoly.integer_dvd {A : Type u_1} [integral_domain A] [algebra A] {x : A} (hx : is_integral x) {P : polynomial } (hprim : P.is_primitive) (hroot : (polynomial.aeval x) P = 0) :

The minimal polynomial over divides any primitive polynomial that has the integral element as root.

theorem minpoly.eq_X_sub_C {A : Type u_1} (B : Type u_2) [field A] [ring B] [algebra A B] [nontrivial B] (a : A) :

If B/K is a nontrivial algebra over a field, and x is an element of K, then the minimal polynomial of algebra_map K B x is X - C x.

theorem minpoly.eq_X_sub_C' {A : Type u_1} [field A] (a : A) :
@[simp]
theorem minpoly.zero (A : Type u_1) (B : Type u_2) [field A] [ring B] [algebra A B] [nontrivial B] :

The minimal polynomial of 0 is X.

@[simp]
theorem minpoly.one (A : Type u_1) (B : Type u_2) [field A] [ring B] [algebra A B] [nontrivial B] :

The minimal polynomial of 1 is X - 1.

theorem minpoly.prime {A : Type u_1} {B : Type u_2} [field A] [domain B] [algebra A B] {x : B} (hx : is_integral A x) :

A minimal polynomial is prime.

theorem minpoly.root {A : Type u_1} {B : Type u_2} [field A] [domain B] [algebra A B] {x : B} (hx : is_integral A x) {y : A} (h : (minpoly A x).is_root y) :
(algebra_map A B) y = x

If L/K is a field extension and an element y of K is a root of the minimal polynomial of an element x ∈ L, then y maps to x under the field embedding.

@[simp]
theorem minpoly.coeff_zero_eq_zero {A : Type u_1} {B : Type u_2} [field A] [domain B] [algebra A B] {x : B} (hx : is_integral A x) :
(minpoly A x).coeff 0 = 0 x = 0

The constant coefficient of the minimal polynomial of x is 0 if and only if x = 0.

theorem minpoly.coeff_zero_ne_zero {A : Type u_1} {B : Type u_2} [field A] [domain B] [algebra A B] {x : B} (hx : is_integral A x) (h : x 0) :
(minpoly A x).coeff 0 0

The minimal polynomial of a nonzero element has nonzero constant coefficient.