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.

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

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.

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.

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

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

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

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

@[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

@[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.

@[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.

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.

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

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.

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

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.

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

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 pis the minimal polynomial ofxoverA`.

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

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.

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.

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

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

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

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

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.

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.

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.