Root enumerations

Let f be a polynomial over a commutative ring R and let L be an R-algebra that is a domain. A family x : ι → L indexed by a finite type is a root enumeration of f when it lists the roots of f in L with multiplicity: the multiset of roots of the image of f in L[X] is the image of x.

Resolvents, discriminants and the elementary symmetric functions of the roots are all computed from such a listing, and two facts are implicit whenever the roots are indexed by a finite set of the size of the degree. Both are stated here.

• Splitting. If ι has at least as many elements as the degree of the image of f in L (in particular, if it has at least f.natDegree elements), then f splits in L. The finite indexing is not available before this: a listing of all roots of a polynomial that does not split in L has fewer entries than its degree.
• Separability. When L is a field and the image of f in L is nonzero, such an enumeration is injective if and only if the image of f in L is separable; over a base field K, for a nonzero f, this is the separability of f itself. Without separability a listing repeats a root, and a permutation of the indices is then no longer determined by the permutation of the roots that it induces.

Conversely, a polynomial that splits in L has a root enumeration indexed by any finite type whose size is the degree of the image of f in L. Reading Vieta's formulas through an enumeration expresses the elementary symmetric polynomials evaluated at x through the coefficients of f.

Main definitions

• Polynomial.IsRootEnumeration f x: x lists the roots of f in L, with multiplicity.

Main results

• Polynomial.IsRootEnumeration.splits: an enumeration with at least as many entries as the degree of the image of f in L makes f split in L.
• Polynomial.exists_isRootEnumeration_iff_splits: a polynomial has an enumeration indexed by a type whose size is the degree of its image in L if and only if it splits in L.
• Polynomial.IsRootEnumeration.injective_iff_separable_map: an enumeration in a field E with as many entries as the degree of the nonzero image of f in E is injective if and only if that image is separable.
• Polynomial.IsRootEnumeration.injective_iff_separable: over a base field, an enumeration of the roots of a nonzero g with g.natDegree entries is injective if and only if g is separable.
• Polynomial.IsRootEnumeration.range_eq_rootSet: the entries of an enumeration are the roots.
• Polynomial.IsRootEnumeration.aeval_esymm_eq_coeff: Vieta's formulas, read through an enumeration of the roots of a monic polynomial.

def Polynomial.IsRootEnumeration {R : Type u_1} {L : Type u_2} {ι : Type u_4} [CommRing R] [CommRing L] [IsDomain L] [Algebra R L] [Fintype ι] (f : Polynomial R) (x : ι → L) : Prop

x is a root enumeration of f in L: it lists the roots of f in L with multiplicity, so that the multiset of roots of the image of f in L[X] is the image of x.

Equations

• f.IsRootEnumeration x = ((Polynomial.map (algebraMap R L) f).roots = Multiset.map x Finset.univ.val)

theorem Polynomial.isRootEnumeration_iff {R : Type u_1} {L : Type u_2} {ι : Type u_4} [CommRing R] [CommRing L] [IsDomain L] [Algebra R L] [Fintype ι] {f : Polynomial R} {x : ι → L} : f.IsRootEnumeration x ↔ (map (algebraMap R L) f).roots = Multiset.map x Finset.univ.val

The defining property of a root enumeration.

@[simp]

theorem Polynomial.isRootEnumeration_comp_equiv_iff {R : Type u_1} {L : Type u_2} {ι : Type u_4} {κ : Type u_5} [CommRing R] [CommRing L] [IsDomain L] [Algebra R L] [Fintype ι] [Fintype κ] {f : Polynomial R} {x : ι → L} (e : κ ≃ ι) : f.IsRootEnumeration (x ∘ ⇑e) ↔ f.IsRootEnumeration x

Reindexing an enumeration along a bijection gives an enumeration.

theorem Polynomial.IsRootEnumeration.card_roots {R : Type u_1} {L : Type u_2} {ι : Type u_4} [CommRing R] [CommRing L] [IsDomain L] [Algebra R L] [Fintype ι] {f : Polynomial R} {x : ι → L} (hx : f.IsRootEnumeration x) : (Polynomial.map (algebraMap R L) f).roots.card = Fintype.card ι

The number of entries of an enumeration is the number of roots of f in L.

theorem Polynomial.IsRootEnumeration.card_le_natDegree {R : Type u_1} {L : Type u_2} {ι : Type u_4} [CommRing R] [CommRing L] [IsDomain L] [Algebra R L] [Fintype ι] {f : Polynomial R} {x : ι → L} (hx : f.IsRootEnumeration x) : Fintype.card ι ≤ f.natDegree

An enumeration has at most f.natDegree entries.

theorem Polynomial.IsRootEnumeration.range_eq_rootSet {R : Type u_1} {L : Type u_2} {ι : Type u_4} [CommRing R] [CommRing L] [IsDomain L] [Algebra R L] [Fintype ι] {f : Polynomial R} {x : ι → L} (hx : f.IsRootEnumeration x) : Set.range x = f.rootSet L

The entries of an enumeration are exactly the roots of f in L.

