Root sets and multiplicities

This file records several facts about the roots of a polynomial, either in its coefficient field or after base change to a domain E.

First, an explicit numbering of the root set of a separable polynomial enumerates its full root multiset: separability makes the roots simple, so the multiset is the image of the numbering. This lets root-product formulas be expressed as finite products indexed by Fin f.natDegree, without choosing a global order on the root set.

Second, the root set of a product of polynomials whose base changes to E are nonzero is the union of the root sets of the factors. This is the lemma that decomposes the roots of a polynomial along a factorisation, for instance the roots of a monic integer polynomial along its monic irreducible factors. The same holds for the distinct roots of a finite product.

Third, dividing a polynomial by the linear factor of a simple root removes exactly that root from the root set. Here a only has to be a simple root in E: f a vanishes and f' a does not vanish after mapping to E, so the map F → E need not be injective.

Fourth, translating the variable moves the roots: the roots of f(X + t) are the points x with x + t a root of f, so x ↦ x + t is a bijection between the two root sets, and f(X + t) is separable exactly when f is.

Fifth, if every root of a nonzero polynomial is among a family of points θ i, then its roots are exactly the θ i in which it has positive multiplicity.

Finally, the roots of a polynomial gcd form the multiset intersection of the roots of its inputs. In characteristic zero this identifies the degree lost to the gcd with the derivative as the number of distinct roots.

Main results

• Polynomial.Separable.roots_map_eq_map_numbering: for a separable polynomial, a numbering of its root set enumerates its full root multiset after base change.
• Polynomial.rootSet_mul: the root set of a product of polynomials whose base changes to E are nonzero is the union of the root sets of the factors.
• Polynomial.roots_prod_toFinset: the distinct roots of a finite product of nonzero polynomials are those of the factors together.
• Polynomial.aroots_prod_toFinset: the distinct roots of a finite product of polynomials whose base changes to E are nonzero are those of the factors together.
• Polynomial.rootSet_divByMonic_X_sub_C: if f a = 0 and f' a ≠ 0 in E, then the roots of f /ₘ (X - C a) are the roots of f other than a.
• Polynomial.rootSet_comp_X_add_C: the roots of f(X + t) are the roots of f moved by -t.
• Polynomial.rootSetCompXAddCEquiv: the bijection x ↦ x + t from the roots of f(X + t) to the roots of f.
• Polynomial.separable_comp_X_add_C_iff: f(X + t) is separable exactly when f is.
• Polynomial.isRoot_iff_of_rootMultiplicity: if every root of a nonzero polynomial is among the θ i, then its roots are the θ i in which it has positive multiplicity.
• Polynomial.rootMultiplicity_gcd: a root's multiplicity in a gcd is the minimum of its multiplicities in the two inputs.
• Polynomial.natDegree_sub_natDegree_gcd_derivative_eq_card_roots_toFinset: over an algebraically closed field of characteristic zero, degree minus the degree of the derivative gcd counts distinct roots.

theorem Polynomial.Separable.roots_map_eq_map_numbering {F : Type u_1} [CommRing F] {E : Type u_2} [CommRing E] [IsDomain E] [Algebra F E] {f : Polynomial F} (hsep : f.Separable) (e : Fin f.natDegree ≃ ↑(f.rootSet E)) : (Polynomial.map (algebraMap F E) f).roots = Multiset.map (fun (i : Fin f.natDegree) => ↑(e i)) Finset.univ.val

A numbering of the root set of a separable polynomial enumerates the whole root multiset: separability makes the roots simple, so the multiset is the image of the numbering.

@[simp]

theorem Polynomial.rootSet_mul {F : Type u_1} [CommRing F] {E : Type u_2} [CommRing E] [IsDomain E] [Algebra F E] {f g : Polynomial F} (hf : map (algebraMap F E) f ≠ 0) (hg : map (algebraMap F E) g ≠ 0) : (f * g).rootSet E = f.rootSet E ∪ g.rootSet E

The root set of a product of polynomials is the union of the root sets of the factors, provided neither factor vanishes after base change to E.

theorem Polynomial.roots_prod_toFinset {F : Type u_1} [CommRing F] [IsDomain F] [DecidableEq F] {ι : Type u_3} (s : Finset ι) (f : ι → Polynomial F) (hf : ∀ k ∈ s, f k ≠ 0) : (s.prod f).roots.toFinset = s.biUnion fun (k : ι) => (f k).roots.toFinset

The distinct roots of a finite product of nonzero polynomials are those of the factors together.

theorem Polynomial.aroots_prod_toFinset {F : Type u_1} [CommRing F] {E : Type u_2} [CommRing E] [IsDomain E] [Algebra F E] [DecidableEq E] {ι : Type u_3} (s : Finset ι) (f : ι → Polynomial F) (hf : ∀ k ∈ s, map (algebraMap F E) (f k) ≠ 0) : ((∏ k ∈ s, f k).aroots E).toFinset = s.biUnion fun (k : ι) => ((f k).aroots E).toFinset

The distinct roots in E of a finite product of polynomials are those of the factors together, provided no factor vanishes after base change to E.

@[simp]

