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.

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

Suppose x : B, where B is an A-algebra.

The minimal polynomial minpoly A x of x is a monic polynomial with coefficients in A of smallest degree that has x as its root, if such exists (is_integral A x) or zero otherwise.

For example, if V is a π•œ-vector space for some field π•œ and f : V β†’β‚—[π•œ] V then the minimal polynomial of f is minpoly π•œ f.

Equations
source
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) :
(minpoly A x).monic

A minimal polynomial is monic.

source
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.

source
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
source
@[simp]
theorem minpoly.aeval (A : Type u_1) {B : Type u_2} [comm_ring A] [ring B] [algebra A B] (x : B) :
⇑(polynomial.aeval x) (minpoly A x) = 0

An element is a root of its minimal polynomial.

source
theorem minpoly.ne_one (A : Type u_1) {B : Type u_2} [comm_ring A] [ring B] [algebra A B] (x : B) [nontrivial B] :
minpoly A x β‰  1

A minimal polynomial is not 1.

source
theorem minpoly.map_ne_one (A : Type u_1) {B : Type u_2} [comm_ring A] [ring B] [algebra A B] (x : B) [nontrivial B] {R : Type u_3} [semiring R] [nontrivial R] (f : A β†’+* R) :
polynomial.map f (minpoly A x) β‰  1
source
theorem minpoly.not_is_unit (A : Type u_1) {B : Type u_2} [comm_ring A] [ring B] [algebra A B] (x : B) [nontrivial B] :
Β¬is_unit (minpoly A x)

A minimal polynomial is not a unit.

source
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) :
x ∈ (algebra_map A B).range
source
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) :
(minpoly A x).degree ≀ p.degree

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.

source
theorem minpoly.subsingleton (A : Type u_1) {B : Type u_2} [comm_ring A] [ring B] [algebra A B] (x : B) [subsingleton B] :
minpoly A x = 1
source
theorem minpoly.nat_degree_pos {A : Type u_1} {B : Type u_2} [comm_ring A] [ring B] [algebra A B] [nontrivial B] {x : B} (hx : is_integral A x) :
0 < (minpoly A x).nat_degree

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

source
theorem minpoly.degree_pos {A : Type u_1} {B : Type u_2} [comm_ring 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.

source
theorem minpoly.eq_X_sub_C_of_algebra_map_inj {A : Type u_1} {B : Type u_2} [comm_ring A] [ring B] [algebra A B] [nontrivial B] (a : A) (hf : function.injective ⇑(algebra_map A B)) :
minpoly A (⇑(algebra_map A B) a) = polynomial.X - ⇑polynomial.C a

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.

source
theorem minpoly.aeval_ne_zero_of_dvd_not_unit_minpoly {A : Type u_1} {B : Type u_2} [comm_ring A] [is_domain A] [ring 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)) :
⇑(polynomial.aeval x) a β‰  0

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

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

A minimal polynomial is irreducible.

source
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) :
(minpoly A x).degree ≀ p.degree

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. See also gcd_domain_degree_le_of_ne_zero which relaxes the assumptions on A in exchange for stronger assumptions on B.

source
theorem minpoly.ne_zero_of_finite_field_extension (A : Type u_1) {B : Type u_2} [field A] [ring B] [algebra A B] (e : B) [finite_dimensional A B] :
minpoly A e β‰  0
source
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 = 0 β†’ p.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. See also minpoly.gcd_unique which relaxes the assumptions on A in exchange for stronger assumptions on B.

source
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. See also minpoly.gcd_domain_dvd which relaxes the assumptions on A in exchange for stronger assumptions on B.

source
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) :
minpoly K x ∣ polynomial.map (algebra_map A K) (minpoly A x)
source
theorem minpoly.aeval_of_is_scalar_tower (R : Type u_1) {K : Type u_2} {T : Type u_3} {U : Type u_4} [comm_ring R] [field K] [comm_ring T] [algebra R K] [algebra K T] [algebra R T] [is_scalar_tower R K T] [comm_semiring U] [algebra K U] [algebra R U] [is_scalar_tower R K U] (x : T) (y : U) (hy : ⇑(polynomial.aeval y) (minpoly K x) = 0) :
⇑(polynomial.aeval y) (minpoly R x) = 0

