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

The nth elementary symmetric function evaluated at the elements of s

Equations

• Multiset.esymm s n = Multiset.sum (Multiset.map Multiset.prod (Multiset.powersetLen n s))

theorem Finset.esymm_map_val {R : Type u_1} [CommSemiring R] {σ : Type u_2} (f : σ → R) (s : Finset σ) (n : ℕ) : Multiset.esymm (Multiset.map f s.val) n = Finset.sum (Finset.powersetLen n s) fun t => Finset.prod t f

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

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

Equations

• MvPolynomial.IsSymmetric φ = ∀ (e : Equiv.Perm σ), ↑(MvPolynomial.rename ↑e) φ = φ

def MvPolynomial.symmetricSubalgebra (σ : Type u_1) (R : Type u_2) [CommSemiring R] : Subalgebra R (MvPolynomial σ R)

The subalgebra of symmetric MvPolynomials.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

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

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

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

The nth elementary symmetric MvPolynomial σ R.

Equations

• MvPolynomial.esymm σ R n = Finset.sum (Finset.powersetLen n Finset.univ) fun t => Finset.prod t fun i => MvPolynomial.X i

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

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

theorem MvPolynomial.esymm_eq_sum_subtype (σ : Type u_1) (R : Type u_2) [CommSemiring R] [Fintype σ] (n : ℕ) : MvPolynomial.esymm σ R n = Finset.sum Finset.univ fun t => Finset.prod ↑t fun i => MvPolynomial.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_1) (R : Type u_2) [CommSemiring R] [Fintype σ] (n : ℕ) : MvPolynomial.esymm σ R n = Finset.sum (Finset.powersetLen n Finset.univ) fun t => ↑(MvPolynomial.monomial (Finset.sum t fun i => fun₀ | i => 1)) 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) [CommSemiring R] [Fintype σ] : MvPolynomial.esymm σ R 0 = 1

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

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

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

theorem MvPolynomial.support_esymm'' (σ : Type u_1) (R : Type u_2) [CommSemiring R] [Fintype σ] (n : ℕ) [DecidableEq σ] [Nontrivial R] : MvPolynomial.support (MvPolynomial.esymm σ R n) = Finset.biUnion (Finset.powersetLen n Finset.univ) fun t => (fun₀ | Finset.sum t fun i => fun₀ | i => 1 => 1).support

theorem MvPolynomial.support_esymm' (σ : Type u_1) (R : Type u_2) [CommSemiring R] [Fintype σ] (n : ℕ) [DecidableEq σ] [Nontrivial R] : MvPolynomial.support (MvPolynomial.esymm σ R n) = Finset.biUnion (Finset.powersetLen n Finset.univ) fun t => {Finset.sum t fun i => fun₀ | i => 1}

theorem MvPolynomial.support_esymm (σ : Type u_1) (R : Type u_2) [CommSemiring R] [Fintype σ] (n : ℕ) [DecidableEq σ] [Nontrivial R] : MvPolynomial.support (MvPolynomial.esymm σ R n) = Finset.image (fun t => Finset.sum t fun i => fun₀ | i => 1) (Finset.powersetLen n Finset.univ)

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

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

The degree-n power sum

Equations

• MvPolynomial.psum σ R n = Finset.sum Finset.univ fun i => MvPolynomial.X i ^ n

theorem MvPolynomial.psum_def (σ : Type u_1) (R : Type u_2) [CommSemiring R] [Fintype σ] (n : ℕ) : MvPolynomial.psum σ R n = Finset.sum Finset.univ fun i => MvPolynomial.X i ^ n

@[simp]

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

@[simp]

theorem MvPolynomial.psum_one (σ : Type u_1) (R : Type u_2) [CommSemiring R] [Fintype σ] : MvPolynomial.psum σ R 1 = Finset.sum Finset.univ fun i => MvPolynomial.X i

@[simp]

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

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