Weighted homogeneity under substitution of homogeneous polynomials

Give the variable i the weight w i, and substitute for it a polynomial that is homogeneous of degree w i. A weighted homogeneous polynomial of weight m then becomes a homogeneous polynomial of degree m. When the substitution is injective the converse holds: a polynomial whose substitution is homogeneous of degree m is itself weighted homogeneous of weight m.

The motivating substitution sends the variable i of MvPolynomial (Fin n) R to the elementary symmetric polynomial eᵢ₊₁, which is homogeneous of degree i + 1 (MvPolynomial.isHomogeneous_esymm). By the fundamental theorem of symmetric polynomials it is injective, so the expression of a homogeneous symmetric polynomial in the elementary symmetric polynomials is weighted homogeneous for the weights i + 1. The coefficients of a product ∏ (X - C Ψ) of linear factors with homogeneous constant terms of a common degree m supply such symmetric polynomials (MvPolynomial.isHomogeneous_coeff_prod_X_sub_C).

Main results

• MvPolynomial.IsWeightedHomogeneous.isHomogeneous_aeval: substituting homogeneous polynomials of the weights turns weighted homogeneity into homogeneity.
• MvPolynomial.isWeightedHomogeneous_of_isHomogeneous_aeval: the converse, for an injective substitution.

theorem MvPolynomial.IsWeightedHomogeneous.isHomogeneous_aeval {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {w : σ → ℕ} {φ : MvPolynomial σ R} {m : ℕ} (hφ : IsWeightedHomogeneous w φ m) {g : σ → MvPolynomial τ R} (hg : ∀ (i : σ), (g i).IsHomogeneous (w i)) : ((aeval g) φ).IsHomogeneous m

Substituting, for each variable i, a polynomial homogeneous of degree w i into a polynomial that is weighted homogeneous of weight m for the weights w gives a homogeneous polynomial of degree m.

theorem MvPolynomial.isWeightedHomogeneous_of_isHomogeneous_aeval {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {w : σ → ℕ} {g : σ → MvPolynomial τ R} (hg : ∀ (i : σ), (g i).IsHomogeneous (w i)) (hinj : Function.Injective ⇑(aeval g)) {φ : MvPolynomial σ R} {m : ℕ} (h : ((aeval g) φ).IsHomogeneous m) : IsWeightedHomogeneous w φ m

Weighted homogeneity from homogeneity of a substitution. If g i is homogeneous of degree w i for every variable i and substitution of the g i is injective, then a polynomial whose substitution is homogeneous of degree m is weighted homogeneous of weight m.