Specializing the universal resolvent at a polynomial

The universal resolvent of an invariant Φ in n formal roots is the product of X - Ψ over the permutation orbit of Φ, and it is a polynomial in the elementary symmetric polynomials of the formal roots: MvPolynomial.existsUnique_orbitProduct provides the unique integral expression D with D.map (esymmSubst n) = universalResolvent Φ.

This file substitutes an actual polynomial into that expression. For a monic f of degree n, Vieta's formulas say that the (k+1)-st elementary symmetric polynomial of its roots is (-1) ^ (k+1) * f.coeff (n - (k+1)), a function of the coefficients of f alone. Substituting those values is the ring morphism TauCeti.vietaHom n f, and D.map (vietaHom n f) is the resolvent of f: a polynomial over the coefficient ring of f, defined without reference to a splitting field.

The comparison with the roots is the last step of the descent. In a ring where f is the product of the linear factors attached to a family x of roots, the substitution factors as evaluation at x of the elementary symmetric polynomials, so the resolvent of f is the orbit product MvPolynomial.galResolvent Φ x formed from the values of the orbit of Φ at x.

The orbit is taken in MvPolynomial (Fin n) ℤ and its elements are then evaluated. Forming the orbit after mapping the coefficients into the target ring would be a different object: over a ring where two integral renamings of Φ become equal the orbit is smaller, and the product over it is not the substitution above.

Main definitions

• MvPolynomial.galResolvent: the orbit product ∏ (X - C (Ψ x)) of the values at a root family x of the permutation orbit of Φ.
• TauCeti.vietaHom: the substitution of the signed coefficients of f for the elementary symmetric polynomials of its roots.

Main results

• TauCeti.vietaHom_eq_comp_esymmSubst: Vieta's formulas in the form the descent uses, that the substitution is evaluation at the roots of the elementary-symmetric substitution.
• TauCeti.map_vietaHom_eq_galResolvent: agreement, that an integral expression for the universal resolvent specializes at f to the orbit product at the roots of f.
• TauCeti.vietaHom_map: the substitution commutes with a ring morphism applied to the coefficients of f, so the specialization of a fixed integral expression is compatible with base change.
• MvPolynomial.monic_galResolvent and MvPolynomial.natDegree_galResolvent: the orbit product is monic of degree the size of the orbit, whatever the values of the orbit at x are.
• MvPolynomial.roots_galResolvent: over a domain its roots are, with multiplicity, the values of the orbit at x.
• MvPolynomial.galResolvent_comp_perm and MvPolynomial.galResolvent_map: it does not depend on the numbering of the roots, and it commutes with a ring morphism applied to them.
• MvPolynomial.galResolvent_rename: renaming the invariant does not change the orbit resolvent.
• TauCeti.monic_map_vietaHom and TauCeti.natDegree_map_vietaHom: the specialization is monic of degree the size of the orbit, over every nonzero coefficient ring.

noncomputable def MvPolynomial.galResolvent {L : Type u_1} [CommRing L] {n : ℕ} (Φ : MvPolynomial (Fin n) ℤ) (x : Fin n → L) : Polynomial L

The orbit resolvent of Φ at a family x of roots: the product of X - Ψ(x) over the permutation orbit of Φ, each orbit element being an integral polynomial evaluated at x.

Equations

• Φ.galResolvent x = ∏ Ψ ∈ Φ.renameOrbit, (Polynomial.X - Polynomial.C (MvPolynomial.eval₂ (Int.castRingHom L) x Ψ))

theorem MvPolynomial.galResolvent_def {L : Type u_1} [CommRing L] {n : ℕ} (Φ : MvPolynomial (Fin n) ℤ) (x : Fin n → L) : Φ.galResolvent x = ∏ Ψ ∈ Φ.renameOrbit, (Polynomial.X - Polynomial.C (eval₂ (Int.castRingHom L) x Ψ))

The orbit resolvent is the product of the monic linear factors attached to the values at x of the elements of the rename-orbit.

