Zulip Chat Archive

Stream: maths

Topic: Young tableaux and RSK


Jake Levinson (Aug 02 2022 at 19:49):

Hi all,

I've been working on formalizing Young tableaux with the goal of formalizing the RSK correspondence. A special case of RSK is an equivalence between permutations of n : ℕ and ordered pairs of standard Young tableaux of the same shape (summing over all shapes of size n).

I have a fair amount of progress toward RSK and have written, I think, reasonably workable definitions of Young diagram, tableau, etc, with some API around them. Github code here: https://github.com/jakelev/lean-rsk.

I'd like to contribute some of it to mathlib, starting with e.g. the basic API around the definitions of young diagram and semistandard Young tableau (SSYT), which for me are:

import tactic
import data.set.basic

@[ext]
structure young_diagram :=
  (cells : finset ( × ))
  (nw_of' :  {i1 i2 j1 j2 : },
    i1  i2  j1  j2  (i2, j2)  cells  (i1, j1)  cells)

instance young_diagram.has_mem : has_mem ( × ) young_diagram :=
{ mem := λ c μ, c  μ.cells, }

@[ext]
structure ssyt (μ : young_diagram) :=
  (entry :     )
  (row_weak :  {i j1 j2 : }, j1 < j2  (i, j2)  μ 
    entry i j1  entry i j2)
  (col_strict :  {i1 i2 j: }, i1 < i2  (i2, j)  μ 
    entry i1 j < entry i2 j)
  (zeros' :  {i j}, (i, j)  μ  entry i j = 0)

For example, I have things like the transpose of a Young diagram, the row and column lengths (as weakly-decreasing sequences), adding or deleting a corner box to a Young diagram or tableau, and a fintype instance for SSYTs of fixed shape and bounded entries:

/- fintype instance for ssyts with bounded entries.
   method is to express as a subtype of (μ.cells → fin m) -/

def ssyt_bounded (μ : young_diagram) (m : ) :=
  {T : ssyt μ //  {i j}, (i, j)  μ  T i j < m}

instance ssyt_bounded.fintype {μ : young_diagram} {m : } :
  fintype (ssyt_bounded μ m) := sorry

RSK can come later, but if you're still reading at this point, basically I have:

  • One direction of RSK defined:
def rsk :
  Π (w : list (lex ( × ))), w.sorted () 
  Σ (μ : young_diagram), ssyt μ × ssyt μ := sorry
  • Part of inverse-RSK defined (there is a design choice here I am uncertain about, so basically so far I have only defined "one induction step of inverse RSK" but haven't defined the whole algorithm)
  • Proofs of inversion of the individual step of the insertion procedure; what's missing has to do with induction and well-founded recursion.

Jake Levinson (Aug 02 2022 at 19:51):

Questions:

  1. Should I just start making a PR with some basics?
  2. @Bhavik Mehta @Hanting Zhang @Kyle Miller I saw the three of you discussing Young tableaux a while back here. Did any of that end up getting PRed?

Yaël Dillies (Aug 02 2022 at 19:52):

You should probably use docs#is_lower_set in the definition of young_diagram.

Heather Macbeth (Aug 02 2022 at 19:53):

Cool!! My first thought (cc @Rob Lewis): Is there scope for a Sage extension calling
https://doc.sagemath.org/html/en/thematic_tutorials/algebraic_combinatorics/rsk.html

Jake Levinson (Aug 02 2022 at 19:57):

Yaël Dillies said:

You should probably use docs#is_lower_set in the definition of young_diagram.

Relatedly, would it be better to just define young_diagram as a subtype of finset (ℕ × ℕ) rather than as a structure?

Yaël Dillies (Aug 02 2022 at 20:01):

Doesn't really matter, I think. I doubt you will need much subtype API and, on the other hand, it won't hurt to define it as a subtype.

Yaël Dillies (Aug 02 2022 at 20:02):

What you should do either way is provide the set_like young_tableau (ℕ × ℕ) instance.

Jake Levinson (Aug 02 2022 at 20:18):

Will that clash with the finset setup? Since it coerces it to a set instead?

Kyle Miller (Aug 02 2022 at 20:21):

Regarding subtypes, a custom structure seems better since you're adding instances. Yael's suggestion to define a set_like instance to give you the has_mem (and some free other lemmas) seems like a good one -- I don't think it will clash with anything. (Make sure to follow the docs#set_like module docs for what boilerplate to define.)

Jake Levinson (Aug 02 2022 at 20:45):

Hmm. Is there any reason not just have the definition be def young_diagram := lower_set (ℕ × ℕ)? edit: oh right, because that isn't a finset.

Antoine Labelle (Aug 02 2022 at 20:47):

Jake Levinson said:

Hmm. Is there any reason not just have the definition be def young_diagram := lower_set (ℕ × ℕ)?

That would allow infinite sets.

Antoine Labelle (Aug 02 2022 at 20:49):

Maybe we should have more generally the lower finsets of any poset?

Jake Levinson (Aug 02 2022 at 20:54):

@Antoine Labelle Sure, though that seems outside the scope of young diagrams (which have properties particular to ℕ × ℕ).

Jake Levinson (Aug 02 2022 at 20:56):

Should cells be renamed to carrier? Seems like that is the convention elsewhere in mathlib.

Yaël Dillies (Aug 02 2022 at 20:57):

Antoine Labelle said:

Maybe we should have more generally the lower finsets of any poset?

That does sound like the correct generalisation, and would fit well with docs#lower_set

Jake Levinson (Aug 02 2022 at 21:02):

How big an initial commit / PR should I make? And, is it OK if I just use is_lower_set for now?

Kyle Miller (Aug 02 2022 at 21:16):

I'm not so sure about carrier here -- the "carrier" is referring to the underlying set of an algebraic structure, but a young diagram isn't an algebraic structure -- defining it as a finite downset of pairs is more of an implementation detail for these combinatorial objects. If you don't want cells, another relevant word is support, especially since a Young tableau is a kind of function with a Young diagram as its support.

Rob Lewis (Aug 02 2022 at 21:19):

Heather Macbeth said:

Cool!! My first thought (cc Rob Lewis): Is there scope for a Sage extension calling
https://doc.sagemath.org/html/en/thematic_tutorials/algebraic_combinatorics/rsk.html

This isn't a topic I know anything about, are there concrete instances of things that you'd want to calculate? What is Sage being called to do and how are you using it In Lean?

Jake Levinson (Aug 02 2022 at 21:24):

@Kyle Miller "Cells" (actually "boxes" :) ) is closest to how I would refer to them in real life. I'm happy to stick with cells then.

Kyle Miller (Aug 02 2022 at 21:27):

Re PR size -- it's best if you do things in small chunks (start with some definitions and some boilerplate?). You can include a link to your repository in the PR description below the "---" to help reviewers know where it's all going.

Jake Levinson (Aug 02 2022 at 21:58):

Okay, will do. Here's an initial PR: #15822

Jake Levinson (Aug 02 2022 at 21:59):

Even the basic boilerplate is a 100-line file with the documentation and everything :sweat_smile:

Jake Levinson (Aug 02 2022 at 22:00):

The linter asked for an inhabited instance for young_diagram, so I added in the definition of the empty Young diagram as well.

Yaël Dillies (Aug 02 2022 at 22:01):

Yeah so this is where lower_finset becomes interesting. You will soon want the order on Young tableaux and other order theoretic notions, so you better set it up in the full generality directly.

Jake Levinson (Aug 02 2022 at 22:23):

I don’t actually use that very much - I agree it’s relevant, but the stuff I plan to contribute doesn’t use stuff like (for example) intersection and union of Young diagrams.

Jake Levinson (Aug 02 2022 at 22:24):

I don’t even know if I use the has_subset instance more than a couple of times

Jake Levinson (Aug 02 2022 at 22:27):

For RSK at least, so far the only stuff I’ve needed is adding or deleting a box to a young diagram. I guess this is an order-theoretic notion (adding a covering element) actually.

Jake Levinson (Aug 02 2022 at 22:28):

Most of the meat involves ssyt stuff

Jake Levinson (Aug 03 2022 at 01:21):

Rob Lewis said:

Heather Macbeth said:

Cool!! My first thought (cc Rob Lewis): Is there scope for a Sage extension calling
https://doc.sagemath.org/html/en/thematic_tutorials/algebraic_combinatorics/rsk.html

This isn't a topic I know anything about, are there concrete instances of things that you'd want to calculate? What is Sage being called to do and how are you using it In Lean?

I'm not sure if I have a use case in mind here for Sage. If anything, maybe it should be the other way around -- if stuff is implemented in Lean with certificates of correctness, then maybe Sage will want access to Lean!

At the moment my implementation of RSK is computable in Lean, so for example I can do

#eval rsk [(1, 1), (1, 3), (1, 3), (2, 2), (2, 2), (3, 1), (3, 2)] sorry
/-
⟨[4, 2, 1]
□□□□
□□
□, (shape: [4, 2, 1]
1, 1, 1, 3
2, 2
3, shape: [4, 2, 1]
1, 1, 2, 2
2, 3
3)⟩
-/

(The sorry is the omitted proof that the input is a sorted list. The output is a shape, a recording tableau and a bumping tableau. It's this example from Wikipedia.)

Jake Levinson (Aug 03 2022 at 13:38):

@Yaël Dillies Regarding lower_finset, is there already a similar setup for other set_like objects like finite subgroups? Like, for any such object, there is always the analogous version whose carrier is a finset.

Yaël Dillies (Aug 03 2022 at 13:38):

I do not think so, no.

Jake Levinson (Aug 03 2022 at 13:40):

I wonder if there’s a way to automatically provide such a thing, like finset_like.

Jake Levinson (Aug 18 2022 at 05:28):

Hi all, #15822 has been added to mathlib. For the next steps, I have a couple of options:

  • Transposes, rows and columns (these are convenient to define together -- PR is just over 100 lines added)
  • Adding and deleting a corner box (this is another thing that would apply in the generality of a hypothetical lower_finset since it amounts to extending a lower set by a covering element, or deleting a maximal element)
  • Basic definition of SSYTs.

Any preferences on what to PR next?

Thomas Browning (Aug 18 2022 at 05:31):

Why not PR in parallel?

Jake Levinson (Aug 18 2022 at 05:33):

Hmm, that would be pretty doable actually, those three are all independent from each other.

Jake Levinson (Aug 18 2022 at 05:51):

Alright, #16120 on transposes, rows and columns is ready for review.

Jake Levinson (Aug 18 2022 at 05:53):

If anyone is interested in some code golf: the main thing I haven't done is to deduce facts about columns by transposing and applying the corresponding facts about rows. Instead all the column proofs are essentially copy/pasted from the rows section.

Jake Levinson (Aug 22 2022 at 06:13):

Alright, #16195 (semistandard Young tableaux) is ready.

Jake Levinson (Aug 24 2022 at 21:30):

@Kyle Miller wrote:

Maybe you could write enough lemmas to carry the theory of col to transpose.row then use simp? One feature you might use are simp sets, so then you can for example write simp with young_diagram_col_to_row to invoke these lemmas.

I have tried this, it seems to work OK, though in the end it doesn't exactly save work since the simp set takes longer to define than the number of lines it saves. Should I post it here or just push it to the PR?


Last updated: Dec 20 2023 at 11:08 UTC