# 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`, and derives some basic properties such as irreducibility under the assumption `B` is a domain.

source
noncomputable def minpoly (A : Type u_1) {B : Type u_2} [CommRing 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 (`IsIntegral 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

- minpoly A x = if hx : IsIntegral A x then ⋯.min (fun (x_1 : Polynomial A) => x_1.Monic ∧ Polynomial.eval₂ (algebraMap A B) x x_1 = 0) hx else 0

Instances For

source
theorem minpoly.monic {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] {x : B} (hx : IsIntegral A x) :
(minpoly A x).Monic

A minimal polynomial is monic.

source
theorem minpoly.ne_zero {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] {x : B} [Nontrivial A] (hx : IsIntegral A x) :
minpoly A x ≠ 0

A minimal polynomial is nonzero.

source
theorem minpoly.eq_zero {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] {x : B} (hx : ¬IsIntegral A x) :
minpoly A x = 0
source
theorem minpoly.ne_zero_iff {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] {x : B} [Nontrivial A] :
minpoly A x ≠ 0 ↔ IsIntegral A x
source
theorem minpoly.algHom_eq {A : Type u_1} {B : Type u_2} {B' : Type u_3} [CommRing A] [Ring B] [Ring B'] [Algebra A B] [Algebra A B'] (f : B →ₐ[A] B') (hf : Function.Injective ⇑f) (x : B) :
minpoly A (f x) = minpoly A x
source
theorem minpoly.algebraMap_eq {A : Type u_1} {B' : Type u_3} [CommRing A] [Ring B'] [Algebra A B'] {B : Type u_4} [CommRing B] [Algebra A B] [Algebra B B'] [IsScalarTower A B B'] (h : Function.Injective ⇑(algebraMap B B')) (x : B) :
minpoly A ((algebraMap B B') x) = minpoly A x
source
@[simp]
theorem minpoly.algEquiv_eq {A : Type u_1} {B : Type u_2} {B' : Type u_3} [CommRing A] [Ring B] [Ring B'] [Algebra A B] [Algebra A B'] (f : B ≃ₐ[A] B') (x : B) :
minpoly A (f x) = minpoly A x
source
@[simp]
theorem minpoly.aeval (A : Type u_1) {B : Type u_2} [CommRing 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
@[simp]
theorem minpoly.aeval_algHom (A : Type u_1) {B : Type u_2} {B' : Type u_3} [CommRing A] [Ring B] [Ring B'] [Algebra A B] [Algebra A B'] (f : B →ₐ[A] B') (x : B) :
(Polynomial.aeval (f x)) (minpoly A x) = 0

Given any `f : B →ₐ[A] B'` and any `x : L`, the minimal polynomial of `x` vanishes at `f x`.

source
theorem minpoly.ne_one (A : Type u_1) {B : Type u_2} [CommRing 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} [CommRing A] [Ring B] [Algebra A B] (x : B) [Nontrivial B] {R : Type u_4} [Semiring R] [Nontrivial R] (f : A →+* R) :
Polynomial.map f (minpoly A x) ≠ 1
source
theorem minpoly.not_isUnit (A : Type u_1) {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (x : B) [Nontrivial B] :
¬IsUnit (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} [CommRing A] [Ring B] [Algebra A B] (x : B) (hx : (minpoly A x).degree = 1) :
x ∈ (algebraMap A B).range
source
theorem minpoly.min (A : Type u_1) {B : Type u_2} [CommRing 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.unique' (A : Type u_1) {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (x : B) {p : Polynomial A} (hm : p.Monic) (hp : (Polynomial.aeval x) p = 0) (hl : ∀ (q : Polynomial A), q.degree < p.degree → q = 0 ∨ (Polynomial.aeval x) q ≠ 0) :
p = minpoly A x
source
theorem minpoly.eq_of_linearIndependent (A : Type u_1) {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (x : B) {p : Polynomial A} (monic : p.Monic) (hp0 : (Polynomial.aeval x) p = 0) (n : ℕ) (hpn : p.degree = ↑n) (ind : LinearIndependent A fun (i : Fin n) => x ^ ↑i) :
minpoly A x = p

If a monic polynomial `p : A[X]` of degree `n` annihilates an element `x` in an `A`-algebra `B`, such that `{xⁱ | 0 ≤ i < n}` is linearly independent over `A`, then `p` is the minimal polynomial of `x` over `A`.

source
theorem minpoly.subsingleton (A : Type u_1) {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (x : B) [Subsingleton B] :
minpoly A x = 1
source
theorem minpoly.natDegree_pos {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] {x : B} [Nontrivial B] (hx : IsIntegral A x) :
0 < (minpoly A x).natDegree

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} [CommRing A] [Ring B] [Algebra A B] {x : B} [Nontrivial B] (hx : IsIntegral A x) :
0 < (minpoly A x).degree

The degree of a minimal polynomial is positive.

source
theorem minpoly.degree_eq_one_iff {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] {x : B} [Nontrivial B] :
(minpoly A x).degree = 1 ↔ x ∈ (algebraMap A B).range
source
theorem minpoly.natDegree_eq_one_iff {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] {x : B} [Nontrivial B] :
(minpoly A x).natDegree = 1 ↔ x ∈ (algebraMap A B).range
source
theorem minpoly.two_le_natDegree_iff {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] {x : B} [Nontrivial B] (int : IsIntegral A x) :
2 ≤ (minpoly A x).natDegree ↔ x ∉ (algebraMap A B).range
source
theorem minpoly.two_le_natDegree_subalgebra {A : Type u_1} [CommRing A] {B : Type u_4} [CommRing B] [Algebra A B] [Nontrivial B] {S : Subalgebra A B} {x : B} (int : IsIntegral (↥S) x) :
2 ≤ (minpoly (↥S) x).natDegree ↔ x ∉ S
source
theorem minpoly.eq_X_sub_C_of_algebraMap_inj {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (a : A) (hf : Function.Injective ⇑(algebraMap A B)) :
minpoly A ((algebraMap 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 `algebraMap A B a` is `X - C a`.

source
theorem minpoly.aeval_ne_zero_of_dvdNotUnit_minpoly {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] {x : B} {a : Polynomial A} (hx : IsIntegral A x) (hamonic : a.Monic) (hdvd : DvdNotUnit 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} [CommRing A] [Ring B] [Algebra A B] {x : B} [IsDomain A] [IsDomain B] (hx : IsIntegral A x) :
Irreducible (minpoly A x)

A minimal polynomial is irreducible.