# Minimal polynomials on an algebra over a field #

This file specializes the theory of minpoly to the setting of field extensions and derives some well-known properties, amongst which the fact that minimal polynomials are irreducible, and uniquely determined by their defining property.

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 `minpoly.IsIntegrallyClosed.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 (A : Type u_1) {B : Type u_2} [Field A] [Ring B] [Algebra A B] (e : B) [FiniteDimensional 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.IsIntegrallyClosed.Minpoly.unique` which relaxes the assumptions on `A` in exchange for stronger assumptions on `B`.

source
theorem minpoly.unique_of_degree_le_degree_minpoly (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 : p.degree ≤ (minpoly A x).degree) :
p = minpoly A x
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.isIntegrallyClosed_dvd` which relaxes the assumptions on `A` in exchange for stronger assumptions on `B`.

source
theorem minpoly.dvd_iff {A : Type u_1} {B : Type u_2} [Field A] [Ring B] [Algebra A B] {x : B} {p : Polynomial A} :
minpoly A x ∣ p ↔ (Polynomial.aeval x) p = 0
source
theorem minpoly.isRadical (A : Type u_1) {B : Type u_2} [Field A] [Ring B] [Algebra A B] (x : B) [IsReduced B] :
IsRadical (minpoly A x)
source
theorem minpoly.dvd_map_of_isScalarTower (A : Type u_3) (K : Type u_4) {R : Type u_5} [CommRing A] [Field K] [Ring R] [Algebra A K] [Algebra A R] [Algebra K R] [IsScalarTower A K R] (x : R) :
minpoly K x ∣ Polynomial.map (algebraMap A K) (minpoly A x)
source
theorem minpoly.dvd_map_of_isScalarTower' (R : Type u_3) {S : Type u_4} (K : Type u_5) (L : Type u_6) [CommRing R] [CommRing S] [Field K] [Ring L] [Algebra R S] [Algebra R K] [Algebra S L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [IsScalarTower R S L] (s : S) :
minpoly K ((algebraMap S L) s) ∣ Polynomial.map (algebraMap R K) (minpoly R s)
source
theorem minpoly.aeval_of_isScalarTower (R : Type u_3) {K : Type u_4} {T : Type u_5} {U : Type u_6} [CommRing R] [Field K] [CommRing T] [Algebra R K] [Algebra K T] [Algebra R T] [IsScalarTower R K T] [CommSemiring U] [Algebra K U] [Algebra R U] [IsScalarTower 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.map_algebraMap {F : Type u_3} {E : Type u_4} {A : Type u_5} [Field F] [Field E] [CommRing A] [Algebra F E] [Algebra E A] [Algebra F A] [IsScalarTower F E A] {a : A} (ha : IsIntegral F a) (h : minpoly E a ∈ Polynomial.lifts (algebraMap F E)) :
Polynomial.map (algebraMap F E) (minpoly F a) = minpoly E a

If a subfield `F` of `E` contains all the coefficients of `minpoly E a`, then `minpoly F a` maps to `minpoly E a` via `algebraMap F E`.

source
@[simp]
theorem minpoly.ker_aeval_eq_span_minpoly (A : Type u_1) {B : Type u_2} [Field A] [Ring B] [Algebra A B] (x : B) :
RingHom.ker (Polynomial.aeval x) = Submodule.span (Polynomial A) {minpoly A x}

See also `minpoly.ker_eval` which relaxes the assumptions on `A` in exchange for stronger assumptions on `B`.

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_iff_aeval_eq_zero {A : Type u_1} {B : Type u_2} [Field A] [Ring B] [Algebra A B] {x : B} [Nontrivial B] {p : Polynomial A} (irr : Irreducible p) (monic : p.Monic) :
p = minpoly A x ↔ (Polynomial.aeval x) p = 0
source
theorem minpoly.eq_iff_aeval_minpoly_eq_zero {A : Type u_1} {B : Type u_2} [Field A] [Ring B] [Algebra A B] [IsDomain B] {C : Type u_3} [Ring C] [Algebra A C] [Nontrivial C] {b : B} (h : IsIntegral A b) {c : C} :
minpoly A b = minpoly A c ↔ (Polynomial.aeval c) (minpoly A b) = 0
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.leadingCoeff⁻¹ = minpoly A x
source
theorem minpoly.add_algebraMap {A : Type u_1} [Field A] {B : Type u_3} [CommRing B] [Algebra A B] (x : B) (a : A) :
minpoly A (x + (algebraMap A B) a) = (minpoly A x).comp (Polynomial.X - Polynomial.C a)
source
theorem minpoly.sub_algebraMap {A : Type u_1} [Field A] {B : Type u_3} [CommRing B] [Algebra A B] (x : B) (a : A) :
minpoly A (x - (algebraMap A B) a) = (minpoly A x).comp (Polynomial.X + Polynomial.C a)
source
theorem minpoly.neg {A : Type u_1} [Field A] {B : Type u_3} [Ring B] [Algebra A B] (x : B) :
minpoly A (-x) = (-1) ^ (minpoly A x).natDegree * (minpoly A x).comp (-Polynomial.X)
source
theorem minpoly.map_eq_of_equiv_equiv {A : Type u_1} [Field A] {R : Type u_3} {S : Type u_4} {T : Type u_5} [CommRing R] [IsDomain R] [Ring S] [Ring T] [IsDomain S] [IsDomain T] [Algebra R S] [Algebra A T] [Algebra.IsIntegral R S] {f : R ≃+* A} {g : S ≃+* T} (hcomp : (algebraMap A T).comp ↑f = (↑g).comp (algebraMap R S)) (x : S) :
Polynomial.map (↑f) (minpoly R x) = minpoly A (g x)
source
noncomputable def minpoly.Fintype.subtypeProd {E : Type u_3} {X : Set E} (hX : X.Finite) {L : Type u_4} (F : E → Multiset L) :
Fintype ((x : ↑X) → { l : L // l ∈ F ↑x })

A technical finiteness result.

Equations

- minpoly.Fintype.subtypeProd hX F = Pi.instFintype

Instances For

source
def minpoly.rootsOfMinPolyPiType (F : Type u_3) (E : Type u_4) (K : Type u_5) [Field F] [Ring E] [CommRing K] [IsDomain K] [Algebra F E] [Algebra F K] [FiniteDimensional F E] (φ : E →ₐ[F] K) (x : ↑(Set.range ⇑(Module.finBasis F E))) :
{ l : K // l ∈ (minpoly F ↑x).aroots K }

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

Equations

- minpoly.rootsOfMinPolyPiType F E K φ x = ⟨φ ↑x, ⋯⟩

Instances For

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] [CommRing K] [IsDomain K] [Algebra F E] [Algebra F K] [FiniteDimensional F E] :
Function.Injective (rootsOfMinPolyPiType F E K)
source
noncomputable instance minpoly.AlgHom.fintype (F : Type u_3) (E : Type u_4) (K : Type u_5) [Field F] [Ring E] [CommRing K] [IsDomain K] [Algebra F E] [Algebra F K] [FiniteDimensional 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

- minpoly.AlgHom.fintype F E K = Fintype.ofInjective (minpoly.rootsOfMinPolyPiType F E K) ⋯

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 ((algebraMap 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 `algebraMap 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] [IsDomain B] [Algebra A B] {x : B} (hx : IsIntegral 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] [IsDomain B] [Algebra A B] {x : B} (hx : IsIntegral A x) {y : A} (h : (minpoly A x).IsRoot y) :
(algebraMap 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] [IsDomain B] [Algebra A B] {x : B} (hx : IsIntegral 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] [IsDomain B] [Algebra A B] {x : B} (hx : IsIntegral A x) (h : x ≠ 0) :
(minpoly A x).coeff 0 ≠ 0

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

source
theorem minpoly_algEquiv_toLinearMap {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [IsDomain L] [Algebra K L] (σ : L ≃ₐ[K] L) (hσ : IsOfFinOrder σ) :
minpoly K σ.toLinearMap = Polynomial.X ^ orderOf σ - Polynomial.C 1

The minimal polynomial (over `K`) of `σ : L ≃ₐ[K] L` is `X ^ (orderOf σ) - 1`.

source
theorem minpoly_algHom_toLinearMap {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [IsDomain L] [Algebra K L] (σ : L →ₐ[K] L) (hσ : IsOfFinOrder σ) :
minpoly K σ.toLinearMap = Polynomial.X ^ orderOf σ - Polynomial.C 1

The minimal polynomial (over `K`) of `σ : Gal(L/K)` is `X ^ (orderOf σ) - 1`.