The grading of a resolvent with a homogeneous invariant

If the invariant Φ of a resolvent specification is homogeneous of degree m, so is every element of its rename-orbit, and the coefficient of X ^ k in the universal resolvent is homogeneous of degree m * ([Sₙ : H] - k). The integral orbit product rewrites that coefficient in the elementary symmetric polynomials, and it is therefore weighted homogeneous of the same weight once the variable i, which stands for eᵢ₊₁, is given the weight i + 1.

This grading is what makes a specialization at a sparse polynomial computable. Specializing at f substitutes the signed coefficients of f for the variables, so a variable whose coefficient vanishes kills every monomial containing it, and the weight leaves only finitely many exponents of the surviving variables, each with an integral coefficient independent of f.

Main results

• MvPolynomial.isHomogeneous_universalResolvent_coeff: the coefficients of the universal resolvent of a homogeneous invariant are homogeneous.
• TauCeti.ResolventSpec.isWeightedHomogeneous_orbitProduct_coeff: the coefficients of the integral orbit product are weighted homogeneous for the weights i + 1.

theorem MvPolynomial.isHomogeneous_universalResolvent_coeff {n : ℕ} {Φ : MvPolynomial (Fin n) ℤ} {m : ℕ} (hΦ : Φ.IsHomogeneous m) (k : ℕ) : (Φ.universalResolvent.coeff k).IsHomogeneous (m * (Φ.renameOrbit.card - k))

If Φ is homogeneous of degree m, the coefficient of X ^ k in its universal resolvent is homogeneous of degree m times the number of orbit elements left over.

theorem TauCeti.ResolventSpec.isWeightedHomogeneous_orbitProduct_coeff {n : ℕ} (spec : ResolventSpec n) {m : ℕ} (hΦ : spec.Φ.IsHomogeneous m) (k : ℕ) : MvPolynomial.IsWeightedHomogeneous (fun (i : Fin n) => ↑i + 1) (spec.orbitProduct.coeff k) (m * (spec.H.index - k))

The grading of the orbit product. If the invariant of a specification is homogeneous of degree m, the coefficient of X ^ k in its integral orbit product is weighted homogeneous of weight m * ([Sₙ : H] - k), the variable i having the weight i + 1 of the elementary symmetric polynomial eᵢ₊₁ it stands for.