Library Combi.MPoly.Schur_altdef: Alternants definition of Schur polynomials

Definition of Schur polynomials as quotient of alternant and Kostka numbers

In the combinatorial definitions below, we use the following notations:

n : an integer denoting the number of variable.
la mu : partitions of an integer d
m : a monomial for the ring of polynomials {mpoly R[n]}
w : a sequence of 'I_n
t : a tableau

We define the following notions:

add_mesym la S == for a set S of 'I_n the partition obtained by incrementing the parts in S if its a partition. If not the value is unspecified.
setdiff la mu == the set of elements i of 'I_n for which the i-th part of la is smaller than the one of mu.

Kostka numbers:

eval w == the evaluation of w as a n.-tuple nat.
KostkaTab la m == the set of tableaux of shape la and evaluation m.
KostkaMon la m == the number of Kostka tableau : #|KostkaTab la m|.
Kostka la mu ==
'K(la, mu) == the Kostka number associated to la and mu as a nat in nat_scope and as an element of R (inferred from the context) in ring_scope.
Kostak_rec la mu == a Coq implementation of the computation of the Kostka number. It suppose that sumn la = sumn mu.
'K^-1(la, mu) == the inverse Kostka number, that is the coefficient of the inverse Kostka matrix computed using matrix inversion.
eqeval t la == the evaluation of t is la. More precisely, the evaluation of the row reading of the tableau t is equal to the monomial associated to la

Kostka numbers and standard tableaux:

In this section, we fix two nat n and d with hypothesis Hd : d <= n.+1.

tabnat_of_ord Hd t == the standard tableau of shape la corresponding to the tableau t : tabsh n la
tabord_of_nat Hd t == the tableau over 'I_n.+1 of shape la corresponding to t : stdtabsh la

Extension of tableaux:

In this section, we fix

a non empty sequence of integer rcons s m whose size is less than n.
la : a partition of sumn s whose size is less than n.
mu : a partition of (sumn s) + m whose size is less than n.

We are given some proofs Hs Hla Hmu that all these partition are of size less than n. We suppose moreover that mu/la is an horizontal border strip. The proof is denoted Hstrip.

We denote by

T : any tableau of shape la and evaluation s.
Tm : any tableau of shape mu and evaluation rcons s m.

Then we define:

shape_res_tab Hsz Tm == the shape obtained by removing from Tm the boxes containing size s
res_tab Hsz Hmu Hstrip Tm == the tableau obtained by removing from Tm the boxes containing size s if its of shape la. Otherwise the result is unspecified.
ext_tab Hsz Hmu Hstrip T == the tableau obtained by filling the boxes of mu/la with size s.

Then ext_tab and res_tab are two inverse bijections.

From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg ssrint fingroup perm.
From mathcomp Require Import mpoly.

Require Import tools combclass ordtype sorted partition tableau.
Require Import skewpart skewtab antisym Schur_mpoly freeSchur therule.
Require Import std stdtab unitriginv presentSn.

Set Implicit Arguments.

Import Order.TTheory.
Import GRing.Theory.

#[local] Open Scope ring_scope.
#[local] Open Scope Combi_scope.

#[local] Reserved Notation "''a_' k"
      (at level 8, k at level 2, format "''a_' k").
#[local] Reserved Notation "''e_' k"
      (at level 8, k at level 2, format "''e_' k").
#[local] Reserved Notation "m # s"
      (at level 40, left associativity, format "m # s").

Alternating and symmetric polynomial

Section Alternant.

Variables (n : nat) (R : comRingType).

#[local] Notation rho := (rho n).
#[local] Notation "''e_' k" := (mesym n R k).
#[local] Notation "''a_' k" := (@alternpol n R 'X_[k]).

