# Symmetric Polynomials and Elementary Symmetric Polynomials #

This file defines symmetric `MvPolynomial`s and the bases of elementary, complete homogeneous, power sum, and monomial symmetric `MvPolynomial`s. 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 `n`th elementary symmetric polynomial in `MvPolynomial σ R`.

- `hsymm σ R n` is the `n`th 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`

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

The `n`th elementary symmetric function evaluated at the elements of `s`

Equations

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

Instances For

source
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
source
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
source
@[simp]
theorem Multiset.esymm_pair_one {R : Type u_1} [CommSemiring R] (x y : R) :
(x ::ₘ {y}).esymm 1 = x + y
source
@[simp]
theorem Multiset.esymm_pair_two {R : Type u_1} [CommSemiring R] (x y : R) :
(x ::ₘ {y}).esymm 2 = x * y
source
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

Equations

- φ.IsSymmetric = ∀ (e : Equiv.Perm σ), (MvPolynomial.rename ⇑e) φ = φ

Instances For

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

The subalgebra of symmetric `MvPolynomial`s.

Equations

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

Instances For

source
@[simp]
theorem MvPolynomial.mem_symmetricSubalgebra {σ : Type u_1} {R : Type u_3} [CommSemiring R] (p : MvPolynomial σ R) :
p ∈ symmetricSubalgebra σ R ↔ p.IsSymmetric
source
@[simp]
theorem MvPolynomial.IsSymmetric.C {σ : Type u_1} {R : Type u_3} [CommSemiring R] (r : R) :
(MvPolynomial.C r).IsSymmetric
source
@[simp]
theorem MvPolynomial.IsSymmetric.zero {σ : Type u_1} {R : Type u_3} [CommSemiring R] :
IsSymmetric 0
source
@[simp]
theorem MvPolynomial.IsSymmetric.one {σ : Type u_1} {R : Type u_3} [CommSemiring R] :
IsSymmetric 1
source
theorem MvPolynomial.IsSymmetric.add {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ ψ : MvPolynomial σ R} (hφ : φ.IsSymmetric) (hψ : ψ.IsSymmetric) :
(φ + ψ).IsSymmetric
source
theorem MvPolynomial.IsSymmetric.mul {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ ψ : MvPolynomial σ R} (hφ : φ.IsSymmetric) (hψ : ψ.IsSymmetric) :
(φ * ψ).IsSymmetric
source
theorem MvPolynomial.IsSymmetric.smul {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} (r : R) (hφ : φ.IsSymmetric) :
(r • φ).IsSymmetric
source
@[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
source
theorem MvPolynomial.IsSymmetric.rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} (hφ : φ.IsSymmetric) (e : σ ≃ τ) :
((rename ⇑e) φ).IsSymmetric
source
@[simp]
theorem MvPolynomial.isSymmetric_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {e : σ ≃ τ} :
((rename ⇑e) φ).IsSymmetric ↔ φ.IsSymmetric
source
theorem MvPolynomial.IsSymmetric.neg {σ : Type u_1} {R : Type u_3} [CommRing R] {φ : MvPolynomial σ R} (hφ : φ.IsSymmetric) :
(-φ).IsSymmetric
source
theorem MvPolynomial.IsSymmetric.sub {σ : Type u_1} {R : Type u_3} [CommRing R] {φ ψ : MvPolynomial σ R} (hφ : φ.IsSymmetric) (hψ : ψ.IsSymmetric) :
(φ - ψ).IsSymmetric
source
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.

Equations

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

Instances For

source
@[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
source
@[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
source
def MvPolynomial.esymm (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] (n : ℕ) :
MvPolynomial σ R

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

Equations

- MvPolynomial.esymm σ R n = ∑ t ∈ Finset.powersetCard n Finset.univ, ∏ i ∈ t, MvPolynomial.X i

Instances For

source
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.

Equations

- MvPolynomial.esymmPart σ R μ = (Multiset.map (MvPolynomial.esymm σ R) μ.parts).prod

Instances For

source
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 `n`th elementary symmetric `MvPolynomial σ R` is obtained by evaluating the `n`th elementary symmetric at the `Multiset` of the monomials

source
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
source
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`.

source
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

source
@[simp]
theorem MvPolynomial.esymm_zero (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] :
esymm σ R 0 = 1
source
@[simp]
theorem MvPolynomial.esymm_one (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] :
esymm σ R 1 = ∑ i : σ, X i
source
theorem MvPolynomial.esymmPart_zero (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] :
esymmPart σ R (Nat.Partition.indiscrete 0) = 1
source
@[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
source
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
source
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
source
theorem MvPolynomial.esymm_isSymmetric (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] (n : ℕ) :
(esymm σ R n).IsSymmetric
source
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
source
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}
source
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)
source
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
source
def MvPolynomial.hsymm (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] (n : ℕ) :
MvPolynomial σ R

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

Equations

- MvPolynomial.hsymm σ R n = ∑ s : Sym σ n, (Multiset.map MvPolynomial.X ↑s).prod

Instances For

source
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.

Equations

- MvPolynomial.hsymmPart σ R μ = (Multiset.map (MvPolynomial.hsymm σ R) μ.parts).prod

Instances For

source
@[simp]
theorem MvPolynomial.hsymm_zero (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] :
hsymm σ R 0 = 1
source
@[simp]
theorem MvPolynomial.hsymm_one (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] :
hsymm σ R 1 = ∑ i : σ, X i
source
theorem MvPolynomial.hsymmPart_zero (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] :
hsymmPart σ R (Nat.Partition.indiscrete 0) = 1
source
@[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
source
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
source
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
source
theorem MvPolynomial.hsymm_isSymmetric (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] (n : ℕ) :
(hsymm σ R n).IsSymmetric
source
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.

Equations

- MvPolynomial.psum σ R n = ∑ i : σ, MvPolynomial.X i ^ n

Instances For

source
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.

Equations

- MvPolynomial.psumPart σ R μ = (Multiset.map (MvPolynomial.psum σ R) μ.parts).prod

Instances For

source
@[simp]
theorem MvPolynomial.psum_zero (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] :
psum σ R 0 = ↑(Fintype.card σ)
source
@[simp]
theorem MvPolynomial.psum_one (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] :
psum σ R 1 = ∑ i : σ, X i
source
@[simp]
theorem MvPolynomial.psumPart_zero (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] :
psumPart σ R (Nat.Partition.indiscrete 0) = 1
source
@[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
source
@[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
source
theorem MvPolynomial.psum_isSymmetric (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] (n : ℕ) :
(psum σ R n).IsSymmetric
source
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 μ.

Equations

- MvPolynomial.msymm σ R μ = ∑ s : { a : Sym σ n // Nat.Partition.ofSym a = μ }, (Multiset.map MvPolynomial.X ↑↑s).prod

Instances For

source
@[simp]
theorem MvPolynomial.msymm_zero (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] :
msymm σ R (Nat.Partition.indiscrete 0) = 1
source
@[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
source
@[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 μ
source
theorem MvPolynomial.msymm_isSymmetric (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] {n : ℕ} (μ : n.Partition) :
(msymm σ R μ).IsSymmetric