theorem Polynomial.rootSet_divByMonic_X_sub_C {F : Type u_1} [CommRing F] {E : Type u_2} [CommRing E] [IsDomain E] [Algebra F E] {f : Polynomial F} {a : F} (ha : (algebraMap F E) (eval a f) = 0) (ha' : (algebraMap F E) (eval a (derivative f)) ≠ 0) : (f /ₘ (X - C a)).rootSet E = f.rootSet E \ {(algebraMap F E) a}

Removing the linear factor of a simple root a removes exactly that root: if, in E, f a vanishes and f' a does not, then the roots of f /ₘ (X - C a) in E are the roots of f other than a.

theorem Polynomial.rootSet_comp_X_add_C {F : Type u_1} [CommRing F] {E : Type u_2} [CommRing E] [IsDomain E] [Algebra F E] (f : Polynomial F) (t : F) : (f.comp (X + C t)).rootSet E = (fun (x : E) => x + (algebraMap F E) t) ⁻¹' f.rootSet E

The roots of f(X + t) are the points x with x + t a root of f.

def Polynomial.rootSetCompXAddCEquiv {F : Type u_1} [CommRing F] (f : Polynomial F) (t : F) (E : Type u_3) [CommRing E] [IsDomain E] [Algebra F E] : ↑((f.comp (X + C t)).rootSet E) ≃ ↑(f.rootSet E)

The bijection x ↦ x + t from the roots of f(X + t) to the roots of f.

Equations

• f.rootSetCompXAddCEquiv t E = Equiv.subtypeEquiv (Equiv.addRight ((algebraMap F E) t)) ⋯

@[simp]

theorem Polynomial.coe_rootSetCompXAddCEquiv_apply {F : Type u_1} [CommRing F] {E : Type u_2} [CommRing E] [IsDomain E] [Algebra F E] (f : Polynomial F) (t : F) (x : ↑((f.comp (X + C t)).rootSet E)) : ↑((f.rootSetCompXAddCEquiv t E) x) = ↑x + (algebraMap F E) t

The bijection Polynomial.rootSetCompXAddCEquiv adds t.

@[simp]

theorem Polynomial.coe_rootSetCompXAddCEquiv_symm_apply {F : Type u_1} [CommRing F] {E : Type u_2} [CommRing E] [IsDomain E] [Algebra F E] (f : Polynomial F) (t : F) (x : ↑(f.rootSet E)) : ↑((f.rootSetCompXAddCEquiv t E).symm x) = ↑x - (algebraMap F E) t

The inverse of Polynomial.rootSetCompXAddCEquiv subtracts t.

theorem Polynomial.Separable.comp_X_add_C {F : Type u_1} [CommRing F] {f : Polynomial F} (hf : f.Separable) (t : F) : (f.comp (X + C t)).Separable

Translating the variable preserves separability.

@[simp]

theorem Polynomial.separable_comp_X_add_C_iff {F : Type u_1} [CommRing F] {f : Polynomial F} {t : F} : (f.comp (X + C t)).Separable ↔ f.Separable

f(X + t) is separable exactly when f is.

theorem Polynomial.isRoot_iff_of_rootMultiplicity {F : Type u_1} [CommRing F] {ι : Type u_3} {p : Polynomial F} {θ : ι → F} {m : ι → ℕ} (hm : ∀ (i : ι), rootMultiplicity (θ i) p = m i) (hθ : ∀ (t : F), p.IsRoot t → ∃ (i : ι), θ i = t) (hp : p ≠ 0) (t : F) : p.IsRoot t ↔ ∃ (i : ι), θ i = t ∧ 0 < m i

If every root of a nonzero polynomial p is some θ i, and the multiplicity of each θ i as a root of p is m i, then the roots of p are the θ i with 0 < m i.

theorem Polynomial.rootMultiplicity_gcd {K : Type u_3} [Field K] [DecidableEq K] (p q : Polynomial K) (hp : p ≠ 0) (hq : q ≠ 0) (x : K) : rootMultiplicity x (EuclideanDomain.gcd p q) = min (rootMultiplicity x p) (rootMultiplicity x q)

The multiplicity of a root in the gcd of two nonzero polynomials is the minimum of its multiplicities in the two polynomials.

theorem Polynomial.roots_gcd {K : Type u_3} [Field K] [DecidableEq K] (p q : Polynomial K) (hp : p ≠ 0) (hq : q ≠ 0) : (EuclideanDomain.gcd p q).roots = p.roots ∩ q.roots

The roots of the gcd of two nonzero polynomials are the multiset intersection of their roots. Thus a common root occurs with the minimum of its two input multiplicities.

theorem Polynomial.roots_gcd_derivative_add_dedup {K : Type u_3} [Field K] [DecidableEq K] [CharZero K] (p : Polynomial K) : (EuclideanDomain.gcd p (derivative p)).roots + p.roots.dedup = p.roots

In characteristic zero, the roots of a polynomial's derivative gcd, together with one copy of each distinct root, recover all roots with multiplicity.

theorem Polynomial.natDegree_sub_natDegree_gcd_derivative_eq_card_roots_toFinset_of_splits {K : Type u_3} [Field K] [DecidableEq K] [CharZero K] {p : Polynomial K} (hp : p ≠ 0) (hsplit : p.Splits) : p.natDegree - (EuclideanDomain.gcd p (derivative p)).natDegree = p.roots.toFinset.card

For a split polynomial in characteristic zero, the number of distinct roots of a nonzero polynomial is its degree minus the degree of its gcd with its derivative.

theorem Polynomial.natDegree_sub_natDegree_gcd_derivative_eq_card_roots_toFinset {K : Type u_3} [Field K] [DecidableEq K] [CharZero K] [IsAlgClosed K] {p : Polynomial K} (hp : p ≠ 0) : p.natDegree - (EuclideanDomain.gcd p (derivative p)).natDegree = p.roots.toFinset.card

Over an algebraically closed field of characteristic zero, the number of distinct roots of a nonzero polynomial is its degree minus the degree of its gcd with its derivative.