@[simp]

theorem MvPolynomial.galResolvent_rename {L : Type u_1} [CommRing L] {n : ℕ} (e : Equiv.Perm (Fin n)) (Φ : MvPolynomial (Fin n) ℤ) (x : Fin n → L) : ((rename ⇑e) Φ).galResolvent x = Φ.galResolvent x

A renamed invariant has the same orbit resolvent at every root family.

theorem MvPolynomial.map_universalResolvent_eq_galResolvent {L : Type u_1} [CommRing L] {n : ℕ} (Φ : MvPolynomial (Fin n) ℤ) (x : Fin n → L) : Polynomial.map (eval₂Hom (Int.castRingHom L) x) Φ.universalResolvent = Φ.galResolvent x

The orbit resolvent at x is the image of the universal resolvent under evaluation at x.

theorem MvPolynomial.monic_galResolvent {L : Type u_1} [CommRing L] {n : ℕ} (Φ : MvPolynomial (Fin n) ℤ) (x : Fin n → L) : (Φ.galResolvent x).Monic

The orbit resolvent is monic: it is a product of monic linear factors.

@[simp]

theorem MvPolynomial.natDegree_galResolvent {L : Type u_1} [CommRing L] {n : ℕ} [Nontrivial L] (Φ : MvPolynomial (Fin n) ℤ) (x : Fin n → L) : (Φ.galResolvent x).natDegree = Φ.renameOrbit.card

The orbit resolvent has degree the size of the orbit, whatever the values at x are.

@[simp]

theorem MvPolynomial.roots_galResolvent {L : Type u_1} [CommRing L] {n : ℕ} [IsDomain L] (Φ : MvPolynomial (Fin n) ℤ) (x : Fin n → L) : (Φ.galResolvent x).roots = Multiset.map (fun (Ψ : MvPolynomial (Fin n) ℤ) => eval₂ (Int.castRingHom L) x Ψ) Φ.renameOrbit.val

The roots of the orbit resolvent are the values of the orbit. Over a domain the orbit resolvent has, with multiplicity, one root for each element of the rename-orbit of Φ, namely its value at x; distinct orbit elements may take the same value there.

theorem MvPolynomial.galResolvent_comp_perm {L : Type u_1} [CommRing L] {n : ℕ} (Φ : MvPolynomial (Fin n) ℤ) (x : Fin n → L) (σ : Equiv.Perm (Fin n)) : Φ.galResolvent (x ∘ ⇑σ) = Φ.galResolvent x

Renumbering the roots leaves the orbit resolvent unchanged, since the product runs over the whole permutation orbit of Φ.

theorem MvPolynomial.galResolvent_map {L : Type u_1} [CommRing L] {n : ℕ} {M : Type u_2} [CommRing M] (φ : L →+* M) (Φ : MvPolynomial (Fin n) ℤ) (x : Fin n → L) : Polynomial.map φ (Φ.galResolvent x) = Φ.galResolvent (⇑φ ∘ x)

The orbit resolvent commutes with a ring morphism applied to the roots.

noncomputable def TauCeti.vietaHom {R : Type u_1} [CommRing R] (n : ℕ) (f : Polynomial R) : MvPolynomial (Fin n) ℤ →+* R

The Vieta substitution of a polynomial f, sending the variable xᵢ — the slot of the (i+1)-st elementary symmetric polynomial of the roots — to the signed coefficient (-1) ^ (i+1) * f.coeff (n - (i+1)). For a monic f of degree n these values are the elementary symmetric polynomials of the roots of f, which is TauCeti.vietaHom_eq_comp_esymmSubst.

Equations

• TauCeti.vietaHom n f = MvPolynomial.eval₂Hom (Int.castRingHom R) fun (i : Fin n) => (-1) ^ (↑i + 1) * f.coeff (n - (↑i + 1))

@[simp]

