Symmetric Polynomials and Elementary Symmetric Polynomials

This file defines symmetric MvPolynomials and the bases of elementary, complete homogeneous, power sum, and monomial symmetric MvPolynomials. We also prove some basic facts about them.

Main declarations

• MvPolynomial.IsSymmetric

• MvPolynomial.symmetricSubalgebra

• MvPolynomial.esymm

• MvPolynomial.hsymm

• MvPolynomial.psum

• MvPolynomial.msymm

Notation

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

• hsymm σ R n is the nth complete homogeneous 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 ∈ σ.

• msymm σ R μ is the monomial symmetric polynomial whose exponents set are the parts of μ ⊢ n in MvPolynomial σ R.

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} [CommSemiring R] (s : Multiset R) (n : ℕ) : R

The nth elementary symmetric function evaluated at the elements of s

theorem Finset.esymm_map_val {R : Type u_1} [CommSemiring R] {σ : Type u_2} (f : σ → R) (s : Finset σ) (n : ℕ) : (Multiset.map f s.val).esymm n = ∑ t ∈ powersetCard n s, t.prod f

theorem Multiset.pow_smul_esymm {R : Type u_1} [CommSemiring R] {S : Type u_2} [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] [SMulCommClass S R R] (s : S) (n : ℕ) (m : Multiset R) : s ^ n • m.esymm n = (map (fun (x : R) => s • x) m).esymm n

@[simp]

theorem Multiset.esymm_pair_one {R : Type u_1} [CommSemiring R] (x y : R) : (x ::ₘ {y}).esymm 1 = x + y

@[simp]

theorem Multiset.esymm_pair_two {R : Type u_1} [CommSemiring R] (x y : R) : (x ::ₘ {y}).esymm 2 = x * y

def MvPolynomial.IsSymmetric {σ : Type u_1} {R : Type u_3} [CommSemiring R] (φ : MvPolynomial σ R) : Prop

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

def MvPolynomial.symmetricSubalgebra (σ : Type u_5) (R : Type u_6) [CommSemiring R] : Subalgebra R (MvPolynomial σ R)

The subalgebra of symmetric MvPolynomials.

@[simp]

theorem MvPolynomial.mem_symmetricSubalgebra {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p : MvPolynomial σ R) : p ∈ symmetricSubalgebra σ R ↔ p.IsSymmetric

@[simp]

theorem MvPolynomial.IsSymmetric.C {σ : Type u_1} {R : Type u_3} [CommSemiring R] (r : R) : (MvPolynomial.C r).IsSymmetric

@[simp]

theorem MvPolynomial.IsSymmetric.zero {σ : Type u_1} {R : Type u_3} [CommSemiring R] : IsSymmetric 0

@[simp]

theorem MvPolynomial.IsSymmetric.one {σ : Type u_1} {R : Type u_3} [CommSemiring R] : IsSymmetric 1

theorem MvPolynomial.IsSymmetric.add {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ ψ : MvPolynomial σ R} (hφ : φ.IsSymmetric) (hψ : ψ.IsSymmetric) : (φ + ψ).IsSymmetric

theorem MvPolynomial.IsSymmetric.mul {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ ψ : MvPolynomial σ R} (hφ : φ.IsSymmetric) (hψ : ψ.IsSymmetric) : (φ * ψ).IsSymmetric

theorem MvPolynomial.IsSymmetric.smul {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} (r : R) (hφ : φ.IsSymmetric) : (r • φ).IsSymmetric

@[simp]

theorem MvPolynomial.IsSymmetric.map {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] {φ : MvPolynomial σ R} (hφ : φ.IsSymmetric) (f : R →+* S) : ((MvPolynomial.map f) φ).IsSymmetric

theorem MvPolynomial.IsSymmetric.rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} (hφ : φ.IsSymmetric) (e : σ ≃ τ) : ((rename ⇑e) φ).IsSymmetric

@[simp]

theorem MvPolynomial.isSymmetric_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {e : σ ≃ τ} : ((rename ⇑e) φ).IsSymmetric ↔ φ.IsSymmetric

theorem MvPolynomial.IsSymmetric.neg {σ : Type u_1} {R : Type u_3} [CommRing R] {φ : MvPolynomial σ R} (hφ : φ.IsSymmetric) : (-φ).IsSymmetric

