Library Combi.MPoly.MurnaghanNakayama: Murnaghan-Nakayama rule

The Murnaghan-Nakayama rule

See the page Murnaghan-Nakayama on Wikipedia for a statement. The fixpoint MN_coeff la mu implement the recursive version, as stated in
Theorem MN_coeff_consE la m0 mu :
  MN_coeff la (m0 :: mu) =
  \sum_(sh : 'P_(sumn mu) | ribbon sh la)
   MN_coeff sh mu * (-1) ^+ (ribbon_height sh la).-1.

and the base case
Lemma MN_coeff0 : MN_coeff [::] [::] = 1.

The Murnaghan-Nakayama rule stated in terms of symmetric polynomials is then
Theorem MN_coeffP d (la : 'P_d) :
'p[la] = \sum_(sh : 'P_d) (MN_coeff sh la)%:~R *: 's[sh] :> {sympoly R[n]}.

There is a second implementation which goes bottom up, adding ribbons instead of removing them. It allows to compute skew Murnaghan-Nakayama coefficients.

We provide the following definitions:

MN_coeff la mu == then Murnaghan-Nakayama coefficients. That is the alternating number of ribbon filling of the shape la with content mu, defined recursively.
MN_coeff_fast la mu == fast version of MN_coeff la mu
MN_coeff_rec la nu mu == The alternating number of ribbon filling of the skew shape la / nu with content mu, defined recursively.

From HB Require Import structures.
From mathcomp Require Import all_boot.
From mathcomp Require Import ssralg ssrint perm fingroup tuple vector rat.
From mathcomp Require Import ssrcomplements mpoly.

Require Import sorted tools ordtype permuted partition skewpart.
Require Import antisym Schur_mpoly Schur_altdef sympoly homogsym.

Set Implicit Arguments.

#[local] Open Scope ring_scope.
Import GRing.Theory.

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

Product of an alternating polynomial and a power sum

Section MultAlternSymp.

Variable n0 : nat.
Variable R : comNzRingType.

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

Lemma mult_altern_symp_pol p d :
  'a_(mpart p + rho ) * (symp_pol n R d.+1) =
   \sum_(i < n) 'a_(mpart p + rho + U_(i) *+ d.+1).

Lemma mult_altern_oapp p d :
  is_part p -> size p <= n ->
  'a_(mpart p + rho ) * (symp_pol n R d.+1) =
  \sum_(i < n) oapp (fun ph => (-1) ^+ ph .2.-1 *: 'a_(mpart ph .1 + rho )) 0
   (add_ribbon p d i).

Lemma mult_altern_pmap p d :
  is_part p -> size p <= n ->
  'a_(mpart p + rho ) * (symp_pol n R d.+1) =
  \sum_(psh <- pmap (add_ribbon p d) (iota 0 n))
   (-1) ^+ (psh .2).-1 *: 'a_(mpart psh .1 + rho ).

End MultAlternSymp.

Product of a Schur polynomial and a power sum

Section MultSymsSympIDomain.

Variable n0 : nat.
#[local] Notation n := n0.+1.
#[local] Notation SF := {sympoly int[n ]}.

Lemma syms_sympM_oapp_int d (la : 'P_d) m :
  m != 0%N -> size la <= n ->
  's [la ] * 'p_m =
  \sum_(i < n) oapp (fun ph => (-1) ^+ ph .2.-1 *: 's [ph .1 ]) 0
   (add_ribbon_intpartn la m.-1 i) :> SF.

End MultSymsSympIDomain.

Section MultSymsSymp.

Variable n0 : nat.
Variable R : comNzRingType.
#[local] Notation n := n0.+1.
#[local] Notation SF := {sympoly R [n ]}.

Lemma syms_sympM_oapp d (la : 'P_d) m :
  m != 0%N ->
  's [la ] * 'p_m =
  \sum_(i < n) oapp (fun ph => (-1) ^+ ph .2.-1 *: 's [ph .1 ]) 0
   (add_ribbon_intpartn la m.-1 i) :> SF.

Lemma syms_sympM_pmap d (la : 'P_d) m :
  m != 0%N ->
  's [la ] * 'p_m =
  \sum_(ph <- pmap (add_ribbon_intpartn la m.-1) (iota 0 n))
   (-1) ^+ ph .2.-1 *: 's [ph .1 ] :> SF.

The following theorem is a step of the Murnaghan-Nakayama rule

Theorem syms_sympM d (la : 'P_d) m :
  m != 0%N ->
  's [la ] * 'p_m =
  \sum_(sh : 'P_(m + d ) | ribbon la sh)
   (-1) ^+ (ribbon_height la sh).-1 *: 's [sh ] :> SF.

End MultSymsSymp.

Murnaghan-Nakayama coefficients

We define those for any sequence of nat, but MN_coeff should only be used when sumn la == sumn mu.

Fixpoint MN_coeff (la mu : seq nat) : int :=
  if mu is m0 :: m then
    foldr (fun sh acc =>
             if ribbon sh la then
               MN_coeff sh m * (-1) ^+ (ribbon_height sh la).-1 + acc
             else acc)
          0 (enum_partn (sumn m))
  else 1.

Base case

Lemma MN_coeff0 : MN_coeff [::] [::] = 1.

Recursive step

Theorem MN_coeff_consE la m0 mu :
  MN_coeff la (m0 :: mu) =
  \sum_(sh : 'P_(sumn mu ) | ribbon sh la)
   MN_coeff sh mu * (-1) ^+ (ribbon_height sh la).-1.

Section Tests.

Tests :

sage: s(p[2,1,1])
-s[1, 1, 1, 1] - s[2, 1, 1] + s[3, 1] + s[4]

Goal ([seq x | x <- [seq (p , MN_coeff p [:: 2; 1; 1]) | p <- enum_partn 4]
               & x .2 != 0%R ] =
      [:: ([:: 4], Posz 1);
      ([:: 3; 1], Posz 1);
      ([:: 2; 1; 1], Negz 0);
      ([:: 1; 1; 1; 1], Negz 0)])%N.

Tests :

sage: s(p[4,2,1,1])
s[1, 1, 1, 1, 1, 1, 1, 1] + s[2, 1, 1, 1, 1, 1, 1] - s[3, 1, 1, 1, 1, 1]
 - 2*s[3, 3, 2] - s[4, 1, 1, 1, 1] + 2*s[4, 2, 1, 1] - s[5, 1, 1, 1]
 - s[6, 1, 1] + s[7, 1] + s[8]

Goal ([seq x | x <- [seq (p , MN_coeff p [:: 4; 2; 1; 1]) | p <- enum_partn 8]
               & x .2 != 0%R ] =
      [:: ([:: 8], Posz 1);
      ([:: 7; 1], Posz 1);
      ([:: 3; 3; 2], Negz 1);
      ([:: 6; 1; 1], Negz 0);
      ([:: 4; 2; 1; 1], Posz 2);
      ([:: 5; 1; 1; 1], Negz 0);
      ([:: 4; 1; 1; 1; 1], Negz 0);
      ([:: 3; 1; 1; 1; 1; 1], Negz 0);
      ([:: 2; 1; 1; 1; 1; 1; 1], Posz 1);
      ([:: 1; 1; 1; 1; 1; 1; 1; 1], Posz 1)])%N.

End Tests.

Murnaghan-Nakayama rule

Section MNRule.

Variable n0 : nat.
#[local] Notation n := n0.+1.

Theorem MN_coeffP_int d (la : 'P_d) :
  'p [la ] = \sum_(sh : 'P_d) MN_coeff sh la *: 's [sh ] :> {sympoly int[n ]}.

Variable R : comNzRingType.
#[local] Notation SF := {sympoly R [n ]}.
#[local] Notation HSF := {homsym R [n , _]}.

Theorem MN_coeffP d (la : 'P_d) :
  'p [la ] = \sum_(sh : 'P_d) (MN_coeff sh la)%:~R *: 's [sh ] :> SF.

Corollary MN_coeff_homogP d (la : 'P_d) :
  'hp [la ] = \sum_(sh : 'P_d) (MN_coeff sh la)%:~R *: 'hs [sh ] :> HSF.

End MNRule.

MN_coeff_rec should only be used when sumn la == sum nu + sumn mu.

Fixpoint MN_coeff_rec (la nu mu : seq nat) : int :=
  if mu is m0 :: m then
    foldr (fun psh acc =>
             MN_coeff_rec la psh .1 m * (-1) ^+ psh .2.-1 + acc)
          0
          [seq psh | psh <- pmap (add_ribbon nu m0.-1) (iota 0 (size la))
                   & included psh .1 la]
  else (la == nu).
Definition MN_coeff_fast la mu := MN_coeff_rec la [::] mu.

Lemma MN_coeff_rec_szE la nu m0 mu :
  MN_coeff_rec la nu (m0 :: mu) =
  \sum_(psh <- pmap (add_ribbon nu m0.-1) (iota 0 (size la))
       | included psh .1 la)
   MN_coeff_rec la psh .1 mu * (-1) ^+ psh .2.-1.

Lemma MN_coeff_rec_notincl la nu mu :
  0%N \notin mu -> is_part nu -> ~~ included nu la ->
  MN_coeff_rec la nu mu = 0.

Lemma MN_coeff_rec_consE n la nu m0 mu :
  m0 != 0%N -> size la <= n ->
  MN_coeff_rec la nu (m0 :: mu) =
  \sum_(psh <- pmap (add_ribbon nu m0.-1) (iota 0 n) | included psh .1 la)
   MN_coeff_rec la psh .1 mu * (-1) ^+ psh .2.-1.

Section Tests.

Tests :

sage: s(p[3, 3, 1, 1]).coefficient([5, 2, 1])
-2

Goal MN_coeff_fast [:: 5; 2; 1]%N [:: 3; 3; 1; 1]%N = - 2%:R.

Tests :

sage: s(p[5, 2, 1]).coefficient([3, 3, 1, 1])
1

Goal MN_coeff_fast [:: 3; 3; 1; 1]%N [:: 5; 2; 1]%N = 1%:R.

Tests :

sage: s(p[6, 5, 5, 4, 2, 1]).coefficient([12, 5, 2, 2, 1, 1])
4

Goal MN_coeff_fast [:: 12; 5; 2; 2; 1; 1]%N [:: 6; 5; 5; 4; 2; 1]%N = 4%:R.

Tests :

sage: s(p[6, 5, 5, 4, 2, 1]).coefficient([12, 5, 3, 1, 1, 1])
-2

Goal MN_coeff_fast [:: 12; 5; 3; 1; 1; 1]%N [:: 6; 5; 5; 4; 2; 1]%N = - 2%:R.
Goal MN_coeff_fast [:: 12; 5; 3; 2; 1]%N [:: 6; 5; 5; 4; 2; 1]%N = - 3%:R.
Goal MN_coeff_fast [:: 12; 5; 4; 1; 1]%N [:: 6; 5; 5; 4; 2; 1]%N = 2%:R.
Goal MN_coeff_fast [:: 12; 5; 4; 2]%N [:: 6; 5; 5; 4; 2; 1]%N = 4%:R.

Local Open Scope int_scope.

Let partn := rev (enum_partn 5).
Goal [seq [seq MN_coeff_fast la mu | mu <- partn ] | la <- partn ]
= [:: [:: 1; -1; 1; 1; -1; -1; 1];
       [:: 4; -2; 1; 0; 0; 1; -1];
       [:: 6; 0; 0; -2; 0; 0; 1];
       [:: 5; -1; -1; 1; 1; -1; 0];
       [:: 4; 2; 1; 0; 0; -1; -1];
       [:: 5; 1; -1; 1; -1; 1; 0];
       [:: 1; 1; 1; 1; 1; 1; 1]].

End Tests.

Section FastImplem.

Variable n0 : nat.
#[local] Notation n := n0.+1.

Lemma syms_prod_sympM_int dn (nu : 'P_dn) dm (mu : 'P_dm) :
  's [nu ] * 'p [mu ] =
  \sum_(la : 'P_(dn + dm )) MN_coeff_rec la nu mu *: 's [la ] :> {sympoly int[n ]}.

Section ComRing.

Variable R : comNzRingType.
#[local] Notation SF := {sympoly R [n ]}.
#[local] Notation HSF := {homsym R [n , _]}.

Theorem syms_prod_sympM dn (nu : 'P_dn) dm (mu : 'P_dm) :
  's [nu ] * 'p [mu ] =
  \sum_(la : 'P_(dn + dm )) (MN_coeff_rec la nu mu)%:~R *: 's [la ] :> SF.

Corollary homsyms_homsympM dn (nu : 'P_dn) dm (mu : 'P_dm) :
  'hs [nu ] *h 'hp [mu ] =
  \sum_(la : 'P_(dn + dm )) (MN_coeff_rec la nu mu)%:~R *: 'hs [la ] :> HSF.

Corollary MN_coeff_recP d (la : 'P_d) :
  'p [la ] = \sum_(sh : 'P_d) (MN_coeff_fast sh la)%:~R *: 's [sh ] :> SF.

Corollary MN_coeff_rec_homogP d (la : 'P_d) :
  'hp [la ] = \sum_(sh : 'P_d) (MN_coeff_fast sh la)%:~R *: 'hs [sh ] :> HSF.

End ComRing.

End FastImplem.

The two implementations coincide

Corollary MN_coeffE d (la mu : 'P_d) : MN_coeff_fast la mu = MN_coeff la mu.