If y is a conjugate of x over a field K, then it is a conjugate over a subring R.

source
theorem minpoly.eq_of_irreducible_of_monic {A : Type u_1} {B : Type u_2} [field A] [ring B] [algebra A B] {x : B} [nontrivial B] {p : polynomial A} (hp1 : irreducible p) (hp2 : ⇑(polynomial.aeval x) p = 0) (hp3 : p.monic) :
p = minpoly A x
source
theorem minpoly.eq_of_irreducible {A : Type u_1} {B : Type u_2} [field A] [ring B] [algebra A B] {x : B} [nontrivial B] {p : polynomial A} (hp1 : irreducible p) (hp2 : ⇑(polynomial.aeval x) p = 0) :
p * ⇑polynomial.C (p.leading_coeff)⁻¹ = minpoly A x
source
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.

source
theorem minpoly.add_algebra_map {A : Type u_1} [field A] {B : Type u_2} [comm_ring B] [algebra A B] {x : B} (hx : is_integral A x) (a : A) :
minpoly A (x + ⇑(algebra_map A B) a) = (minpoly A x).comp (polynomial.X - ⇑polynomial.C a)
source
theorem minpoly.sub_algebra_map {A : Type u_1} [field A] {B : Type u_2} [comm_ring B] [algebra A B] {x : B} (hx : is_integral A x) (a : A) :
minpoly A (x - ⇑(algebra_map A B) a) = (minpoly A x).comp (polynomial.X + ⇑polynomial.C a)
source
noncomputable def minpoly.fintype.subtype_prod {E : Type u_1} {X : set E} (hX : X.finite) {L : Type u_2} (F : E β†’ multiset L) :
fintype (Ξ  (x : β†₯X), {l // l ∈ F ↑x})

A technical finiteness result.

Equations
source
def minpoly.roots_of_min_poly_pi_type (F : Type u_3) (E : Type u_4) (K : Type u_5) [field F] [ring E] [comm_ring K] [is_domain K] [algebra F E] [algebra F K] [finite_dimensional F E] (Ο† : E →ₐ[F] K) (x : β†₯(set.range ⇑(finite_dimensional.fin_basis F E))) :
{l // l ∈ (polynomial.map (algebra_map F K) (minpoly F x.val)).roots}

Function from Hom_K(E,L) to pi type Ξ  (x : basis), roots of min poly of x

Equations
source
theorem minpoly.aux_inj_roots_of_min_poly (F : Type u_3) (E : Type u_4) (K : Type u_5) [field F] [ring E] [comm_ring K] [is_domain K] [algebra F E] [algebra F K] [finite_dimensional F E] :
function.injective (minpoly.roots_of_min_poly_pi_type F E K)
source
@[protected, instance]
noncomputable def minpoly.alg_hom.fintype (F : Type u_3) (E : Type u_4) (K : Type u_5) [field F] [ring E] [comm_ring K] [is_domain K] [algebra F E] [algebra F K] [finite_dimensional F E] :
fintype (E →ₐ[F] K)

Given field extensions E/F and K/F, with E/F finite, there are finitely many F-algebra homomorphisms E →ₐ[K] K.

Equations
source
theorem minpoly.gcd_domain_eq_field_fractions {R : Type u_3} {S : Type u_4} (K : Type u_5) (L : Type u_6) [comm_ring R] [is_domain R] [normalized_gcd_monoid R] [field K] [comm_ring S] [is_domain S] [algebra R K] [is_fraction_ring R K] [algebra R S] [field L] [algebra S L] [algebra K L] [algebra R L] [is_scalar_tower R K L] [is_scalar_tower R S L] {s : S} (hs : is_integral R s) :
minpoly K (⇑(algebra_map S L) s) = polynomial.map (algebra_map R K) (minpoly R s)

For GCD domains, the minimal polynomial over the ring is the same as the minimal polynomial over the fraction field. See minpoly.gcd_domain_eq_field_fractions' if S is already a K-algebra.

source
theorem minpoly.gcd_domain_eq_field_fractions' {R : Type u_3} {S : Type u_4} (K : Type u_5) [comm_ring R] [is_domain R] [normalized_gcd_monoid R] [field K] [comm_ring S] [is_domain S] [algebra R K] [is_fraction_ring R K] [algebra R S] {s : S} (hs : is_integral R s) [algebra K S] [is_scalar_tower R K S] :
minpoly K s = polynomial.map (algebra_map R K) (minpoly R s)

For GCD domains, the minimal polynomial over the ring is the same as the minimal polynomial over the fraction field. Compared to minpoly.gcd_domain_eq_field_fractions, this version is useful if the element is in a ring that is already a K-algebra.

source
theorem minpoly.gcd_domain_dvd {R : Type u_3} {S : Type u_4} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] [comm_ring S] [is_domain S] [algebra R S] {s : S} (hs : is_integral R s) [no_zero_smul_divisors R S] {P : polynomial R} (hP : P β‰  0) (hroot : ⇑(polynomial.aeval s) P = 0) :
minpoly R s ∣ P

For GCD domains, the minimal polynomial divides any primitive polynomial that has the integral element as root. See also minpoly.dvd which relaxes the assumptions on S in exchange for stronger assumptions on R.

source
theorem minpoly.gcd_domain_degree_le_of_ne_zero {R : Type u_3} {S : Type u_4} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] [comm_ring S] [is_domain S] [algebra R S] {s : S} (hs : is_integral R s) [no_zero_smul_divisors R S] {p : polynomial R} (hp0 : p β‰  0) (hp : ⇑(polynomial.aeval s) p = 0) :
(minpoly R s).degree ≀ p.degree

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. See also minpoly.degree_le_of_ne_zero which relaxes the assumptions on S in exchange for stronger assumptions on R.

source
theorem minpoly.gcd_domain_unique {R : Type u_3} {S : Type u_4} [comm_ring R] [is_domain R] [normalized_gcd_monoid R] [comm_ring S] [is_domain S] [algebra R S] {s : S} [no_zero_smul_divisors R S] {P : polynomial R} (hmo : P.monic) (hP : ⇑(polynomial.aeval s) P = 0) (Pmin : βˆ€ (Q : polynomial R), Q.monic β†’ ⇑(polynomial.aeval s) Q = 0 β†’ P.degree ≀ Q.degree) :
P = minpoly R s

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. See also minpoly.unique which relaxes the assumptions on S in exchange for stronger assumptions on R.

source
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) :
minpoly A (⇑(algebra_map A B) a) = polynomial.X - ⇑polynomial.C 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.

source
theorem minpoly.eq_X_sub_C' {A : Type u_1} [field A] (a : A) :
minpoly A a = polynomial.X - ⇑polynomial.C a
source
@[simp]
theorem minpoly.zero (A : Type u_1) (B : Type u_2) [field A] [ring B] [algebra A B] [nontrivial B] :
minpoly A 0 = polynomial.X

The minimal polynomial of 0 is X.

source
@[simp]
theorem minpoly.one (A : Type u_1) (B : Type u_2) [field A] [ring B] [algebra A B] [nontrivial B] :
minpoly A 1 = polynomial.X - 1

The minimal polynomial of 1 is X - 1.

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

A minimal polynomial is prime.

source
theorem minpoly.root {A : Type u_1} {B : Type u_2} [field A] [ring B] [is_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.

source
@[simp]
theorem minpoly.coeff_zero_eq_zero {A : Type u_1} {B : Type u_2} [field A] [ring B] [is_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.

source
theorem minpoly.coeff_zero_ne_zero {A : Type u_1} {B : Type u_2} [field A] [ring B] [is_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.