Substitution in symmetric multivariate polynomials

Substituting the same univariate polynomial into every variable of a symmetric multivariate polynomial preserves symmetry. For finitely many variables over a commutative ring, the fundamental theorem of symmetric polynomials then expresses the substituted polynomial in the elementary symmetric polynomials.

Main declarations

• MvPolynomial.IsSymmetric.exists_aeval_esymm: the fundamental theorem of symmetric polynomials, unbundled: a symmetric polynomial is a polynomial in the elementary symmetric polynomials.
• MvPolynomial.IsSymmetric.bind₁_aeval_X: uniform univariate substitution preserves symmetry.
• MvPolynomial.IsSymmetric.exists_aeval_esymm_eq_bind₁_aeval_X: the substituted polynomial is a polynomial in the elementary symmetric polynomials.

theorem MvPolynomial.IsSymmetric.bind₁_aeval_X {σ : Type u_1} {R : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} (hp : p.IsSymmetric) (q : Polynomial R) : ((bind₁ fun (i : σ) => (Polynomial.aeval (X i)) q) p).IsSymmetric

Substituting the same univariate polynomial into every variable of a symmetric multivariate polynomial preserves symmetry.

theorem MvPolynomial.IsSymmetric.exists_aeval_esymm {R : Type u_1} [CommRing R] {n : ℕ} {p : MvPolynomial (Fin n) R} (hp : p.IsSymmetric) : ∃ (W : MvPolynomial (Fin n) R), (aeval fun (j : Fin n) => esymm (Fin n) R (↑j + 1)) W = p

The fundamental theorem of symmetric polynomials, unbundled: a symmetric polynomial in n variables over a commutative ring is a polynomial in the first n elementary symmetric polynomials.

theorem MvPolynomial.IsSymmetric.exists_aeval_esymm_eq_bind₁_aeval_X {R : Type u_1} [CommRing R] {n : ℕ} {p : MvPolynomial (Fin n) R} (hp : p.IsSymmetric) (q : Polynomial R) : ∃ (W : MvPolynomial (Fin n) R), (aeval fun (j : Fin n) => esymm (Fin n) R (↑j + 1)) W = (bind₁ fun (i : Fin n) => (Polynomial.aeval (X i)) q) p

Over a commutative ring, uniformly substituting a univariate polynomial into a symmetric polynomial in n variables yields a polynomial in the first n elementary symmetric polynomials: the substituted polynomial is symmetric by MvPolynomial.IsSymmetric.bind₁_aeval_X, so the fundamental theorem (MvPolynomial.IsSymmetric.exists_aeval_esymm) applies to it.