theorem MvPolynomial.IsSymmetric.sub {σ : Type u_1} {R : Type u_3} [CommRing R] {φ ψ : MvPolynomial σ R} (hφ : φ.IsSymmetric) (hψ : ψ.IsSymmetric) : (φ - ψ).IsSymmetric

def MvPolynomial.renameSymmetricSubalgebra {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (e : σ ≃ τ) : ↥(symmetricSubalgebra σ R) ≃ₐ[R] ↥(symmetricSubalgebra τ R)

MvPolynomial.rename induces an isomorphism between the symmetric subalgebras.

@[simp]

theorem MvPolynomial.renameSymmetricSubalgebra_symm_apply_coe {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (e : σ ≃ τ) (a : ↥(symmetricSubalgebra τ R)) : ↑((renameSymmetricSubalgebra e).symm a) = (rename ⇑e.symm) ↑a

@[simp]

theorem MvPolynomial.renameSymmetricSubalgebra_apply_coe {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (e : σ ≃ τ) (a : ↥(symmetricSubalgebra σ R)) : ↑((renameSymmetricSubalgebra e) a) = (rename ⇑e) ↑a

def MvPolynomial.esymm (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] (n : ℕ) : MvPolynomial σ R

The nth elementary symmetric MvPolynomial σ R. It is the sum over all the degree n squarefree monomials in MvPolynomial σ R.

def MvPolynomial.esymmPart (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] {n : ℕ} (μ : n.Partition) : MvPolynomial σ R

esymmPart is the product of the symmetric polynomials esymm μᵢ, where μ = (μ₁, μ₂, ...) is a partition.

theorem MvPolynomial.esymm_eq_multiset_esymm (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] : esymm σ R = (Multiset.map 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 {S : Type u_4} (σ : Type u_5) (R : Type u_6) [CommSemiring R] [CommSemiring S] [Fintype σ] [Algebra R S] (n : ℕ) (f : σ → S) : (aeval f) (esymm σ R n) = (Multiset.map f Finset.univ.val).esymm n

theorem MvPolynomial.esymm_eq_sum_subtype (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] (n : ℕ) : esymm σ R n = ∑ t : { s : Finset σ // s.card = n }, ∏ i ∈ ↑t, X i

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

theorem MvPolynomial.esymm_eq_sum_monomial (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] (n : ℕ) : esymm σ R n = ∑ t ∈ Finset.powersetCard n Finset.univ, (monomial (∑ i ∈ t, Finsupp.single i 1)) 1

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

@[simp]

theorem MvPolynomial.esymm_zero (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] : esymm σ R 0 = 1

@[simp]

theorem MvPolynomial.esymm_one (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] : esymm σ R 1 = ∑ i : σ, X i

theorem MvPolynomial.esymmPart_zero (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] : esymmPart σ R (Nat.Partition.indiscrete 0) = 1

@[simp]

theorem MvPolynomial.esymmPart_indiscrete (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] (n : ℕ) : esymmPart σ R (Nat.Partition.indiscrete n) = esymm σ R n

theorem MvPolynomial.map_esymm {S : Type u_4} (σ : Type u_5) (R : Type u_6) [CommSemiring R] [CommSemiring S] [Fintype σ] (n : ℕ) (f : R →+* S) : (map f) (esymm σ R n) = esymm σ S n

theorem MvPolynomial.rename_esymm {τ : Type u_2} (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [Fintype τ] (n : ℕ) (e : σ ≃ τ) : (rename ⇑e) (esymm σ R n) = esymm τ R n

theorem MvPolynomial.esymm_isSymmetric (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] (n : ℕ) : (esymm σ R n).IsSymmetric

theorem MvPolynomial.support_esymm'' (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] [Nontrivial R] (n : ℕ) : (esymm σ R n).support = (Finset.powersetCard n Finset.univ).biUnion fun (t : Finset σ) => (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support

theorem MvPolynomial.support_esymm' (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] [Nontrivial R] (n : ℕ) : (esymm σ R n).support = (Finset.powersetCard n Finset.univ).biUnion fun (t : Finset σ) => {∑ i ∈ t, Finsupp.single i 1}

theorem MvPolynomial.support_esymm (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] [Nontrivial R] (n : ℕ) : (esymm σ R n).support = Finset.image (fun (t : Finset σ) => ∑ i ∈ t, Finsupp.single i 1) (Finset.powersetCard n Finset.univ)

theorem MvPolynomial.degrees_esymm (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [Nontrivial R] {n : ℕ} (hpos : 0 < n) (hn : n ≤ Fintype.card σ) : (esymm σ R n).degrees = Finset.univ.val

def MvPolynomial.hsymm (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] (n : ℕ) : MvPolynomial σ R

The nth complete homogeneous symmetric MvPolynomial σ R. It is the sum over all the degree n monomials in MvPolynomial σ R.

def MvPolynomial.hsymmPart (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] {n : ℕ} (μ : n.Partition) : MvPolynomial σ R

hsymmPart is the product of the symmetric polynomials hsymm μᵢ, where μ = (μ₁, μ₂, ...) is a partition.

@[simp]

theorem MvPolynomial.hsymm_zero (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] : hsymm σ R 0 = 1

@[simp]

theorem MvPolynomial.hsymm_one (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] : hsymm σ R 1 = ∑ i : σ, X i

theorem MvPolynomial.hsymmPart_zero (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] : hsymmPart σ R (Nat.Partition.indiscrete 0) = 1

@[simp]

theorem MvPolynomial.hsymmPart_indiscrete (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] (n : ℕ) : hsymmPart σ R (Nat.Partition.indiscrete n) = hsymm σ R n

theorem MvPolynomial.map_hsymm {S : Type u_4} (σ : Type u_5) (R : Type u_6) [CommSemiring R] [CommSemiring S] [Fintype σ] [DecidableEq σ] (n : ℕ) (f : R →+* S) : (map f) (hsymm σ R n) = hsymm σ S n

theorem MvPolynomial.rename_hsymm {τ : Type u_2} (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [Fintype τ] [DecidableEq σ] [DecidableEq τ] (n : ℕ) (e : σ ≃ τ) : (rename ⇑e) (hsymm σ R n) = hsymm τ R n

theorem MvPolynomial.hsymm_isSymmetric (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] (n : ℕ) : (hsymm σ R n).IsSymmetric

def MvPolynomial.psum (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] (n : ℕ) : MvPolynomial σ R

The degree-n power sum symmetric MvPolynomial σ R. It is the sum over all the n-th powers of the variables.

def MvPolynomial.psumPart (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] {n : ℕ} (μ : n.Partition) : MvPolynomial σ R

psumPart is the product of the symmetric polynomials psum μᵢ, where μ = (μ₁, μ₂, ...) is a partition.

@[simp]

theorem MvPolynomial.psum_zero (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] : psum σ R 0 = ↑(Fintype.card σ)

@[simp]

theorem MvPolynomial.psum_one (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] : psum σ R 1 = ∑ i : σ, X i

@[simp]

theorem MvPolynomial.psumPart_zero (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] : psumPart σ R (Nat.Partition.indiscrete 0) = 1

@[simp]

theorem MvPolynomial.psumPart_indiscrete (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] {n : ℕ} (npos : n ≠ 0) : psumPart σ R (Nat.Partition.indiscrete n) = psum σ R n

@[simp]

theorem MvPolynomial.rename_psum {τ : Type u_2} (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [Fintype τ] (n : ℕ) (e : σ ≃ τ) : (rename ⇑e) (psum σ R n) = psum τ R n

theorem MvPolynomial.psum_isSymmetric (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] (n : ℕ) : (psum σ R n).IsSymmetric

def MvPolynomial.msymm (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] {n : ℕ} (μ : n.Partition) : MvPolynomial σ R

The monomial symmetric MvPolynomial σ R with exponent set μ. It is the sum over all the monomials in MvPolynomial σ R such that the multiset of exponents is equal to the multiset of parts of μ.

@[simp]

theorem MvPolynomial.msymm_zero (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] : msymm σ R (Nat.Partition.indiscrete 0) = 1

@[simp]

theorem MvPolynomial.msymm_one (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] : msymm σ R (Nat.Partition.indiscrete 1) = ∑ i : σ, X i

@[simp]

theorem MvPolynomial.rename_msymm {τ : Type u_2} (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [Fintype τ] [DecidableEq σ] [DecidableEq τ] {n : ℕ} (μ : n.Partition) (e : σ ≃ τ) : (rename ⇑e) (msymm σ R μ) = msymm τ R μ

theorem MvPolynomial.msymm_isSymmetric (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] {n : ℕ} (μ : n.Partition) : (msymm σ R μ).IsSymmetric