Library Combi.LRrule.stdplact: Plactic congruences and standardization

Plactic congruences and standardization

The goal of this file is to show a few important properties of plactic congruence related to standardisation.

The first one is easy: it says that standardization preserve plactic congruence. This is Theorem std_plact and is stated as u =Pl v -> std u =Pl std v.

The next series of results relates the result of the RS map applied on u and std u:

the insertion tableau have the same shape: Theorem shape_RS_std;
the recording tableau are equal: Theorem RSmap_std and RStabmap_std.

And finally, inverting a standard word amount to exchange the insertion and the recording tableaux: Theorem invseqRSPQE, and Corollaries invseqRSE, invstdRSE, RSTabmapstdE and RSinvstdE.

From mathcomp Require Import all_ssreflect.
From mathcomp Require Import perm fingroup.

Require Import tools combclass ordcast partition Yamanouchi ordtype std tableau.
Require Import stdtab sorted Schensted congr plactic Greene Greene_inv.

Set Implicit Arguments.

Import Order.TTheory.

Plactic congruence and standardization

Section StdRS.

Context {disp : unit} {Alph : inhOrderType disp}.
Implicit Type s u v w : seq Alph.
Implicit Type p : seq nat.
Implicit Type t : seq (seq Alph).

Lemma std_plact1 (u v1 w v2 : seq Alph) :
v2 \in plact1 v1 -> std (u ++ v1 ++ w) =Pl std (u ++ v2 ++ w).

Lemma std_plact2 (u v1 w v2 : seq Alph) :
v2 \in plact2 v1 -> std (u ++ v1 ++ w) =Pl std (u ++ v2 ++ w).

Theorem std_plact u v : u =Pl v -> std u =Pl std v.

Robinson-Schensted correspondence and standardization

Lemma cast_enum u (S : {set 'I_(size u)}) :
  enum (mem (cast_set (esym (size_std u)) S)) =
  map (cast_ord (esym (size_std u))) (enum (mem S)).

Lemma sorted_std_extract u (S : {set 'I_(size u)}) :
  sorted <=%O (extractpred (in_tuple u) (mem S)) =
  sorted <=%O (extractpred (in_tuple (std u))
                           (mem (cast_set (esym (size_std u)) S))).

Lemma ksupp_inj_std u k : ksupp_inj <=%O <=%O k u (std u).

Lemma ksupp_inj_stdI u k : ksupp_inj <=%O <=%O k (std u) u.

Lemma Greene_std u k : Greene_row (std u) k = Greene_row u k.

Theorem shape_RS_std u : shape (RS (std u)) = shape (RS u).

End StdRS.

Theorem RSmap_std (d : unit) (T : inhOrderType d) (w : seq T) :
  (RSmap (std w)).2 = (RSmap w ).2.

Corollary RStabmap_std (d : unit) (T : inhOrderType d) (w : seq T) :
  (RStabmap (std w)).2 = (RStabmap w ).2.

Robinson-Schensted correspondence and inversion

Section KsuppInj.

Variable s t : seq nat.
Hypothesis Hinv : invseq s t.

#[local] Lemma Hinvst : linvseq s t.
#[local] Lemma Hinvts : linvseq t s.

#[local] Definition val2pos :=
  fun (i : 'I_(size s)) => Ordinal (linvseq_ltn_szt Hinvst (ltn_ord i)).

Lemma val2posE : val \o val2pos =1 nth (size t) s.
Lemma val2pos_inj : injective val2pos.

Lemma val2pos_enum (p : {set 'I_(size s)}) :

  sorted <=%O [seq tnth (in_tuple s) i | i <- enum (mem p)] ->
  enum (mem [set val2pos x | x in p]) = [seq val2pos x | x <- enum p].

Lemma ksupp_inj_invseq k : ksupp_inj <=%O <=%O k s t.

End KsuppInj.

Lemma Greene_invseq s t k : invseq s t -> Greene_row s k = Greene_row t k.

Lemma shape_invseq s t : invseq s t -> shape (RS s) = shape (RS t).

Lemma std_rcons_shiftinv t tn :
  is_std (rcons t tn) -> std t = map (shiftinv_pos tn) t.

Lemma posbig_invseq s0 s t tn :
  invseq (s0 :: s) (rcons t tn) -> posbig (s0 :: s) = tn.

Lemma nth_std_pos s i x :
  is_std s -> i < size s -> i != posbig s -> nth x s i < (size s).-1.

Lemma linvseqK s0 s t tn :
  invseq (s0 :: s) (rcons t tn) -> linvseq (rembig (s0 :: s)) (std t).

Lemma invseqK s0 s t tn :
  invseq (s0 :: s) (rcons t tn) -> invseq (rembig (s0 :: s)) (std t).

Theorem invseqRSPQE s t :
  invseq s t -> (RStabmap s ).1 = (RStabmap t ).2.

Corollary invseqRSE s t :
  invseq s t -> RStabmap s = ((RStabmap t ).2 , (RStabmap t ).1 ).

Corollary invstdRSE s :
  is_std s -> let (P, Q) := RStabmap (invstd s) in RStabmap s = (Q , P ).

Corollary RSTabmapstdE (disp : unit) (T : inhOrderType disp) (w : seq T) :
  (RStabmap (invstd (std w))).1 = (RStabmap (std w)).2.

Corollary RSinvstdE (disp : unit) (T : inhOrderType disp) (w : seq T) :
  RS (invstd (std w)) = (RStabmap w ).2.