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

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

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 = (Finset.powersetCard n s).sum fun (t : Finset σ) => t.prod 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

• φ.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

• MvPolynomial.symmetricSubalgebra σ R = { carrier := setOf MvPolynomial.IsSymmetric, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

@[simp]

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

@[simp]

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

@[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φ : φ.IsSymmetric) (hψ : ψ.IsSymmetric) : (φ + ψ).IsSymmetric

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

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

@[simp]

theorem MvPolynomial.IsSymmetric.map {σ : Type u_1} {R : Type u_2} {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} {R : Type u_2} {τ : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} (hφ : φ.IsSymmetric) (e : σ ≃ τ) : ((MvPolynomial.rename ⇑e) φ).IsSymmetric

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

MvPolynomial.rename induces an isomorphism between the symmetric subalgebras.

Equations

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

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

theorem MvPolynomial.esymm_eq_sum_subtype (σ : Type u_1) (R : Type u_2) [CommSemiring R] [Fintype σ] (n : ℕ) : MvPolynomial.esymm σ R n = Finset.univ.sum fun (t : { s : Finset σ // s.card = n }) => (↑t).prod 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.powersetCard n Finset.univ).sum fun (t : Finset σ) => (MvPolynomial.monomial (t.sum fun (i : σ) => Finsupp.single 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.esymm σ R n).IsSymmetric

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

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

theorem MvPolynomial.support_esymm (σ : Type u_1) (R : Type u_2) [CommSemiring R] [Fintype σ] (n : ℕ) [DecidableEq σ] [Nontrivial R] : (MvPolynomial.esymm σ R n).support = Finset.image (fun (t : Finset σ) => t.sum fun (i : σ) => Finsupp.single i 1) (Finset.powersetCard 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.esymm σ R n).degrees = 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.univ.sum 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.univ.sum 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.univ.sum 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.psum σ R n).IsSymmetric