Symmetric Polynomials and Elementary Symmetric Polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines symmetric mv_polynomials and elementary symmetric mv_polynomials. We also prove some basic facts about them.

Main declarations #

Notation #

esymm σ R n, is the nth elementary symmetric polynomial in mv_polynomial σ R.

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

σ τ : Type* (indexing the variables)
R S : Type* [comm_semiring R] [comm_semiring S] (the coefficients)
r : R elements of the coefficient ring
i : σ, with corresponding monomial X i, often denoted X_i by mathematicians
φ ψ : mv_polynomial σ R

source

def multiset.esymm {R : Type u_1} [comm_semiring R] (s : multiset R) (n : ℕ) :

The nth elementary symmetric function evaluated at the elements of s

Equations

s.esymm n = (multiset.map multiset.prod (multiset.powerset_len n s)).sum

source

theorem finset.esymm_map_val {R : Type u_1} [comm_semiring R] {σ : Type u_2} (f : σ → R) (s : finset σ) (n : ℕ) :

(multiset.map f s.val).esymm n = (finset.powerset_len n s).sum (λ (t : finset σ), t.prod f)

source

def mv_polynomial.is_symmetric {σ : Type u_1} {R : Type u_2} [comm_semiring R] (φ : mv_polynomial σ R) :

Prop

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

Equations

φ.is_symmetric = ∀ (e : equiv.perm σ), ⇑(mv_polynomial.rename ⇑e) φ = φ

source

def mv_polynomial.symmetric_subalgebra (σ : Type u_1) (R : Type u_2) [comm_semiring R] :

subalgebra R (mv_polynomial σ R)

The subalgebra of symmetric mv_polynomials.

Equations

mv_polynomial.symmetric_subalgebra σ R = {carrier := set_of mv_polynomial.is_symmetric, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}

source

@[simp]

theorem mv_polynomial.mem_symmetric_subalgebra {σ : Type u_1} {R : Type u_2} [comm_semiring R] (p : mv_polynomial σ R) :

p ∈ mv_polynomial.symmetric_subalgebra σ R ↔ p.is_symmetric

source

@[simp]

theorem mv_polynomial.is_symmetric.C {σ : Type u_1} {R : Type u_2} [comm_semiring R] (r : R) :

(⇑mv_polynomial.C r).is_symmetric

source

@[simp]

theorem mv_polynomial.is_symmetric.zero {σ : Type u_1} {R : Type u_2} [comm_semiring R] :

0.is_symmetric

source

@[simp]

theorem mv_polynomial.is_symmetric.one {σ : Type u_1} {R : Type u_2} [comm_semiring R] :

1.is_symmetric

source

theorem mv_polynomial.is_symmetric.add {σ : Type u_1} {R : Type u_2} [comm_semiring R] {φ ψ : mv_polynomial σ R} (hφ : φ.is_symmetric) (hψ : ψ.is_symmetric) :

(φ + ψ).is_symmetric

source

theorem mv_polynomial.is_symmetric.mul {σ : Type u_1} {R : Type u_2} [comm_semiring R] {φ ψ : mv_polynomial σ R} (hφ : φ.is_symmetric) (hψ : ψ.is_symmetric) :

(φ * ψ).is_symmetric

source

theorem mv_polynomial.is_symmetric.smul {σ : Type u_1} {R : Type u_2} [comm_semiring R] {φ : mv_polynomial σ R} (r : R) (hφ : φ.is_symmetric) :

(r • φ).is_symmetric

source

@[simp]

theorem mv_polynomial.is_symmetric.map {σ : Type u_1} {R : Type u_2} {S : Type u_4} [comm_semiring R] [comm_semiring S] {φ : mv_polynomial σ R} (hφ : φ.is_symmetric) (f : R →+* S) :

(⇑(mv_polynomial.map f) φ).is_symmetric

source

theorem mv_polynomial.is_symmetric.neg {σ : Type u_1} {R : Type u_2} [comm_ring R] {φ : mv_polynomial σ R} (hφ : φ.is_symmetric) :

(-φ).is_symmetric

source

theorem mv_polynomial.is_symmetric.sub {σ : Type u_1} {R : Type u_2} [comm_ring R] {φ ψ : mv_polynomial σ R} (hφ : φ.is_symmetric) (hψ : ψ.is_symmetric) :

(φ - ψ).is_symmetric

source

noncomputable def mv_polynomial.esymm (σ : Type u_1) (R : Type u_2) [comm_semiring R] [fintype σ] (n : ℕ) :

mv_polynomial σ R

