Homogeneous substitution with independent coefficient and polynomial variables, and specialization of the resulting coefficient forms.

theorem CCDN.CoefficientwiseHomogeneous.eval₂ {R : Type u_1} {S : Type u_2} {σ : Type u_3} {τ : Type u_4} {υ : Type u_5} [CommRing R] [CommRing S] {φ : MvPolynomial σ R} {m n : ℕ} (hφ : φ.IsHomogeneous m) (f : R →+* MvPolynomial τ (MvPolynomial υ S)) (g : σ → MvPolynomial τ (MvPolynomial υ S)) (hf : ∀ (r : R), CoefficientwiseHomogeneous (f r) 0) (hg : ∀ (i : σ), CoefficientwiseHomogeneous (g i) n) : CoefficientwiseHomogeneous (MvPolynomial.eval₂ f g φ) (n * m)

Substituting coefficientwise homogeneous forms of degree n into a homogeneous polynomial φ of degree m, with constant coefficients mapped to coefficientwise degree 0, gives a coefficientwise homogeneous polynomial of degree n * m.

theorem CCDN.homogeneousCoefficientSpecialization_map {R : Type u_1} {S : Type u_2} {σ : Type u_3} [CommRing R] [CommRing S] [Fintype σ] [DecidableEq σ] (ψ : R →+* S) (d : ℕ) (f : MvPolynomial σ R) (Φ : MvPolynomial (Sym σ d) ℤ) : ψ ((homogeneousCoefficientSpecialization d f) Φ) = (homogeneousCoefficientSpecialization d ((MvPolynomial.map ψ) f)) Φ

Specializing a universal coefficient polynomial Φ at the degree-d coefficients of f commutes with applying a ring homomorphism ψ to the coefficients of f.

theorem CCDN.homogeneousCoefficientSpecialization_homogeneous {σ : Type u_1} {τ : Type u_2} [Fintype σ] [DecidableEq σ] (d e r : ℕ) (f : MvPolynomial σ (MvPolynomial τ ℤ)) (hf : CoefficientwiseHomogeneous f e) (Φ : MvPolynomial (Sym σ d) ℤ) (hΦ : Φ.IsHomogeneous r) : ((homogeneousCoefficientSpecialization d f) Φ).IsHomogeneous (e * r)

If the coefficients of f are homogeneous of degree e in auxiliary variables and Φ is a homogeneous polynomial of degree r in the universal coefficients, then specializing Φ at the degree-d coefficients of f gives a homogeneous polynomial of degree e * r.