Young tableaux and RSK

Stream: maths

[Jake Levinson]

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]

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]

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

[Heather Macbeth]

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]

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]

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]

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

[Jake Levinson]

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

[Kyle Miller]

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]

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]

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]

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

[Jake Levinson]

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

[Jake Levinson]

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

[Yaël Dillies]

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]

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

[Kyle Miller]

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]

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]

@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]

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]

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

[Jake Levinson]

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

[Jake Levinson]

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]

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]

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]

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

[Jake Levinson]

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]

Most of the meat involves ssyt stuff

[Jake Levinson]

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]

@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]

I do not think so, no.

[Jake Levinson]

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

[Jake Levinson]

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]

Why not PR in parallel?

[Jake Levinson]

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

[Jake Levinson]

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

[Jake Levinson]

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]

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

[Jake Levinson]

@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?