# Symmetric Polynomials and Elementary Symmetric Polynomials #

This file defines symmetric MvPolynomials and elementary symmetric MvPolynomials. We also prove some basic facts about them.

## Main declarations #

• MvPolynomial.IsSymmetric

• MvPolynomial.symmetricSubalgebra

• MvPolynomial.esymm

• MvPolynomial.psum

## Notation #

• esymm σ R n is the nth elementary symmetric polynomial in MvPolynomial σ R.

• psum σ R n is the degree-n power sum in MvPolynomial σ R, i.e. the sum of monomials (X i)^n over i ∈ σ.

As in other polynomial files, we typically use the notation:

• σ τ : Type* (indexing the variables)

• R S : Type* [CommSemiring R] [CommSemiring S] (the coefficients)

• r : R elements of the coefficient ring

• i : σ, with corresponding monomial X i, often denoted X_i by mathematicians

• φ ψ : MvPolynomial σ R

def Multiset.esymm {R : Type u_1} [] (s : ) (n : ) :
R

The nth elementary symmetric function evaluated at the elements of s

Equations
Instances For
theorem Finset.esymm_map_val {R : Type u_1} [] {σ : Type u_2} (f : σR) (s : ) (n : ) :
(Multiset.map f s.val).esymm n = t, t.prod f
def MvPolynomial.IsSymmetric {σ : Type u_1} {R : Type u_2} [] (φ : ) :

A MvPolynomial φ is symmetric if it is invariant under permutations of its variables by the rename operation

Equations
• φ.IsSymmetric = ∀ (e : ), () φ = φ
Instances For
def MvPolynomial.symmetricSubalgebra (σ : Type u_1) (R : Type u_2) [] :

The subalgebra of symmetric MvPolynomials.

