Minimal polynomials of classes in AdjoinRoot

For polynomials f and g over a field K, the class AdjoinRoot.mk f g is the value g(α) at the root α of f. Its minimal polynomial over K is the polynomial whose roots are the images under g of the roots of f when f is irreducible: it divides p exactly when f ∣ p.comp g, which for squarefree f says that g maps the roots of f into the roots of p. It is irreducible of degree at most deg f.

Main results

• AdjoinRoot.minpoly_mk_dvd_iff: minpoly K (mk f g) ∣ p ↔ f ∣ p.comp g.
• AdjoinRoot.natDegree_minpoly_mk_le: for f ≠ 0, the minimal polynomial has degree at most f.natDegree.
• AdjoinRoot.irreducible_minpoly_mk: for f irreducible, the minimal polynomial is irreducible.
• AdjoinRoot.minpoly_root_of_monic: over any commutative ring, the minimal polynomial of the adjoined root of a monic f is f.

theorem AdjoinRoot.minpoly_mk_dvd_iff {K : Type u_1} [Field K] {f g p : Polynomial K} : minpoly K ((mk f) g) ∣ p ↔ f ∣ p.comp g

The minimal polynomial of g(α), for the root α of f, divides p exactly when f ∣ p.comp g, that is, when p(g(α)) = 0 in AdjoinRoot f. For squarefree f this says that g maps the roots of f into the roots of p.

theorem AdjoinRoot.dvd_minpoly_mk_comp {K : Type u_1} [Field K] (f g : Polynomial K) : f ∣ (minpoly K ((mk f) g)).comp g

g maps the roots of f into the roots of the minimal polynomial of g(α).

theorem AdjoinRoot.natDegree_minpoly_mk_le {K : Type u_1} [Field K] {f : Polynomial K} (g : Polynomial K) (hf : f ≠ 0) : (minpoly K ((mk f) g)).natDegree ≤ f.natDegree

The minimal polynomial of an element of AdjoinRoot f has degree at most that of f.

theorem AdjoinRoot.irreducible_minpoly_mk {K : Type u_1} [Field K] {f : Polynomial K} (g : Polynomial K) (hf : Irreducible f) : Irreducible (minpoly K ((mk f) g))

For f irreducible, the minimal polynomial of an element of AdjoinRoot f is irreducible.

theorem AdjoinRoot.minpoly_root_of_monic {R : Type u_2} [CommRing R] {f : Polynomial R} (hf : f.Monic) : minpoly R (root f) = f

Over any commutative ring, the minimal polynomial of the adjoined root of a monic polynomial f is f itself: no nonzero polynomial of smaller degree vanishes at root f, because 1, root f, …, root f ^ (deg f - 1) is a basis. Over a field this is AdjoinRoot.minpoly_powerBasis_gen_of_monic.