Documentation

Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

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 #

Notation #

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

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
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 = tpowersetCard 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) :

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

Equations

The subalgebra of symmetric MvPolynomials.

Equations
@[simp]
theorem MvPolynomial.IsSymmetric.C {σ : Type u_1} {R : Type u_3} [CommSemiring R] (r : R) :
@[simp]
theorem MvPolynomial.IsSymmetric.zero {σ : Type u_1} {R : Type u_3} [CommSemiring R] :
@[simp]
theorem MvPolynomial.IsSymmetric.one {σ : Type u_1} {R : Type u_3} [CommSemiring R] :
theorem MvPolynomial.IsSymmetric.add {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ ψ : MvPolynomial σ R} ( : φ.IsSymmetric) ( : ψ.IsSymmetric) :
(φ + ψ).IsSymmetric
theorem MvPolynomial.IsSymmetric.mul {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ ψ : MvPolynomial σ R} ( : φ.IsSymmetric) ( : ψ.IsSymmetric) :
(φ * ψ).IsSymmetric
theorem MvPolynomial.IsSymmetric.smul {σ : Type u_1} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} (r : R) ( : φ.IsSymmetric) :
@[simp]
theorem MvPolynomial.IsSymmetric.map {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] {φ : MvPolynomial σ R} ( : φ.IsSymmetric) (f : R →+* S) :
theorem MvPolynomial.IsSymmetric.rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} ( : φ.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 : σ τ} :
theorem MvPolynomial.IsSymmetric.neg {σ : Type u_1} {R : Type u_3} [CommRing R] {φ : MvPolynomial σ R} ( : φ.IsSymmetric) :
theorem MvPolynomial.IsSymmetric.sub {σ : Type u_1} {R : Type u_3} [CommRing R] {φ ψ : MvPolynomial σ R} ( : φ.IsSymmetric) ( : ψ.IsSymmetric) :
(φ - ψ).IsSymmetric
def MvPolynomial.renameSymmetricSubalgebra {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (e : σ τ) :

MvPolynomial.rename induces an isomorphism between the symmetric subalgebras.

Equations
  • One or more equations did not get rendered due to their size.
@[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 : ) :

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

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

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

Equations

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) :
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 }, it, 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 = tFinset.powersetCard n Finset.univ, (monomial (∑ it, 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
@[simp]
theorem MvPolynomial.esymmPart_indiscrete (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] (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 : ) :
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 (∑ it, 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 σ) => {it, 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 σ) => it, 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 σ) :
def MvPolynomial.hsymm (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] (n : ) :

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

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

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

Equations
@[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
@[simp]
theorem MvPolynomial.hsymmPart_indiscrete (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] (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 : ) :
def MvPolynomial.psum (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] (n : ) :

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

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

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

Equations
@[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]
@[simp]
theorem MvPolynomial.psumPart_indiscrete (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] {n : } (npos : n 0) :
@[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) :

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
@[simp]
theorem MvPolynomial.msymm_zero (σ : Type u_5) (R : Type u_6) [CommSemiring R] [Fintype σ] [DecidableEq σ] :
@[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