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.

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

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.

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

theorem minpoly.unique (A : Type u_1) {B : Type u_2} [Field A] [Ring B] [Algebra A B] (x : B) {p : Polynomial A} (pmonic : Polynomial.Monic p) (hp : ↑(Polynomial.aeval x) p = 0) (pmin : ∀ (q : Polynomial A), Polynomial.Monic q → ↑(Polynomial.aeval x) q = 0 → Polynomial.degree p ≤ Polynomial.degree q) : 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.

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.

theorem minpoly.dvd_map_of_isScalarTower (A : Type u_3) (K : Type u_4) {R : Type u_5} [CommRing A] [Field K] [CommRing 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)

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] [CommRing 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)

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.

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 : Polynomial.Monic p) : p = minpoly A x

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 (Polynomial.leadingCoeff p)⁻¹ = minpoly A x

theorem minpoly.add_algebraMap {A : Type u_1} [Field A] {B : Type u_3} [CommRing B] [Algebra A B] {x : B} (hx : IsIntegral A x) (a : A) : minpoly A (x + ↑(algebraMap A B) a) = Polynomial.comp (minpoly A x) (Polynomial.X - ↑Polynomial.C a)

theorem minpoly.sub_algebraMap {A : Type u_1} [Field A] {B : Type u_3} [CommRing B] [Algebra A B] {x : B} (hx : IsIntegral A x) (a : A) : minpoly A (x - ↑(algebraMap A B) a) = Polynomial.comp (minpoly A x) (Polynomial.X + ↑Polynomial.C a)

noncomputable def minpoly.Fintype.subtypeProd {E : Type u_3} {X : Set E} (hX : Set.Finite X) {L : Type u_4} (F : E → Multiset L) : Fintype ((x : ↑X) → { l // l ∈ F ↑x })

A technical finiteness result.

Equations

• minpoly.Fintype.subtypeProd hX F = Pi.fintype

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 ↑(FiniteDimensional.finBasis F E))) : { l // l ∈ Polynomial.aroots (minpoly F ↑x) 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 = { val := ↑φ ↑x, property := (_ : ↑φ ↑x ∈ Polynomial.aroots (minpoly F ↑x) K) }

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 (minpoly.rootsOfMinPolyPiType F E K)

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) (_ : Function.Injective (minpoly.rootsOfMinPolyPiType F E K))

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.

theorem minpoly.eq_X_sub_C' {A : Type u_1} [Field A] (a : A) : minpoly A a = Polynomial.X - ↑Polynomial.C a

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

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

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.

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 : Polynomial.IsRoot (minpoly A x) 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.

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

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