Library Combi.LRrule.freeSchur: Free Schur functions
Free Schur functions
- commword n R w == the commutative image of the word w as a multivariate polynomial (of type {mpoly R[n]}).
- homlang n d == the type of homogenous langage over 'I_n.+1 of degre d. that is {set d.-tuple 'I_n}.
- polylang n R s == the commutative image of the langage s where s is of type homlang n d.
- catlang l1 l2 == the concatenation of homogeneous language: given s1 of degree d1 and s2 of degree d2 return an homogeneous language of degree d1 + d2.
- tabwordshape n sh == the set of reading of tableaux over 'I_n.+1 of shape sh, where sh is of type 'P_d
- freeSchur n t == the set of words whose recording tableau over 'I_n.+1 is t, where t is of type stdtabn
- tabword_of_tuple w == the bijection freeSchur -> tabwordshape as stated
in Theorem tabword_of_tuple_freeSchur:
forall Q : stdtabn d, [set tabword_of_tuple x | x in freeSchur n0 Q] = tabwordshape n0 (shape_deg Q)
- LRsupport Q1 Q2 == the set of standard Littlewood-Richardson Q-tableau in the product of the free Schur function indexed by Q1 and Q2, that is the set of Q which forms a LRtriple with Q1 and Q2.
- hyper_stdtab sh == the hyper standard tableau of shape sh as a seq (seq nat).
- hyper_stdtabn sh == the hyper standard tableau of shape sh as a stdtabn d where sh is a 'P_d.
- LRtab_set Q1 Q2 Q == the set of standard Littlewood-Richardson Q-tableau in the product of the free Schur function indexed by Q1 and Q2 of shape Q.
- LRtab_coeff Q1 Q2 == the Littlewood-Richardson coefficient defined as the cardinality of LRtab_set Q1 Q2 Q.
- bij_LRsupport Q1 Q2 == a bijection from LRsupport T1 T2 to LRsupport Q1 Q2
as long as T1 and Q1 have the same shape as well as
T2 and Q2. It is used to show Theorem
LRtab_coeff_shapeE:
shape T1 = P1 -> shape T2 = P2 -> LRtab_coeff P = #|[set Q in (LRsupport T1 T2) | (shape Q == P)]|.
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 Yamanouchi std tableau stdtab.
Require Import Schensted congr plactic stdplact Yam_plact Greene_inv shuffle.
Require Import Schur_mpoly.
Set Implicit Arguments.
Import Order.TTheory.
#[local] Open Scope ring_scope.
Import GRing.Theory.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg.
From mathcomp Require Import ssrcomplements freeg mpoly.
Require Import tools ordtype partition Yamanouchi std tableau stdtab.
Require Import Schensted congr plactic stdplact Yam_plact Greene_inv shuffle.
Require Import Schur_mpoly.
Set Implicit Arguments.
Import Order.TTheory.
#[local] Open Scope ring_scope.
Import GRing.Theory.
Section CommutativeImage.
Variable n : nat.
Variable R : comRingType.
Definition commword (w : seq 'I_n) : {mpoly R[n]} := \prod_(i <- w) 'X_i.
Lemma perm_commword (u v : seq 'I_n) :
perm_eq u v -> commword u = commword v.
Lemma commword_morph (u v : seq 'I_n) :
commword (u ++ v) = (commword u) * (commword v).
Lemma commtuple_morph d1 d2 (u : d1.-tuple 'I_n) (v : d2.-tuple 'I_n) :
commword (cat_tuple u v) = (commword u) * (commword v).
Definition homlang d := {set d.-tuple 'I_n}.
Definition polylang d (s : homlang d) := \sum_(w in s) commword w.
Definition catlang d1 d2 (s1 : homlang d1) (s2 : homlang d2) :
homlang (d1 + d2) :=
[set cat_tuple w1 w2 | w1 in s1, w2 in s2].
Lemma cat_tuple_inj d1 d2 (u x : d1.-tuple 'I_n) (v y : d2.-tuple 'I_n) :
cat_tuple u v = cat_tuple x y -> (u, v) = (x, y).
Lemma catlangM d1 d2 (s1 : homlang d1) (s2 : homlang d2) :
polylang s1 * polylang s2 = polylang (catlang s1 s2).
End CommutativeImage.
Variable n : nat.
Variable R : comRingType.
Definition commword (w : seq 'I_n) : {mpoly R[n]} := \prod_(i <- w) 'X_i.
Lemma perm_commword (u v : seq 'I_n) :
perm_eq u v -> commword u = commword v.
Lemma commword_morph (u v : seq 'I_n) :
commword (u ++ v) = (commword u) * (commword v).
Lemma commtuple_morph d1 d2 (u : d1.-tuple 'I_n) (v : d2.-tuple 'I_n) :
commword (cat_tuple u v) = (commword u) * (commword v).
Definition homlang d := {set d.-tuple 'I_n}.
Definition polylang d (s : homlang d) := \sum_(w in s) commword w.
Definition catlang d1 d2 (s1 : homlang d1) (s2 : homlang d2) :
homlang (d1 + d2) :=
[set cat_tuple w1 w2 | w1 in s1, w2 in s2].
Lemma cat_tuple_inj d1 d2 (u x : d1.-tuple 'I_n) (v y : d2.-tuple 'I_n) :
cat_tuple u v = cat_tuple x y -> (u, v) = (x, y).
Lemma catlangM d1 d2 (s1 : homlang d1) (s2 : homlang d2) :
polylang s1 * polylang s2 = polylang (catlang s1 s2).
End CommutativeImage.
Section TableauReading.
Context {disp : unit} {A : inhOrderType disp}.
Definition tabsh_reading_RS (sh : seq nat) (w : seq A) :=
(to_word (RS w) == w) && (shape (RS (w)) == sh).
Lemma tabsh_reading_RSP (sh : seq nat) (w : seq A) :
reflect
(exists tab, [/\ is_tableau tab, shape tab = sh & to_word tab = w])
(tabsh_reading_RS sh w).
Lemma tabsh_reading_RSE sh :
tabsh_reading sh =1 tabsh_reading_RS sh.
End TableauReading.
Context {disp : unit} {A : inhOrderType disp}.
Definition tabsh_reading_RS (sh : seq nat) (w : seq A) :=
(to_word (RS w) == w) && (shape (RS (w)) == sh).
Lemma tabsh_reading_RSP (sh : seq nat) (w : seq A) :
reflect
(exists tab, [/\ is_tableau tab, shape tab = sh & to_word tab = w])
(tabsh_reading_RS sh w).
Lemma tabsh_reading_RSE sh :
tabsh_reading sh =1 tabsh_reading_RS sh.
End TableauReading.
Section FreeSchur.
Variable R : comRingType.
Variable n0 : nat.
#[local] Notation n := (n0.+1).
#[local] Notation Schur sh := (Schur n0 R sh).
#[local] Notation homlang d := (homlang n d).
Section Degree.
Variable d : nat.
Definition tabwordshape (sh : 'P_d) : homlang d :=
[set t : d.-tuple 'I_n | tabsh_reading sh t ].
Definition freeSchur (Q : stdtabn d) : homlang d :=
[set t : d.-tuple 'I_n | (RStabmap t).2 == Q].
Lemma freeSchurP Q (t : d.-tuple 'I_n) :
t \in freeSchur Q = (val t \in langQ Q).
Lemma size_RS_tuple (t : d.-tuple 'I_n) : size (to_word (RS t)) == d.
Variable R : comRingType.
Variable n0 : nat.
#[local] Notation n := (n0.+1).
#[local] Notation Schur sh := (Schur n0 R sh).
#[local] Notation homlang d := (homlang n d).
Section Degree.
Variable d : nat.
Definition tabwordshape (sh : 'P_d) : homlang d :=
[set t : d.-tuple 'I_n | tabsh_reading sh t ].
Definition freeSchur (Q : stdtabn d) : homlang d :=
[set t : d.-tuple 'I_n | (RStabmap t).2 == Q].
Lemma freeSchurP Q (t : d.-tuple 'I_n) :
t \in freeSchur Q = (val t \in langQ Q).
Lemma size_RS_tuple (t : d.-tuple 'I_n) : size (to_word (RS t)) == d.
Bijection freeSchur -> tabwordshape
Definition tabword_of_tuple (t : d.-tuple 'I_n) : d.-tuple 'I_n :=
Tuple (size_RS_tuple t).
Lemma perm_tabword_of_tuple (t : d.-tuple 'I_n) :
perm_eq t (tabword_of_tuple t).
Lemma tabword_of_tuple_freeSchur_inj (Q : stdtabn d) :
{in (freeSchur Q) &, injective tabword_of_tuple}.
Lemma tabword_of_tuple_freeSchur (Q : stdtabn d) :
[set tabword_of_tuple x | x in freeSchur Q] = tabwordshape (shape_deg Q).
End Degree.
Tuple (size_RS_tuple t).
Lemma perm_tabword_of_tuple (t : d.-tuple 'I_n) :
perm_eq t (tabword_of_tuple t).
Lemma tabword_of_tuple_freeSchur_inj (Q : stdtabn d) :
{in (freeSchur Q) &, injective tabword_of_tuple}.
Lemma tabword_of_tuple_freeSchur (Q : stdtabn d) :
[set tabword_of_tuple x | x in freeSchur Q] = tabwordshape (shape_deg Q).
End Degree.
Section FreeLRrule.
Variables (d1 d2 : nat).
Variables (Q1 : stdtabn d1) (Q2 : stdtabn d2).
Definition LRsupport :=
[set Q : stdtabn (d1 + d2) | pred_LRtriple_fast Q1 Q2 Q ].
Lemma free_LR_rule :
catlang (freeSchur Q1) (freeSchur Q2) = \bigcup_(Q in LRsupport) freeSchur Q.
Variables (d1 d2 : nat).
Variables (Q1 : stdtabn d1) (Q2 : stdtabn d2).
Definition LRsupport :=
[set Q : stdtabn (d1 + d2) | pred_LRtriple_fast Q1 Q2 Q ].
Lemma free_LR_rule :
catlang (freeSchur Q1) (freeSchur Q2) = \bigcup_(Q in LRsupport) freeSchur Q.
Alternative proof from LRrule_langQ
Lemma free_LR_rule_alternate :
catlang (freeSchur Q1) (freeSchur Q2) = \bigcup_(Q in LRsupport) freeSchur Q.
catlang (freeSchur Q1) (freeSchur Q2) = \bigcup_(Q in LRsupport) freeSchur Q.
Passing to commutative image in the free LR rule
Theorem LR_rule_tab :
Schur (shape_deg Q1) * Schur (shape_deg Q2) =
\sum_(Q in LRsupport) (Schur (shape_deg Q)).
End FreeLRrule.
Definition hyper_stdtab sh := RS (std (hyper_yam sh)).
Lemma hyper_stdtabP sh : is_stdtab (hyper_stdtab sh).
Lemma hyper_stdtabnP d (P : 'P_d) : is_stdtab_of_n d (hyper_stdtab P).
Canonical hyper_stdtabn d (P : 'P_d) := StdtabN (hyper_stdtabnP P).
Lemma shape_hyper_stdtabnP d (P : 'P_d) : shape (hyper_stdtabn P) = P.
Lemma shaped_hyper_stdtabnP d (P : 'P_d) : shape_deg (hyper_stdtabn P) = P.
Section Coeffs.
Variables d1 d2 : nat.
Variables (P1 : 'P_d1) (P2 : 'P_d2).
Definition LRtab_set (P : 'P_(d1 + d2)) :=
[set Q in (LRsupport (hyper_stdtabn P1) (hyper_stdtabn P2)) | (shape Q == P)].
Definition LRtab_coeff (P : 'P_(d1 + d2)) := #|LRtab_set P|.
Theorem LRtab_coeffP :
Schur P1 * Schur P2 = \sum_P (Schur P) *+ LRtab_coeff P.
Lemma size_RSmapinv2_yam d
(disp : unit) (Typ : inhOrderType disp)
(tab : seq (seq Typ)) (T : stdtabn d) :
size (RSmapinv2 (tab, yam_of_stdtab T)) = d.
Schur (shape_deg Q1) * Schur (shape_deg Q2) =
\sum_(Q in LRsupport) (Schur (shape_deg Q)).
End FreeLRrule.
Definition hyper_stdtab sh := RS (std (hyper_yam sh)).
Lemma hyper_stdtabP sh : is_stdtab (hyper_stdtab sh).
Lemma hyper_stdtabnP d (P : 'P_d) : is_stdtab_of_n d (hyper_stdtab P).
Canonical hyper_stdtabn d (P : 'P_d) := StdtabN (hyper_stdtabnP P).
Lemma shape_hyper_stdtabnP d (P : 'P_d) : shape (hyper_stdtabn P) = P.
Lemma shaped_hyper_stdtabnP d (P : 'P_d) : shape_deg (hyper_stdtabn P) = P.
Section Coeffs.
Variables d1 d2 : nat.
Variables (P1 : 'P_d1) (P2 : 'P_d2).
Definition LRtab_set (P : 'P_(d1 + d2)) :=
[set Q in (LRsupport (hyper_stdtabn P1) (hyper_stdtabn P2)) | (shape Q == P)].
Definition LRtab_coeff (P : 'P_(d1 + d2)) := #|LRtab_set P|.
Theorem LRtab_coeffP :
Schur P1 * Schur P2 = \sum_P (Schur P) *+ LRtab_coeff P.
Lemma size_RSmapinv2_yam d
(disp : unit) (Typ : inhOrderType disp)
(tab : seq (seq Typ)) (T : stdtabn d) :
size (RSmapinv2 (tab, yam_of_stdtab T)) = d.
Section Bij_LRsupport.
Section ChangeUT.
Variable (U1 T1 : stdtabn d1) (U2 T2 : stdtabn d2).
Hypothesis Hsh1 : shape U1 = shape T1.
Hypothesis Hsh2 : shape U2 = shape T2.
Section TakeDrop.
Context {disp : unit} {T : inhOrderType disp}.
Lemma RStabE (w : seq T) : (RStab w).1 = (RS w).
Definition changeUT T1 T2 (w : seq T) : seq T :=
(RSmapinv2 (RS (take d1 w), yam_of_stdtab T1)) ++
(RSmapinv2 (RS (drop d1 w), yam_of_stdtab T2)).
Variable w : seq T.
Hypothesis Htake : shape (RS (take d1 w)) = shape U1.
Hypothesis Hdrop : shape (RS (drop d1 w)) = shape U2.
Lemma changeUtakeP : is_RStabpair (RS (take d1 w), val U1).
Lemma changeUdropP : is_RStabpair (RS (drop d1 w), val U2).
Lemma changeTtakeP : is_RStabpair (RS (take d1 w), val T1).
Lemma changeTdropP : is_RStabpair (RS (drop d1 w), val T2).
Lemma toDepRSPair (u : seq T) d (t : stdtabn d) :
forall H : is_RStabpair (RS u, val t),
RSmapinv2 (RS u, yam_of_stdtab t) = RStabinv (RSTabPair H).
Lemma plact_changeUT_take : take d1 (changeUT T1 T2 w) =Pl take d1 w.
Lemma plact_changeUT_drop : drop d1 (changeUT T1 T2 w) =Pl drop d1 w.
Lemma plact_changeUT : changeUT T1 T2 w =Pl w.
End TakeDrop.
Lemma changeUTK (disp : unit) (T : inhOrderType disp) (w : seq T) :
(take d1 w) \in langQ U1 ->
(drop d1 w) \in langQ U2 ->
changeUT U1 U2 (changeUT T1 T2 w) = w.
Section DefBij.
Variable Q : stdtabn (d1 + d2).
Hypothesis HTriple : pred_LRtriple U1 U2 Q.
Let w := RSmapinv2 (yamtab (shape Q), yam_of_stdtab Q).
Lemma RSpairyamQ : is_RSpair (yamtab (shape Q), yam_of_stdtab Q).
Lemma bij_LRsupportP :
is_stdtab_of_n (d1 + d2)
(RStab (changeUT T1 T2 (RSmapinv2 (yamtab (shape Q), yam_of_stdtab Q)))).2.
Definition bij_LRsupport := StdtabN bij_LRsupportP.
Lemma take_drop_langQ :
((take d1 w) \in langQ U1 /\ (drop d1 w) \in langQ U2).
Lemma shape_bij_LRsupport : shape bij_LRsupport = shape Q.
Lemma shape_takeRS : shape (RS (take d1 w)) = shape U1.
Lemma shape_dropRS : shape (RS (drop d1 w)) = shape U2.
Lemma predLR_bij_LRsupport : pred_LRtriple T1 T2 bij_LRsupport.
End DefBij.
Lemma card_LRtab_set_leq (P : seq nat) :
#|[set Q in (LRsupport U1 U2) | (shape Q == P)]| <=
#|[set Q in (LRsupport T1 T2) | (shape Q == P)]|.
End ChangeUT.
Lemma card_LRtab_set_shapeE P (U1 T1 : stdtabn d1) (U2 T2 : stdtabn d2) :
shape T1 = shape U1 -> shape T2 = shape U2 ->
#|[set Q in (LRsupport U1 U2) | (shape Q == P)]| =
#|[set Q in (LRsupport T1 T2) | (shape Q == P)]|.
Theorem LRtab_coeff_shapeE (T1 : stdtabn d1) (T2 : stdtabn d2) P :
shape T1 = P1 -> shape T2 = P2 ->
LRtab_coeff P = #|[set Q in (LRsupport T1 T2) | (shape Q == P)]|.
End Bij_LRsupport.
End Coeffs.
End FreeSchur.
Section ChangeUT.
Variable (U1 T1 : stdtabn d1) (U2 T2 : stdtabn d2).
Hypothesis Hsh1 : shape U1 = shape T1.
Hypothesis Hsh2 : shape U2 = shape T2.
Section TakeDrop.
Context {disp : unit} {T : inhOrderType disp}.
Lemma RStabE (w : seq T) : (RStab w).1 = (RS w).
Definition changeUT T1 T2 (w : seq T) : seq T :=
(RSmapinv2 (RS (take d1 w), yam_of_stdtab T1)) ++
(RSmapinv2 (RS (drop d1 w), yam_of_stdtab T2)).
Variable w : seq T.
Hypothesis Htake : shape (RS (take d1 w)) = shape U1.
Hypothesis Hdrop : shape (RS (drop d1 w)) = shape U2.
Lemma changeUtakeP : is_RStabpair (RS (take d1 w), val U1).
Lemma changeUdropP : is_RStabpair (RS (drop d1 w), val U2).
Lemma changeTtakeP : is_RStabpair (RS (take d1 w), val T1).
Lemma changeTdropP : is_RStabpair (RS (drop d1 w), val T2).
Lemma toDepRSPair (u : seq T) d (t : stdtabn d) :
forall H : is_RStabpair (RS u, val t),
RSmapinv2 (RS u, yam_of_stdtab t) = RStabinv (RSTabPair H).
Lemma plact_changeUT_take : take d1 (changeUT T1 T2 w) =Pl take d1 w.
Lemma plact_changeUT_drop : drop d1 (changeUT T1 T2 w) =Pl drop d1 w.
Lemma plact_changeUT : changeUT T1 T2 w =Pl w.
End TakeDrop.
Lemma changeUTK (disp : unit) (T : inhOrderType disp) (w : seq T) :
(take d1 w) \in langQ U1 ->
(drop d1 w) \in langQ U2 ->
changeUT U1 U2 (changeUT T1 T2 w) = w.
Section DefBij.
Variable Q : stdtabn (d1 + d2).
Hypothesis HTriple : pred_LRtriple U1 U2 Q.
Let w := RSmapinv2 (yamtab (shape Q), yam_of_stdtab Q).
Lemma RSpairyamQ : is_RSpair (yamtab (shape Q), yam_of_stdtab Q).
Lemma bij_LRsupportP :
is_stdtab_of_n (d1 + d2)
(RStab (changeUT T1 T2 (RSmapinv2 (yamtab (shape Q), yam_of_stdtab Q)))).2.
Definition bij_LRsupport := StdtabN bij_LRsupportP.
Lemma take_drop_langQ :
((take d1 w) \in langQ U1 /\ (drop d1 w) \in langQ U2).
Lemma shape_bij_LRsupport : shape bij_LRsupport = shape Q.
Lemma shape_takeRS : shape (RS (take d1 w)) = shape U1.
Lemma shape_dropRS : shape (RS (drop d1 w)) = shape U2.
Lemma predLR_bij_LRsupport : pred_LRtriple T1 T2 bij_LRsupport.
End DefBij.
Lemma card_LRtab_set_leq (P : seq nat) :
#|[set Q in (LRsupport U1 U2) | (shape Q == P)]| <=
#|[set Q in (LRsupport T1 T2) | (shape Q == P)]|.
End ChangeUT.
Lemma card_LRtab_set_shapeE P (U1 T1 : stdtabn d1) (U2 T2 : stdtabn d2) :
shape T1 = shape U1 -> shape T2 = shape U2 ->
#|[set Q in (LRsupport U1 U2) | (shape Q == P)]| =
#|[set Q in (LRsupport T1 T2) | (shape Q == P)]|.
Theorem LRtab_coeff_shapeE (T1 : stdtabn d1) (T2 : stdtabn d2) P :
shape T1 = P1 -> shape T2 = P2 ->
LRtab_coeff P = #|[set Q in (LRsupport T1 T2) | (shape Q == P)]|.
End Bij_LRsupport.
End Coeffs.
End FreeSchur.
Section Conj.
Variables d1 d2 : nat.
Lemma LRsupport_conj (T1 : stdtabn d1) (T2 : stdtabn d2):
LRsupport (conj_stdtabn T1) (conj_stdtabn T2) =
(@conj_stdtabn _) @: (LRsupport T1 T2).
Theorem LRtab_coeff_conj (P1 : 'P_d1) (P2 : 'P_d2) (P : 'P_(d1 + d2)) :
LRtab_coeff P1 P2 P =
LRtab_coeff (conj_intpartn P1) (conj_intpartn P2) (conj_intpartn P).
End Conj.
Variables d1 d2 : nat.
Lemma LRsupport_conj (T1 : stdtabn d1) (T2 : stdtabn d2):
LRsupport (conj_stdtabn T1) (conj_stdtabn T2) =
(@conj_stdtabn _) @: (LRsupport T1 T2).
Theorem LRtab_coeff_conj (P1 : 'P_d1) (P2 : 'P_d2) (P : 'P_(d1 + d2)) :
LRtab_coeff P1 P2 P =
LRtab_coeff (conj_intpartn P1) (conj_intpartn P2) (conj_intpartn P).
End Conj.