Library Combi.MPoly.Schur_mpoly: Schur symmetric polynomials
Combinatorial definition of Schur symmetric polynomials
- Schur n0 R la == The Schur polynomial associated to the partition la in {mpoly R[n0.+1]} as the sum of all tableau of shape la over the alphabet 'I_n0.+1.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg.
From mathcomp Require Import ssrcomplements freeg mpoly.
Require Import tools ordtype partition tableau.
Set Implicit Arguments.
Import Order.TTheory.
#[local] Open Scope ring_scope.
Import GRing.Theory.
Section Schur.
Variable n0 : nat.
#[local] Notation n := n0.+1.
Variable R : ringType.
Lemma mons2mE s : 'X_[s2m s] = \prod_(i <- s) 'X_i :> {mpoly R[n]}.
Definition Schur d (sh : 'P_d) : {mpoly R[n]} :=
\sum_(t : tabsh sh) \prod_(i <- to_word t) 'X_i.
Lemma Schur_tabsh_readingE d (sh : 'P_d) :
Schur sh =
\sum_(t : d.-tuple 'I_n | tabsh_reading sh t) \prod_(i <- t) 'X_i.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg.
From mathcomp Require Import ssrcomplements freeg mpoly.
Require Import tools ordtype partition tableau.
Set Implicit Arguments.
Import Order.TTheory.
#[local] Open Scope ring_scope.
Import GRing.Theory.
Section Schur.
Variable n0 : nat.
#[local] Notation n := n0.+1.
Variable R : ringType.
Lemma mons2mE s : 'X_[s2m s] = \prod_(i <- s) 'X_i :> {mpoly R[n]}.
Definition Schur d (sh : 'P_d) : {mpoly R[n]} :=
\sum_(t : tabsh sh) \prod_(i <- to_word t) 'X_i.
Lemma Schur_tabsh_readingE d (sh : 'P_d) :
Schur sh =
\sum_(t : d.-tuple 'I_n | tabsh_reading sh t) \prod_(i <- t) 'X_i.
Lemma Schur0 (sh : 'P_0) : Schur sh = 1.
Lemma Schur_oversize d (sh : 'P_d) : (size sh > n)%N -> Schur sh = 0.
Equivalent definition of symh symmetric function
Lemma tabwordshape_row d (w : d.-tuple 'I_n) :
tabsh_reading (rowpartn d) w = sorted leq [seq val i | i <- w].
Lemma symh_basisE d :
\sum_(s in basis n d) 'X_[s2m s] = Schur (rowpartn d).
End Schur.
Section SchurComRingType.
Variable n0 : nat.
#[local] Notation n := (n0.+1).
Variable R : comRingType.
Lemma perm_enum_basis d :
perm_eq [seq s2m (tval s) | s in basis n d]
[seq val m | m in [set m : 'X_{1..n < d.+1} | mdeg m == d]].
Lemma Schur_rowpartn d :
\sum_(m : 'X_{1..n < d.+1} | mdeg m == d) 'X_[m] = Schur n0 R (rowpartn d).
The definition of column Schur symmetric polynomials agrees with mesym
from mpoly