theorem TauCeti.vietaHom_X {R : Type u_1} [CommRing R] {n : ℕ} (f : Polynomial R) (i : Fin n) : (vietaHom n f) (MvPolynomial.X i) = (-1) ^ (↑i + 1) * f.coeff (n - (↑i + 1))

The Vieta substitution sends the variable xᵢ to the signed coefficient of f in degree n - (i+1).

theorem TauCeti.vietaHom_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {n : ℕ} (φ : R →+* S) (f : Polynomial R) : vietaHom n (Polynomial.map φ f) = φ.comp (vietaHom n f)

The Vieta substitution reads only the coefficients of f, so mapping them along a ring morphism φ substitutes the images.

theorem TauCeti.vietaHom_eq_comp_esymmSubst {R : Type u_1} [CommRing R] {n : ℕ} {f : Polynomial R} {x : Fin n → R} (hf : f = ∏ i : Fin n, (Polynomial.X - Polynomial.C (x i))) : vietaHom n f = (MvPolynomial.eval₂Hom (Int.castRingHom R) x).comp (esymmSubst n)

Vieta's formulas, in the form the symmetric descent uses: if f is the product of the linear factors attached to x, then substituting the signed coefficients of f is the same as substituting the elementary symmetric polynomials and evaluating at x.

theorem TauCeti.map_vietaHom_eq_galResolvent {R : Type u_1} [CommRing R] {n : ℕ} {Φ : MvPolynomial (Fin n) ℤ} {D : Polynomial (MvPolynomial (Fin n) ℤ)} (hD : Polynomial.map (esymmSubst n) D = Φ.universalResolvent) {f : Polynomial R} {x : Fin n → R} (hf : f = ∏ i : Fin n, (Polynomial.X - Polynomial.C (x i))) : Polynomial.map (vietaHom n f) D = Φ.galResolvent x

Agreement of the two sides of the descent. An integral expression D for the universal resolvent of Φ in the elementary symmetric polynomials specializes, at a polynomial f that is the product of the linear factors attached to x, to the orbit product of Φ at x.

theorem TauCeti.monic_map_vietaHom {R : Type u_1} [CommRing R] {n : ℕ} {Φ : MvPolynomial (Fin n) ℤ} {D : Polynomial (MvPolynomial (Fin n) ℤ)} (hD : Polynomial.map (esymmSubst n) D = Φ.universalResolvent) (f : Polynomial R) : (Polynomial.map (vietaHom n f) D).Monic

The specialization is monic. An integral expression for the universal resolvent is monic, and so is its substitution: reading the coefficients of f never lowers the leading coefficient.

theorem TauCeti.natDegree_map_vietaHom {R : Type u_1} [CommRing R] {n : ℕ} [Nontrivial R] {Φ : MvPolynomial (Fin n) ℤ} {D : Polynomial (MvPolynomial (Fin n) ℤ)} (hD : Polynomial.map (esymmSubst n) D = Φ.universalResolvent) (f : Polynomial R) : (Polynomial.map (vietaHom n f) D).natDegree = Φ.renameOrbit.card

The specialization keeps the full degree. Over every nonzero coefficient ring and for every f, monic or not, the substitution has degree the size of the orbit: what a specialization can destroy is the distinctness of the orbit values, never the degree.

theorem TauCeti.map_vietaHom_eq_galResolvent_of_roots {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] {Φ : MvPolynomial (Fin n) ℤ} {D : Polynomial (MvPolynomial (Fin n) ℤ)} (hD : Polynomial.map (esymmSubst n) D = Φ.universalResolvent) {f : Polynomial R} {x : Fin n → R} (hf : f.Monic) (hdeg : f.natDegree = n) (hroots : f.roots = Multiset.map x Finset.univ.val) : Polynomial.map (vietaHom n f) D = Φ.galResolvent x

Agreement, from a root enumeration. Over a domain, a monic f of degree n whose roots, with multiplicity, are listed by x specializes an integral expression for the universal resolvent to the orbit product at those roots.