Library Combi.LRrule.Yam_plact: Plactic classes and Yamanouchi words

Plactic classes and Yamanouchi words

The goal of this file is to show that the Yamanouchi words of a given evaluation form a plactic class.

yamtab sh == the uniq Yamanouchi tableau of shape sh: the i-th line contains only i's as in: 33 2222 11111 0000000.

The main result is Corollary yam_plactic_shape

y =Pl z <-> (is_yam z /\ evalseq y = evalseq z).

We also show that for all partition sh the standardization defines a bijection from Yamanouchi words of evaluation sh and a plactic class. In particular, it is surjective. This is Theorem plact_from_yam:

w =Pl std (hyper_yam sh) -> { y | is_yam_of_eval sh y & std y = w }.

Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq fintype.
From mathcomp Require Import tuple finfun finset path bigop order.

Require Import tools partition Yamanouchi ordtype std tableau stdtab.
Require Import Schensted congr plactic Greene_inv stdplact.

Set Implicit Arguments.

Import Order.TTheory.
Open Scope N.

Lemma is_part_incr_nthE sh i j :
  i.+1 < j -> is_part sh -> is_part (incr_nth (incr_nth sh j) i) ->
  is_part (incr_nth sh i) = is_part (incr_nth sh j).

Lemma is_part_incr_nth1E sh i :
  is_part sh ->
  is_part (incr_nth (incr_nth sh i.+1) i) = is_part (incr_nth sh i).

Lemma is_yam_plactic y : is_yam y -> forall w, y =Pl w -> is_yam w.

The Yamanouchi tableau

Fixpoint yamtab_rec i sh :=
  if sh is s0 :: s then
    nseq s0 i :: yamtab_rec (i.+1) s
  else [::].
Definition yamtab := yamtab_rec 0.

Lemma shape_yamtab sh : shape (yamtab sh) = sh.

Lemma to_word_yamtab sh : to_word (yamtab sh) = hyper_yam sh.

Lemma yamtabP sh : is_part sh -> is_tableau (yamtab sh).

Lemma yamtab_rcons sh sn :
  yamtab (rcons sh sn) = rcons (yamtab sh) (nseq sn (size sh)).

Lemma yamtab_unique t :
  is_tableau t -> is_yam (to_word t) -> t = yamtab (shape t).

Corollary RS_yam_RS y : is_yam y -> RS y = yamtab (shape (RS y)).

Lemma shape_RS_yam y : is_yam y -> shape (RS y) = evalseq y.

Lemma RS_yam y : is_yam y -> RS y = yamtab (evalseq y).

Theorem yam_plactic_hyper y : is_yam y -> y =Pl hyper_yam (evalseq y).

Corollary yam_plactic_shape y z :
  is_yam y -> ( y =Pl z <-> (is_yam z /\ evalseq y = evalseq z )).

Yamanouchi words, standardization and plactic classes

Lemma yam_std_inj : {in is_yam &, injective std }.

Lemma auxbijP p (y : yameval p) : is_yam_of_eval p ((RSmap y ).2).

#[local] Definition auxbij (p : intpart) (y : yameval p) : yameval p :=
  YamEval (auxbijP y).

Lemma auxbij_inj (p : intpart) : injective (@auxbij p).

#[local] Definition auxbij_inv (p : intpart) := invF (@auxbij_inj p).

Theorem plact_from_yam sh w :
  is_part sh ->
  w =Pl std (hyper_yam sh) ->
  { y | is_yam_of_eval sh y & std y = w }.