Equations
• = { carrier := setOf MvPolynomial.IsSymmetric, mul_mem' := , one_mem' := , add_mem' := , zero_mem' := , algebraMap_mem' := }
Instances For
@[simp]
theorem MvPolynomial.mem_symmetricSubalgebra {σ : Type u_1} {R : Type u_2} [] (p : ) :
p.IsSymmetric
@[simp]
theorem MvPolynomial.IsSymmetric.C {σ : Type u_1} {R : Type u_2} [] (r : R) :
(MvPolynomial.C r).IsSymmetric
@[simp]
theorem MvPolynomial.IsSymmetric.zero {σ : Type u_1} {R : Type u_2} [] :
@[simp]
theorem MvPolynomial.IsSymmetric.one {σ : Type u_1} {R : Type u_2} [] :
theorem MvPolynomial.IsSymmetric.add {σ : Type u_1} {R : Type u_2} [] {φ : } {ψ : } (hφ : φ.IsSymmetric) (hψ : ψ.IsSymmetric) :
(φ + ψ).IsSymmetric
theorem MvPolynomial.IsSymmetric.mul {σ : Type u_1} {R : Type u_2} [] {φ : } {ψ : } (hφ : φ.IsSymmetric) (hψ : ψ.IsSymmetric) :
(φ * ψ).IsSymmetric
theorem MvPolynomial.IsSymmetric.smul {σ : Type u_1} {R : Type u_2} [] {φ : } (r : R) (hφ : φ.IsSymmetric) :
(r φ).IsSymmetric
@[simp]
theorem MvPolynomial.IsSymmetric.map {σ : Type u_1} {R : Type u_2} {S : Type u_4} [] [] {φ : } (hφ : φ.IsSymmetric) (f : R →+* S) :
(() φ).IsSymmetric
theorem MvPolynomial.IsSymmetric.rename {σ : Type u_1} {R : Type u_2} {τ : Type u_3} [] {φ : } (hφ : φ.IsSymmetric) (e : σ τ) :
(() φ).IsSymmetric
@[simp]
theorem MvPolynomial.isSymmetric_rename {σ : Type u_1} {R : Type u_2} {τ : Type u_3} [] {φ : } {e : σ τ} :
(() φ).IsSymmetric φ.IsSymmetric
theorem MvPolynomial.IsSymmetric.neg {σ : Type u_1} {R : Type u_2} [] {φ : } (hφ : φ.IsSymmetric) :
(-φ).IsSymmetric
theorem MvPolynomial.IsSymmetric.sub {σ : Type u_1} {R : Type u_2} [] {φ : } {ψ : } (hφ : φ.IsSymmetric) (hψ : ψ.IsSymmetric) :
(φ - ψ).IsSymmetric
@[simp]
theorem MvPolynomial.renameSymmetricSubalgebra_apply_coe {σ : Type u_1} {R : Type u_2} {τ : Type u_3} [] (e : σ τ) (a : ) :
= () a
@[simp]
theorem MvPolynomial.renameSymmetricSubalgebra_symm_apply_coe {σ : Type u_1} {R : Type u_2} {τ : Type u_3} [] (e : σ τ) (a : ) :
( a) = (MvPolynomial.rename e.symm) a
def MvPolynomial.renameSymmetricSubalgebra {σ : Type u_1} {R : Type u_2} {τ : Type u_3} [] (e : σ τ) :

MvPolynomial.rename induces an isomorphism between the symmetric subalgebras.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MvPolynomial.esymm (σ : Type u_1) (R : Type u_2) [] [] (n : ) :

The nth elementary symmetric MvPolynomial σ R.

Equations
Instances For
theorem MvPolynomial.esymm_eq_multiset_esymm (σ : Type u_1) (R : Type u_2) [] [] :
= (Multiset.map MvPolynomial.X Finset.univ.val).esymm

The nth elementary symmetric MvPolynomial σ R is obtained by evaluating the nth elementary symmetric at the Multiset of the monomials

theorem MvPolynomial.aeval_esymm_eq_multiset_esymm (σ : Type u_1) (R : Type u_2) {S : Type u_4} [] [] [] [Algebra R S] (f : σS) (n : ) :
() = (Multiset.map f Finset.univ.val).esymm n
theorem MvPolynomial.esymm_eq_sum_subtype (σ : Type u_1) (R : Type u_2) [] [] (n : ) :
= t : { s : // s.card = n }, it,

We can define esymm σ R n by summing over a subtype instead of over powerset_len.

theorem MvPolynomial.esymm_eq_sum_monomial (σ : Type u_1) (R : Type u_2) [] [] (n : ) :
= tFinset.powersetCard n Finset.univ, (MvPolynomial.monomial (it, )) 1

We can define esymm σ R n as a sum over explicit monomials

@[simp]
theorem MvPolynomial.esymm_zero (σ : Type u_1) (R : Type u_2) [] [] :
= 1
theorem MvPolynomial.map_esymm (σ : Type u_1) (R : Type u_2) {S : Type u_4} [] [] [] (n : ) (f : R →+* S) :
() () =
theorem MvPolynomial.rename_esymm (σ : Type u_1) (R : Type u_2) {τ : Type u_3} [] [] [] (n : ) (e : σ τ) :
() () =
theorem MvPolynomial.esymm_isSymmetric (σ : Type u_1) (R : Type u_2) [] [] (n : ) :
().IsSymmetric
theorem MvPolynomial.support_esymm'' (σ : Type u_1) (R : Type u_2) [] [] (n : ) [] [] :
().support = (Finset.powersetCard n Finset.univ).biUnion fun (t : ) => (Finsupp.single (it, ) 1).support
theorem MvPolynomial.support_esymm' (σ : Type u_1) (R : Type u_2) [] [] (n : ) [] [] :
().support = (Finset.powersetCard n Finset.univ).biUnion fun (t : ) => {it, }
theorem MvPolynomial.support_esymm (σ : Type u_1) (R : Type u_2) [] [] (n : ) [] [] :
().support = Finset.image (fun (t : ) => it, ) (Finset.powersetCard n Finset.univ)
theorem MvPolynomial.degrees_esymm (σ : Type u_1) (R : Type u_2) [] [] [] (n : ) (hpos : 0 < n) (hn : ) :
().degrees = Finset.univ.val
def MvPolynomial.psum (σ : Type u_1) (R : Type u_2) [] [] (n : ) :

The degree-n power sum

Equations
• = i : σ,
Instances For
theorem MvPolynomial.psum_def (σ : Type u_1) (R : Type u_2) [] [] (n : ) :
= i : σ,
@[simp]
theorem MvPolynomial.psum_zero (σ : Type u_1) (R : Type u_2) [] [] :
= ()
@[simp]
theorem MvPolynomial.psum_one (σ : Type u_1) (R : Type u_2) [] [] :
= i : σ,
@[simp]
theorem MvPolynomial.rename_psum (σ : Type u_1) (R : Type u_2) {τ : Type u_3} [] [] [] (n : ) (e : σ τ) :
() () =
theorem MvPolynomial.psum_isSymmetric (σ : Type u_1) (R : Type u_2) [] [] (n : ) :
().IsSymmetric