Documentation

Mathlib.RingTheory.MvPolynomial.Symmetric

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 #

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
Instances For
    theorem Finset.esymm_map_val {R : Type u_1} [CommSemiring R] {σ : Type u_2} (f : σR) (s : Finset σ) (n : ) :
    def MvPolynomial.IsSymmetric {σ : Type u_1} {R : Type u_2} [CommSemiring R] (φ : MvPolynomial σ R) :

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

    Equations
    Instances For

      The subalgebra of symmetric MvPolynomials.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem MvPolynomial.IsSymmetric.C {σ : Type u_1} {R : Type u_2} [CommSemiring R] (r : R) :
        MvPolynomial.IsSymmetric (MvPolynomial.C r)
        theorem MvPolynomial.IsSymmetric.smul {σ : Type u_1} {R : Type u_2} [CommSemiring R] {φ : MvPolynomial σ R} (r : R) (hφ : MvPolynomial.IsSymmetric φ) :
        @[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) :
        theorem MvPolynomial.IsSymmetric.rename {σ : Type u_1} {R : Type u_2} {τ : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} (hφ : MvPolynomial.IsSymmetric φ) (e : σ τ) :
        @[simp]
        theorem MvPolynomial.isSymmetric_rename {σ : Type u_1} {R : Type u_2} {τ : Type u_3} [CommSemiring R] {φ : MvPolynomial σ R} {e : σ τ} :

        MvPolynomial.rename induces an isomorphism between the symmetric subalgebras.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def MvPolynomial.esymm (σ : Type u_1) (R : Type u_2) [CommSemiring R] [Fintype σ] (n : ) :

          The nth elementary symmetric MvPolynomial σ R.

          Equations
          Instances For
            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 : ) :
            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 : { s : Finset σ // s.card = n }) => 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.powersetCard n Finset.univ) fun (t : Finset σ) => (MvPolynomial.monomial (Finset.sum t 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 σ] :
            theorem MvPolynomial.map_esymm (σ : Type u_1) (R : Type u_2) {S : Type u_4} [CommSemiring R] [CommSemiring S] [Fintype σ] (n : ) (f : R →+* S) :
            theorem MvPolynomial.rename_esymm (σ : Type u_1) (R : Type u_2) {τ : Type u_3} [CommSemiring R] [Fintype σ] [Fintype τ] (n : ) (e : σ τ) :
            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.powersetCard n Finset.univ) fun (t : Finset σ) => (Finsupp.single (Finset.sum t 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.support (MvPolynomial.esymm σ R n) = Finset.biUnion (Finset.powersetCard n Finset.univ) fun (t : Finset σ) => {Finset.sum t 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.support (MvPolynomial.esymm σ R n) = Finset.image (fun (t : Finset σ) => Finset.sum t 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.degrees (MvPolynomial.esymm σ R n) = Finset.univ.val
            def MvPolynomial.psum (σ : Type u_1) (R : Type u_2) [CommSemiring R] [Fintype σ] (n : ) :

            The degree-n power sum

            Equations
            Instances For
              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 σ] :
              @[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 : σ τ) :