Library Combi.LRrule.therule: The Littlewood-Richardson rule

The Littlewood-Richardson rule

The goal of this file is to formalize the final step ot the proof: a bijection beetween LR-standard tableau as defined in LRsupport Q1 Q2 and LR-Yamanouchi tableaux.

Below we use the following notation:

d1 and d2 are nat,
P1 : a partition of d1 (of type: inpartn d1).
P2 : a partition of d2 (of type: inpartn d2).
P : a partition of d1 + d2 (of type: inpartn d1 + d2).

We define the following:

is_skew_reshape_tableau P P1 w == w is the row reading of a skew tableau of shape P/P1. Equivalently, the P/P1-reshape of w is a skew tableau.
bijLRyam P P1 == a map from seq nat to seq (seq nat) which defines a bijection between LR yamanouchi tableaux and LR-standard tableaux
bijLR P P1 == the sigma-type version of bijLRyam: (yam : yameval P2) -> stdtabn (d1 + d2)
LRyam_set P1 P2 P == the set of LR Yamanouchi words.
LRyam_coeff P1 P2 P == the LR coefficient defined as the cardinality of the set of LR Yamanouchi words.
LRyam_enum P1 P2 P == a list for the LR Yamanouchi words.
LRyam_compute P1 P2 P == the length LRyam_enum, allows to compute LR-coeffs and LR-tableaux from the definition inside coq. As an implementation, its a very slow way to compute LR-coeff. Indeed, the set of Yamanouchi words where we are looking for LR words is much too large. The module implem will provide a much efficient way using backtracking instead of filtering to enumerate those.
yamrow n == the trivial Yamanouchi word of size n whis is constant to 0

The main theorem is Theorem LRyam_coeffP:

Schur P1 * Schur P2 = \sum_(P : 'P_(d1 + d2) | included P1 P) Schur P *+ LRyam_coeff P.

As a corollary we provide the two Pieri rules Pieri_rowpartn and Pieri_colpartn.

From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg.
From mathcomp Require Import mpoly.

Require Import tools ordcast combclass partition skewpart Yamanouchi ordtype.
Require Import std tableau stdtab Schensted congr plactic Greene_inv.
Require Import stdplact Yam_plact skewtab shuffle Schur_mpoly freeSchur.

Set Implicit Arguments.

Import Order.TTheory.
Open Scope N.
#[local] Open Scope Combi.

Gluing a standard tableaux with a skew tableau

Section LR.

Lemma to_word_map_shiftn sh t :
  to_word (map (shiftn sh) t) = shiftn sh (to_word t).

Lemma filter_le_shiftn sh t :
  [seq x - sh | x <- [seq sh + i | i <- t] & sh <= x] = t.

Lemma filter_gt_shiftn sh t :
  [seq x <- [seq sh + i | i <- t] | gtn sh x] = [::].

Lemma shiftn_skew_dominate n sh u v :
  skew_dominate sh u v -> skew_dominate sh (shiftn n u) (shiftn n v).

Lemma is_skew_tableau_map_shiftn sh inn t :
  is_skew_tableau inn t -> is_skew_tableau inn (map (shiftn sh) t).

Lemma join_stdtab s t :
  is_stdtab s -> is_skew_tableau (shape s) t ->
  is_tableau (join_tab s (map (shiftn (size_tab s)) t)).

Lemma join_stdtab_in_shuffle s t :
  is_stdtab s ->
  size s <= size t ->
  to_word (join_tab s (map (shiftn (size_tab s)) t)) \in
       shsh (to_word s) (to_word t).

Variables d1 d2 : nat.

Section TheRule.

Variables (P1 : 'P_d1) (P2 : 'P_d2).

Lemma sfilterleq_LRsupportP Q :
  Q \in LRsupport (hyper_stdtabn P1) (hyper_stdtabn P2) ->
  exists y : yameval P2 , std y = (sfilterleq d1 (to_word Q)).

Lemma filter_gt_to_word (d : unit) (T : inhOrderType d) n (t : seq (seq T)) :
  filter (>%O n) (to_word t) = to_word (filter_gt_tab n t).

Lemma filter_le_to_word (d : unit) (T : inhOrderType d) n (t : seq (seq T)) :
  filter (<=%O n) (to_word t) = to_word (filter_le_tab n t).

Littlewood-Richardson Yamanouchi tableaux

Section OneCoeff.

Variable P : 'P_(d1 + d2 ).
Hypothesis Hincl : included P1 P.

Lemma sumn_diff_shape_intpartE : sumn (P / P1) = sumn P2.

Definition is_skew_reshape_tableau (P P1 : seq nat) (w : seq nat) :=
  is_skew_tableau P1 (skew_reshape P1 P w).
Definition LRyam_set :=
  [set y : yameval P2 | is_skew_reshape_tableau P P1 y].
Definition LRyam_coeff := #|LRyam_set|.

Lemma is_skew_reshape_tableauP (w : seq nat) :
  size w = sumn (P / P1) ->
  reflect
    (exists tab , [/\ is_skew_tableau P1 tab ,
                  shape tab = P / P1 & to_word tab = w ])
    (is_skew_reshape_tableau P P1 w).

Lemma size_leq_skew_reshape (y : seq nat) :
  size (RS (std (hyper_yam P1))) <= size (skew_reshape P1 P y).

The final bijection

Definition bijLRyam :=
  [fun y : seq nat =>
     join_tab (hyper_stdtabn P1) (map (shiftn d1) (skew_reshape P1 P (std y)))].

Lemma pred_LRtriple_fast_bijLRyam (yam : yameval P2) :
  is_skew_reshape_tableau P P1 yam ->
  pred_LRtriple_fast (hyper_stdtabn P1) (hyper_stdtabn P2) (bijLRyam yam).

Lemma bijLRyamP (yam : yameval P2) :
  is_skew_reshape_tableau P P1 yam -> is_stdtab_of_n (d1 + d2) (bijLRyam yam).

Definition bijLR (yam : yameval P2) : stdtabn (d1 + d2) :=
  if (boolP (is_skew_reshape_tableau P P1 yam)) is AltTrue pf then
    StdtabN (bijLRyamP pf)
  else
    hyper_stdtabn P.

Lemma bijLR_LRsupport yam :
  yam \in LRyam_set ->
  bijLR yam \in LRsupport (hyper_stdtabn P1) (hyper_stdtabn P2).

Lemma filtergtn_LRsupport Q :
  Q \in LRsupport (hyper_stdtabn P1) (hyper_stdtabn P2) ->
  filter_gt_tab d1 Q = hyper_stdtabn P1.

Lemma size_zip2 (T : Type) (s t : seq (seq T)) :
  [seq size p .1 + size p .2 | p <- zip s t] =
  [seq p .1 + p .2 | p <- zip (map size s) (map size t)].

Lemma shape_bijLR yam : yam \in LRyam_set -> shape (bijLR yam) = P.

Lemma filterleq_LRsupport Q :
  Q \in LRtab_set P1 P2 P ->
  (skew_reshape P1 P [seq x <- to_word Q | d1 <= x]) = filter_le_tab d1 Q.

Lemma sfilterleq_LRsupport_skew Q :
  Q \in LRtab_set P1 P2 P ->
        is_skew_reshape_tableau P P1 (sfilterleq d1 (to_word Q)).

Lemma bijLR_surj Q :
  Q \in LRtab_set P1 P2 P -> exists2 yam , yam \in LRyam_set & bijLR yam = Q.

Lemma bijLR_inj : {in LRyam_set &, injective bijLR }.

Lemma bijLR_image : LRtab_set P1 P2 P = [set bijLR x | x in LRyam_set].

Theorem LRyam_coeffE : LRtab_coeff P1 P2 P = LRyam_coeff.

A slow way to compute LR coefficients in coq:

We enumerate Yamanouchi words and filter those who are row reading of the skew tableaux of shape P/P1. This is very innefficient. A better way is to use backtracking as in implem.

Definition LRyam_enum (P1 P2 P : seq nat) :=
  [seq x <- enum_yameval P2 | is_skew_reshape_tableau P P1 x].
Definition LRyam_compute (P1 P2 P : seq nat) := size (LRyam_enum P1 P2 P).

Lemma LRcoeff_computeP : LRyam_compute P1 P2 P = LRyam_coeff.

End OneCoeff.

Lemma included_shape_filter_gt_tab
      (d : unit) (T : inhOrderType d) (n : T) t :
  is_tableau t -> included (shape (filter_gt_tab n t)) (shape t).

Lemma LRtab_set_included (P : 'P_(d1 + d2 )) Q :
  Q \in LRtab_set P1 P2 P -> included P1 P.

The statement of the Littlewood-Richardson rule

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

Variable (n0 : nat) (R : comRingType).
#[local] Notation n := (n0.+1).
Notation Schur p := (Schur n0 R p).

Theorem LRyam_coeffP :
Schur P1 * Schur P2 =
\sum_(P : 'P_(d1 + d2 ) | included P1 P) Schur P *+ LRyam_coeff P.

End TheRule.

Pieri's rules

Section Pieri.

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

Variable (n0 : nat) (R : comRingType).
#[local] Notation n := (n0.+1).
Notation Schur p := (Schur n0 R p).

Lemma yamrowP :
  is_yam_of_eval (intpart_of_intpartn (rowpartn d2)) (ncons d2 0%N [::]).
Definition yamrow : yameval (rowpartn d2) := YamEval yamrowP.

Lemma is_row_yamrow : is_row (ncons d2 0%N [::]).

Lemma yam_of_rowpart d y : is_yam_of_eval (rowpartn d) y -> y = ncons d 0%N [::].

Theorem LRyam_coeff_rowpart (P1 : 'P_d1) (P : 'P_(d1 + d2 )) :
included P1 P -> LRyam_coeff P1 (rowpartn d2) P = hb_strip P1 P.

Theorem Pieri_rowpartn (P1 : 'P_d1) :
  Schur P1 * Schur (rowpartn d2) =
  \sum_(P : 'P_(d1 + d2 ) | hb_strip P1 P) Schur P.

Theorem LRyam_coeff_colpartn (P1 : 'P_d1) (P : 'P_(d1 + d2 )) :
  included P1 P -> LRyam_coeff P1 (colpartn d2) P = vb_strip P1 P.

Theorem Pieri_colpartn (P1 : 'P_d1) :
  Schur P1 * Schur (colpartn d2) =
  \sum_(P : 'P_(d1 + d2 ) | vb_strip P1 P) Schur P.

End Pieri.

End LR.