The nth elementary symmetric mv_polynomial σ R.

Equations

mv_polynomial.esymm σ R n = (finset.powerset_len n finset.univ).sum (λ (t : finset σ), t.prod (λ (i : σ), mv_polynomial.X i))

source

theorem mv_polynomial.esymm_eq_multiset_esymm (σ : Type u_1) (R : Type u_2) [comm_semiring R] [fintype σ] :

mv_polynomial.esymm σ R = (multiset.map mv_polynomial.X finset.univ.val).esymm

The nth elementary symmetric mv_polynomial σ R is obtained by evaluating the nth elementary symmetric at the multiset of the monomials

source

theorem mv_polynomial.aeval_esymm_eq_multiset_esymm (σ : Type u_1) (R : Type u_2) {S : Type u_4} [comm_semiring R] [comm_semiring S] [fintype σ] [algebra R S] (f : σ → S) (n : ℕ) :

⇑(mv_polynomial.aeval f) (mv_polynomial.esymm σ R n) = (multiset.map f finset.univ.val).esymm n

source

theorem mv_polynomial.esymm_eq_sum_subtype (σ : Type u_1) (R : Type u_2) [comm_semiring R] [fintype σ] (n : ℕ) :

mv_polynomial.esymm σ R n = finset.univ.sum (λ (t : {s // s.card = n}), ↑t.prod (λ (i : σ), mv_polynomial.X i))

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

source

theorem mv_polynomial.esymm_eq_sum_monomial (σ : Type u_1) (R : Type u_2) [comm_semiring R] [fintype σ] (n : ℕ) :

mv_polynomial.esymm σ R n = (finset.powerset_len n finset.univ).sum (λ (t : finset σ), ⇑(mv_polynomial.monomial (t.sum (λ (i : σ), finsupp.single i 1))) 1)

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

source

@[simp]

theorem mv_polynomial.esymm_zero (σ : Type u_1) (R : Type u_2) [comm_semiring R] [fintype σ] :

mv_polynomial.esymm σ R 0 = 1

source

theorem mv_polynomial.map_esymm (σ : Type u_1) (R : Type u_2) {S : Type u_4} [comm_semiring R] [comm_semiring S] [fintype σ] (n : ℕ) (f : R →+* S) :

⇑(mv_polynomial.map f) (mv_polynomial.esymm σ R n) = mv_polynomial.esymm σ S n

source

theorem mv_polynomial.rename_esymm (σ : Type u_1) (R : Type u_2) {τ : Type u_3} [comm_semiring R] [fintype σ] [fintype τ] (n : ℕ) (e : σ ≃ τ) :

⇑(mv_polynomial.rename ⇑e) (mv_polynomial.esymm σ R n) = mv_polynomial.esymm τ R n

source

theorem mv_polynomial.esymm_is_symmetric (σ : Type u_1) (R : Type u_2) [comm_semiring R] [fintype σ] (n : ℕ) :

(mv_polynomial.esymm σ R n).is_symmetric

source

theorem mv_polynomial.support_esymm'' (σ : Type u_1) (R : Type u_2) [comm_semiring R] [fintype σ] (n : ℕ) [decidable_eq σ] [nontrivial R] :

(mv_polynomial.esymm σ R n).support = (finset.powerset_len n finset.univ).bUnion (λ (t : finset σ), (finsupp.single (t.sum (λ (i : σ), finsupp.single i 1)) 1).support)

source

theorem mv_polynomial.support_esymm' (σ : Type u_1) (R : Type u_2) [comm_semiring R] [fintype σ] (n : ℕ) [decidable_eq σ] [nontrivial R] :

(mv_polynomial.esymm σ R n).support = (finset.powerset_len n finset.univ).bUnion (λ (t : finset σ), {t.sum (λ (i : σ), finsupp.single i 1)})

source

theorem mv_polynomial.support_esymm (σ : Type u_1) (R : Type u_2) [comm_semiring R] [fintype σ] (n : ℕ) [decidable_eq σ] [nontrivial R] :

(mv_polynomial.esymm σ R n).support = finset.image (λ (t : finset σ), t.sum (λ (i : σ), finsupp.single i 1)) (finset.powerset_len n finset.univ)

source

theorem mv_polynomial.degrees_esymm (σ : Type u_1) (R : Type u_2) [comm_semiring R] [fintype σ] [nontrivial R] (n : ℕ) (hpos : 0 < n) (hn : n ≤ fintype.card σ) :

(mv_polynomial.esymm σ R n).degrees = finset.univ.val