Lemma alt_syme (m : 'X_{1..n}) k :
  'a_(m + rho ) * 'e_k =
  \sum_(h : {set 'I_n} | #|h| == k) 'a_(m + mesym1 h + rho ).

#[local] Open Scope nat_scope.

Section HasIncr.

Variables (d k : nat) (la : 'P_d) (h : {set 'I_n}).

#[local] Definition hasincr :=
  has (fun i => (nth 0 (mpart la + mesym1 h)%MM i).+1 ==
                 nth 0 (mpart la + mesym1 h)%MM i.+1) (iota 0 n.-1).

Lemma hasincr0 : hasincr -> 'a_(mpart la + mesym1 h + rho ) = 0%R :> {mpoly R[n]}.

Lemma not_hasincr_part :
  size la <= n -> ~~ hasincr ->
  is_part_of_n (d + #|h|) (rem_trail0 (mpart la + mesym1 h)%MM).

Let add_mpart_mesym :=
  if [&& size la <= n , #|h| == k & ~~ hasincr ]
  then (rem_trail0 (mpart la + mesym1 h)%MM)
  else rowpartn (d + k) .
Lemma add_mpart_mesymP : is_part_of_n (d + k) add_mpart_mesym.
Definition add_mesym : 'P_(d + k ) := IntPartN add_mpart_mesymP.

Lemma add_mesymE :
  size la <= n -> #|h| == k -> ~~ hasincr ->
  mpart add_mesym = (mpart la + mesym1 h)%MM.

End HasIncr.

Definition setdiff (la mu : seq nat) : {set 'I_n} :=
  [set i : 'I_n | nth 0 la i < nth 0 mu i].

Lemma card_setdiff d k (la : 'P_d) (mu : 'P_(d + k )) :
  size mu <= n -> size la <= n -> vb_strip la mu -> #|setdiff la mu| = k.

Lemma nth_add_setdiff d k (la : 'P_d) (mu : 'P_(d + k )) :
  size mu <= n -> size la <= n -> vb_strip la mu ->
  forall i,
  nth 0 [seq (mpart la) i0 + (mesym1 (setdiff la mu)) i0 | i0 : 'I_n] i =
  nth 0 mu i.

Lemma nohasincr_setdiff d k (la : 'P_d) (mu : 'P_(d + k )) :
  size mu <= n -> size la <= n ->
  vb_strip la mu -> ~~ hasincr la (setdiff la mu).

Lemma add_mesymK d k (la : 'P_d) :
  size la <= n ->
  {in [pred mu : 'P_(d + k ) | vb_strip la mu && (size mu <= n )],
  cancel (fun mu : 'P_(d + k ) => setdiff la (val mu)) (add_mesym k la)}.

Piery's rule for alternating polynomials

Theorem alt_mpart_syme d (la : 'P_d) k :
  size la <= n ->
  ('a_(mpart la + rho ) * 'e_k =
  \sum_(mu : 'P_(d + k ) | vb_strip la mu && (size mu <= n ))
     'a_(mpart mu + rho ))%R.

Lemma vb_strip_rem_col0 d (la : 'P_d) :
  vb_strip (conj_part (behead (conj_part la))) la.

Lemma vb_strip_lexi (d1 k : nat) (la : 'P_(d1 + k )) (mu : seq nat) :
  vb_strip mu la ->
  sumn mu = d1 ->
  is_part mu -> (val la <= incr_first_n mu k :> seqlexi nat)%O.

End Alternant.

Jacobi's definition of schur function

Section SchurAlternantDef.

Variable (n0 : nat) (R : comRingType).
#[local] Notation n := (n0.+1).
#[local] Notation rho := (rho n).
#[local] Notation "''s_[' k ']'" := (Schur n0 R k).
#[local] Notation "''a_' k" := (@alternpol n R 'X_[k]).

Lemma Schur_cast d d' (la : 'P_d) (Heq : d = d') :
  Schur n0 R (cast_intpartn Heq la) = 's_[la ].

Theorem alt_SchurE d (la : 'P_d) :
  size la <= n -> 'a_rho * 's_[la ] = 'a_(mpart la + rho ).

Import LeqGeqOrder.

Lemma mcoeff_alt_SchurE d (la mu : 'P_d) :
  size la <= n -> size mu <= n ->
  ('a_rho * Schur n0 R la)@_(mpart mu + rho) = (la == mu)%:R.

End SchurAlternantDef.

Schur polynomials are symmetric at last

Section IdomainSchurSym.

Variable (n0 : nat) (R : idomainType).
#[local] Notation n := (n0.+1).
#[local] Notation rho := (rho n).
#[local] Notation "''s_' k" := (Schur n0 R k).
#[local] Notation "''a_' k" := (@alternpol n R 'X_[k]).

Theorem alt_uniq d (la : 'P_d) (s : {mpoly R[n]}) :
size la <= n -> 'a_rho * s = 'a_(mpart la + rho ) -> s = 's_la.

Theorem Schur_sym_idomain d (la : 'P_d) : 's_la \is symmetric.

End IdomainSchurSym.

Section RingSchurSym.

Variable (n0 : nat) (R : ringType).
#[local] Notation n := (n0.+1).
#[local] Notation "''s_' k" := (Schur n0 R k).

Theorem Schur_sym d (la : 'P_d) : 's_la \is symmetric.

Lemma Schur_homog (d : nat) (la : 'P_d) : 's_la \is d.-homog.

End RingSchurSym.

Kostka numbers

#[local] Open Scope nat_scope.

Section DefsKostkaMon.

Variables (d : nat) (la : 'P_d) (n : nat).
Implicit Type m : 'X_{1..n.+1}.
Definition eval (w : seq 'I_n.+1) := [tuple count_mem i w | i < n.+1].
Definition KostkaTab m := [set t : tabsh la | eval (to_word t) == m].
Definition KostkaMon m := #|KostkaTab m|.

Lemma sumn_eval w : sumn (eval w) = size w.

Lemma KostkaMon_sumeval m :
  mdeg m != sumn la -> KostkaMon m = 0.

Lemma evalE (R : ringType) m w :
  (\prod_(v <- w) 'X_v)@_m = (eval w == m)%:R :> R.

Lemma Kostka_Coeff (R : ringType) m : (Schur n R la)@_m = (KostkaMon m)%:R.

Lemma perm_KostkaMon m1 m2 :
  perm_eq m1 m2 -> KostkaMon m1 = KostkaMon m2.

Lemma tab_eval_partdom (t : tabsh la) : partdom (eval (to_word t)) la.

Lemma KostkaMon_partdom m : KostkaMon m != 0 -> partdom m la.

End DefsKostkaMon.

Section KostkaEq.

Variables (d : nat) (la : 'P_d).

Lemma Kostka_mnmwiden n (m : 'X_{1..n.+1}) :
  KostkaMon la m = KostkaMon la (mnmwiden m).

End KostkaEq.

Section Kostka.

Variable d : nat.
Implicit Type la : 'P_d.

Definition Kostka la mu :=
  KostkaMon la (mpart (n := (size mu).-1.+1) mu).
#[local] Notation "''K' ( la , mu )" := (Kostka la mu)
  (at level 8, format "''K' ( la , mu )") : nat_scope.
#[local] Notation "''K' ( la , mu )" := ((Kostka la mu)%:R : int)
  (at level 8, format "''K' ( la , mu )") : ring_scope.

#[local] Arguments mpart n s : clear implicits.

Lemma mpartS n mu :
  size mu <= n -> mnmwiden (mpart n mu) = mpart n.+1 mu.

Lemma Kostka_any la mu n :
  size mu <= n.+1 -> 'K (la , mu ) = KostkaMon la (mpart n.+1 mu).

Lemma Kostka_sumnE la mu : d != sumn mu -> Kostka la mu = 0.

Lemma Kostka_size0 la mu :
  size la > size mu -> 'K (la , mu ) = 0.

Lemma Kostka_partdom (la mu : 'PDom_d) : 'K (la , mu ) != 0 -> (mu <= la)%O.

Lemma Kostka0 (la mu : 'PDom_d) : ~~ (mu <= la)%O -> 'K (la , mu ) = 0.

Lemma Kostka_diag la : 'K (la , la ) = 1.

End Kostka.

Converting between standard tableau and tableau over 'I_n.

The type stdtabsh sh is a subtype of seq nat whereas tabsh sh is a subtype of seq 'I_n.+1. We provide two conversion functions tabnat_of_ord and tabord_of_nat

Section StdKostka.

Variables (d : nat) (la : 'P_d).

Section Nvar.

Variable n : nat.
Hypothesis Hd : d <= n.+1.

Let td := [tuple ((i < d ) : nat) | i < n.+1].

Lemma stdtabsh_eval_to_word (t : stdtabsh la) :
  eval [seq inord i | i <- to_word t] = td.

Lemma tabsh_is_std (t : tabsh la) :
  eval (to_word t) = td -> is_std [seq (i : nat) | i : 'I_n .+1 <- to_word t].

Definition tabnat_of_ord_fun (t : tabsh la) :=
  if (eval (to_word t) == td )
  then [seq [seq (i : nat) | i : 'I_n .+1 <- r] | r <- t]
  else hyper_stdtabsh la.

Definition tabord_of_nat_fun (t : stdtabsh la) : seq (seq 'I_n.+1) :=
  [seq map inord r | r <- t].

Lemma tabnat_of_ord_subproof (t : tabsh la) :
  is_stdtab_of_shape la (tabnat_of_ord_fun t).
Definition tabnat_of_ord (t : tabsh la) :=
  StdtabSh (sh := la) (tabnat_of_ord_subproof t).

Lemma tabord_of_nat_subproof (t : stdtabsh la) :
  is_tab_of_shape la (tabord_of_nat_fun t).
Definition tabord_of_nat (t : stdtabsh la) :=
  TabSh (sh := la) (tabord_of_nat_subproof t).

Lemma tabord_of_natK : cancel tabord_of_nat tabnat_of_ord.

Lemma tabnat_of_ordK :
  {in [pred t : tabsh la | eval (to_word t) == td ],
   cancel tabnat_of_ord tabord_of_nat }.

End Nvar.

Lemma KostkaStd : Kostka la (colpartn d) = #|{: stdtabsh la }|.

End StdKostka.

Definition eqeval n (t : (seq (seq 'I_n.+1))) (la : seq nat) :=
  eval (to_word t) == mpart la.

Lemma eqevalP n (t : (seq (seq 'I_n.+1))) (la : seq nat) :
  size la <= n.+1 ->
  reflect (forall i : 'I_n.+1, count_mem i (to_word t) = nth 0 la i)
          (eqeval t la).

Restricting and extending tableaux

Section BijectionExtTab.

Variable n : nat.

#[local] Open Scope nat_scope.

Variables (s : seq nat) (m : nat).
Hypothesis (Hsz : size s < n.+1).
#[local] Notation sz := (Ordinal Hsz).
#[local] Lemma Hszrcons : size (rcons s m) <= n.+1.

#[local] Notation P := ('P_(sumn s )).
#[local] Notation Pm := ('P_((sumn s) + m )).
Variable (mu : Pm).
#[local] Notation Tm := (tabsh mu).
Hypothesis Hmu : size mu <= n.+1.

Lemma shape_res_tab_subproof (t : Tm) :
  is_part_of_n (sumn s) (
                 if eqeval t (rcons s m) then shape (filter_gt_tab sz t)
                 else locked rowpartn (sumn s)).
Definition shape_res_tab (t : Tm) := IntPartN (shape_res_tab_subproof t).

Lemma hb_strip_shape_res_tab (t : Tm) :
  eqeval t (rcons s m) -> hb_strip (shape_res_tab t) mu.

Variable (la : P).
Hypothesis Hstrip : hb_strip la mu.
#[local] Notation T := (tabsh la).

#[local] Definition Hlamu := size_included (hb_strip_included Hstrip).
#[local] Definition Hla : size la <= n.+1 := leq_trans Hlamu Hmu.

Definition res_tab (t : Tm) : T :=
  if insub (filter_gt_tab sz t) is Some tr then tr
  else locked (tabrowconst Hla).
#[local] Definition ext_tab_fun (t : T) :=
  if eqeval t s then join_tab t (skew_reshape la mu (nseq m sz))
  else locked (tabrowconst Hmu).

#[local] Lemma sumndiff : sumn (mu / la) = m.

Lemma ext_tab_subproof t : is_tab_of_shape mu (ext_tab_fun t).
Definition ext_tab t := TabSh (ext_tab_subproof t).

Lemma res_tabP (t : Tm) :
  shape (filter_gt_tab sz t) == la ->
  is_tab_of_shape la (filter_gt_tab sz t).

Lemma eval_res_tab (t : Tm) :
  shape (filter_gt_tab sz t) == la ->
  eqeval t (rcons s m) -> eqeval (res_tab t) s.

Lemma eval_ext_tab (t : T) :
  eqeval t s -> eqeval (ext_tab t) (rcons s m).

Lemma res_tabK (t : Tm) :
  shape (filter_gt_tab sz t) == la ->
  eqeval t (rcons s m) -> ext_tab (res_tab t) = t.

Corollary res_tab_inj :
  {in [set x : Tm | eqeval x (rcons s m) & shape_res_tab x == la] &,
      injective res_tab }.

Lemma filter_ext_tab (t : T) :
  eqeval t s -> filter_gt_tab sz (ext_tab t) = t.

Lemma ext_tabK (t : T) : eqeval t s -> res_tab (ext_tab t) = t.

Corollary ext_tab_inj : {in [pred t : T | eqeval t s ] &, injective ext_tab }.

Lemma card_eq_eval :
  #|[set t : tabsh ['I_n.+1] mu |
     (eqeval t (rcons s m)) && (shape (filter_gt_tab sz t) == la )]|
  = #|[set t : tabsh ['I_n.+1] la | eqeval t s]|.

End BijectionExtTab.

Recursive computation of Kostka numbers

Section KostkaRec.

#[local] Open Scope nat_scope.

Lemma Kostka_ind d (la : 'P_d) m mu :
  d = m + sumn mu ->
  Kostka la (m :: mu) =
  \sum_(nu : 'P_(sumn mu ) | hb_strip nu la) Kostka nu mu.

Fixpoint Kostka_rec (la mu : seq nat) : nat :=
  if mu is m :: mu then
    sumn [seq Kostka_rec nu mu | nu <- enum_partn (sumn mu) & hb_strip nu la]
  else la == [::].

Example Kostka_expl1 :
  Kostka_rec [:: 4; 3] [:: 3; 2; 2] == 2.
Example Kostka_expl2 :
  Kostka_rec [:: 4; 3; 1] [:: 3; 2; 2; 1] == 5.
Example Kostka_expl3 :
  Kostka_rec [:: 4; 4; 3; 1] [:: 3; 3; 2; 2; 1; 1] == 25.

Lemma Kostka_rec_size0 la mu :
  size la > size mu -> Kostka_rec la mu = 0.

Lemma Kostka_recE d (la : 'P_d) mu :
  sumn mu = d -> Kostka_rec la mu = Kostka la mu.

End KostkaRec.

Notation "''K' ( la , mu )" := (Kostka la mu)
  (at level 8, format "''K' ( la , mu )") : nat_scope.
Notation "''K' ( la , mu )" := (Kostka la mu)%:R
  (at level 8, format "''K' ( la , mu )") : ring_scope.

Lemma Kostka_unitrig (R : comUnitRingType) d :
  unitrig (fun la mu : 'PDom_d => 'K (la , mu )%:R : R).

Inverse Kostka numbers

Definition KostkaInv d : 'P_d -> 'P_d -> int :=
  Minv (fun la mu : 'PDom_d => 'K (la , mu )%:R : int).

Lemma KostkaInv_unitrig d :
  unitrig (fun la mu : 'PDom_d => KostkaInv la mu).

Notation "''K^-1' ( la , mu )" := ((KostkaInv la mu)%:~R)
  (at level 8, format "''K^-1' ( la , mu )") : ring_scope.

Straightening of alternant polynomials

Section AlternStraighten.

Variable n0 : nat.
Variable R : comRingType.

#[local] Notation n := n0.+1.
#[local] Notation rho := (rho n).
#[local] Notation "''a_' k" := (@alternpol n R 'X_[k]).
#[local] Notation "m # s" := [multinom m (s i) | i < n].

Lemma alt_straight_step (m : 'X_{1..n}) (i : nat) :
  i < n0 -> m (inord i.+1) != 0%N ->
  'a_(m + rho ) = - 'a_(m # 's_i - U_(inord i) + U_(inord i.+1) + rho ).

Lemma alt_straight_add_ribbon0 (p : seq nat) (i : 'I_n) (d : nat) :
  is_part p -> size p <= n ->
  add_ribbon p d i == None -> 'a_(mpart p + rho + U_(i) *+ d.+1) = 0%R.

Lemma alt_straight_add_ribbon (p : seq nat) (i : 'I_n) (d : nat) :
  is_part p -> size p <= n ->
  forall res h, add_ribbon p d i = Some (res , h ) ->
    'a_(mpart p + rho + U_(i) *+ d.+1) = (-1) ^+ h.-1 *: 'a_(mpart res + rho ).

End AlternStraighten.