theorem Polynomial.IsRootEnumeration.natDegree_map_eq_card {R : Type u_1} {L : Type u_2} {ι : Type u_4} [CommRing R] [CommRing L] [IsDomain L] [Algebra R L] [Fintype ι] {f : Polynomial R} {x : ι → L} (hx : f.IsRootEnumeration x) (hdeg : (Polynomial.map (algebraMap R L) f).natDegree ≤ Fintype.card ι) : (Polynomial.map (algebraMap R L) f).natDegree = Fintype.card ι

An enumeration with at least as many entries as the degree of the image of f in L has exactly that many entries, since the number of roots never exceeds the degree. This applies in particular when the enumeration has at least f.natDegree entries, by natDegree_map_le.

theorem Polynomial.IsRootEnumeration.splits {R : Type u_1} {L : Type u_2} {ι : Type u_4} [CommRing R] [CommRing L] [IsDomain L] [Algebra R L] [Fintype ι] {f : Polynomial R} {x : ι → L} (hx : f.IsRootEnumeration x) (hdeg : (Polynomial.map (algebraMap R L) f).natDegree ≤ Fintype.card ι) : (Polynomial.map (algebraMap R L) f).Splits

An enumeration forces splitting. If x enumerates the roots of f in L and has at least as many entries as the degree of the image of f in L (for instance, at least f.natDegree entries), then f splits in L.

theorem Polynomial.IsRootEnumeration.map {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_4} [CommRing R] [CommRing L] [IsDomain L] [Algebra R L] [Fintype ι] {f : Polynomial R} {x : ι → L} [CommRing M] [IsDomain M] [Algebra R M] (hx : f.IsRootEnumeration x) (hdeg : (Polynomial.map (algebraMap R L) f).natDegree ≤ Fintype.card ι) (φ : L →ₐ[R] M) (hφ : Function.Injective ⇑φ) : f.IsRootEnumeration (⇑φ ∘ x)

An enumeration with at least as many entries as the degree of the image of f in L is carried by an injective algebra morphism to an enumeration in the target.

theorem Polynomial.exists_isRootEnumeration_iff_splits {R : Type u_1} {L : Type u_2} {ι : Type u_4} [CommRing R] [CommRing L] [IsDomain L] [Algebra R L] [Fintype ι] {f : Polynomial R} (hdeg : (map (algebraMap R L) f).natDegree = Fintype.card ι) : (∃ (x : ι → L), f.IsRootEnumeration x) ↔ (map (algebraMap R L) f).Splits

Root enumerations exist exactly for split polynomials. If the image of f in L has degree Fintype.card ι, then f has a root enumeration in L indexed by ι if and only if f splits in L.

theorem Polynomial.IsRootEnumeration.aeval_esymm_eq_coeff {R : Type u_1} {L : Type u_2} {ι : Type u_4} [CommRing R] [CommRing L] [IsDomain L] [Algebra R L] [Fintype ι] {f : Polynomial R} {x : ι → L} (hx : f.IsRootEnumeration x) (hf : f.Monic) (hdeg : f.natDegree ≤ Fintype.card ι) {k : ℕ} (hk : k ≤ Fintype.card ι) : (MvPolynomial.aeval x) (MvPolynomial.esymm ι R k) = (-1) ^ k * (algebraMap R L) (f.coeff (Fintype.card ι - k))

Vieta's formulas, read through a root enumeration. If x enumerates the roots in L of the monic polynomial f of degree Fintype.card ι, then for every k ≤ Fintype.card ι the k-th elementary symmetric polynomial evaluated at x is (-1) ^ k times the coefficient of f in degree Fintype.card ι - k.

theorem Polynomial.IsRootEnumeration.injective_iff_separable_map {R : Type u_1} {ι : Type u_4} [CommRing R] [Fintype ι] {f : Polynomial R} {E : Type u_7} [Field E] [Algebra R E] {y : ι → E} (hy : f.IsRootEnumeration y) (hdeg : (Polynomial.map (algebraMap R E) f).natDegree ≤ Fintype.card ι) (hf : Polynomial.map (algebraMap R E) f ≠ 0) : Function.Injective y ↔ (Polynomial.map (algebraMap R E) f).Separable

An enumeration is injective exactly when the polynomial is separable. If y enumerates the roots in the field E of a polynomial f whose image in E is nonzero, and has at least as many entries as the degree of that image, then y is injective if and only if the image of f in E is separable.

theorem Polynomial.IsRootEnumeration.injective_iff_separable {ι : Type u_4} [Fintype ι] {K : Type u_6} {E : Type u_7} [Field K] [Field E] [Algebra K E] {y : ι → E} {g : Polynomial K} (hy : g.IsRootEnumeration y) (hdeg : g.natDegree ≤ Fintype.card ι) (hg : g ≠ 0) : Function.Injective y ↔ g.Separable

An enumeration is injective exactly when the polynomial is separable, over a base field: if y enumerates the roots of the nonzero polynomial g over K and has at least g.natDegree entries, then y is injective if and only if g is separable.