Young tableau

Stream: new members

[Hanting Zhang]

I'm trying to define Young tableau in terms of partitions and finsets of ℕ × ℕ. First I turn a partition, which is implemented over a multiset, into a indexed function fin k → ℕ. The point being that I want to sort a partition {7, 2, 1, 5, 1, 6} into [1, 1, 2, 5, 6, 7]. To make a Young Tableau, the plan is to induce a finset of ℕ × ℕ which corresponds to the partition, along with a filling from that finset to ℕ. Here's my attempt to do it:

import tactic
import data.nat.choose.basic
import combinatorics.partition

open nat fin multiset
open_locale big_operators

namespace partition

variables {n : ℕ} (p : partition n)

def length : ℕ := multiset.card (p.parts)

-- for example, sort a partition `{7, 2, 1, 5, 1, 6}` into `[7, 6, 5, 2, 1, 1]`
def to_index : fin (p.length) → ℕ := λ i, list.index_of (i : ℕ) (sort has_le.le p.parts)

-- for example, given a partition [2, 1], output the subset {(0, 0), (0, 1), (1, 0)}
def to_grid {n : ℕ} (p : partition n) : finset (ℕ × ℕ) := by sorry

--  define a young_tableau with shape `p` as a filling of the subset of `ℕ × ℕ` induced by `p`
structure young_tableau {n : ℕ} (p : partition n) :=
(carrier : finset (ℕ × ℕ))
(proof_that_partition_induces_carrier : carrier = p.to_grid)
(filling : {x : (ℕ × ℕ) // x ∈ carrier} → ℕ)

-- a tableau is standard if `syt.filling` is a bijection
-- from `{x : (ℕ × ℕ) // x ∈ carrier} ` to `range n`
-- but how do I say that?
def is_standard (syt : young_tableau p) : Prop := by sorry

end partition

But I'm getting stuck on trying to define a standard tableau, because it's hard to reason while carrying {x : (ℕ × ℕ) // x ∈ carrier}everywhere. But I also don't want to drop it, since that would mean I have to say filling : ℕ × ℕ → ℕ along with something that restricts the function to only the carrier.
Or is there a better way to do all this?

[Kyle Miller]

@Hanting Zhang Oh, I see you've deleted your message in the meantime. In case you're still wondering about formulating Young tableaux, here's something that might work. The design is set up to make it so that transposing a tableau is easy. Then, you can get the partition from a tableau by taking the supremum index from each row and forming a multiset of these indices. At the very end, young_tableau_of p is the subtype of all Young tableau with a particular partition p.

The young_tableau type is designed so that equality of Young tableau corresponds to equality of young_tableau terms. The notion of a standard tableau is young_tableau.is_standard, and it just writes out the two axioms of injectivity and surjectivity.

This can all definitely be better organized and simplified! I'm also not sure how awkward it would be working with young_tableau_of p, which unfortunately uses eq.rec_on...

import tactic
import data.nat.choose.basic
import combinatorics.partition

open nat fin multiset
open_locale big_operators

namespace partition

@[ext]
structure young_tableau :=
(filling : ℕ × ℕ → ℕ)
(carrier : finset (ℕ × ℕ))
(is_carrier : ∀ s, filling s ≠ 0 ↔ s ∈ carrier)
(left_closed : ∀ i j, filling (i, j) ≠ 0 → ∀ j', j' ≤ j → filling (i, j') ≠ 0)
(up_closed : ∀ i j, filling (i, j) ≠ 0 → ∀ i', i' ≤ i → filling (i', j) ≠ 0)

namespace young_tableau

lemma left_closed' (t : young_tableau) :
  ∀ i j, (i, j) ∈ t.carrier → ∀ j', j' ≤ j → (i, j') ∈ t.carrier :=
by { have h := t.left_closed, simp only [t.is_carrier] at h, assumption }

lemma up_closed' (t : young_tableau) :
  ∀ i j, (i, j) ∈ t.carrier → ∀ i', i' ≤ i → (i', j) ∈ t.carrier :=
by { have h := t.up_closed, simp only [t.is_carrier] at h, assumption }

/-- The number of nonzero entries in the Young tableau. -/
def size (t : young_tableau) : ℕ := t.carrier.card

@[simps]
def transpose (t : young_tableau) : young_tableau :=
{ filling := λ s, t.filling s.swap,
  carrier := t.carrier.map (equiv.prod_comm ℕ ℕ).to_embedding,
  is_carrier := λ s, begin
    rw t.is_carrier,
    simp only [exists_prop, equiv.to_embedding_apply, finset.mem_map, prod.mk.inj_iff,
               equiv.prod_comm_apply, prod.swap_prod_mk, prod.exists],
    split,
    { intro h, refine ⟨s.2, s.1, h, prod.mk.eta⟩, },
    { rintro ⟨j, i, h, rfl, rfl⟩, exact h, },
  end,
  up_closed := λ j i, t.left_closed i j,
  left_closed := λ j i, t.up_closed i j }

/-- `t.filling` is a bijection from `t.carrier` to the interval `[1, t.size]`. -/
structure is_standard (t : young_tableau) : Prop :=
(filling_inj : ∀ (s s' : ℕ × ℕ), s ∈ t.carrier → s' ∈ t.carrier → t.filling s = t.filling s' → s = s')
(filling_surj : ∀ (s : ℕ × ℕ), s ∈ t.carrier → t.filling s ≤ t.size)

/-- Get the smallest `j'` such that `(i,j) ∈ t.carrier` implies `j < j'` -/
def width_at (t : young_tableau) (i : ℕ) : ℕ :=
(t.carrier.filter (λ (s : ℕ × ℕ), s.1 = i)).sup (λ s, s.2 + 1)

/-- Get the smallest `i'` such that `(i,0) ∈ t.carrier` implies `i < i'`  -/
def height (t : young_tableau) : ℕ :=
(t.carrier.filter (λ (s : ℕ × ℕ), s.2 = 0)).sup (λ s, s.1 + 1)

def widths (t : young_tableau) : multiset ℕ :=
(range t.height).map (λ i, t.width_at i)

def mem_sup {α : Type*} [decidable_eq α] (s : finset α) (hne : s.nonempty) (f : α → ℕ) :
  ∃ (a : α), a ∈ s ∧ s.sup f = f a :=
begin
  refine finset.induction_on s _ (λ a s' hs' ih hine', _) hne,
  simp,
  by_cases hne' : s'.nonempty,
  swap,
  { simp at hne',
    subst s',
    use a, simp, },
  { rcases ih hne' with ⟨b, hb, hfb⟩,
    by_cases hm : f a ≤ f b,
    { use b, simp [hb, hfb, hm], },
    { rw not_le at hm,
      use a,
      simp only [finset.sup_insert, hfb],
      simp [le_of_lt hm], }, },
end

lemma carrier_eq_bind (t : young_tableau) :
  t.carrier = (finset.range t.height).bind (λ i, (finset.range (t.width_at i)).image (λ j, (i, j))) :=
begin
  ext x,
  cases x with i j,
  simp only [height, width_at, exists_prop, finset.mem_bind, finset.mem_image, finset.mem_range,
             prod.mk.inj_iff],
  by_cases hne : t.carrier.nonempty,
  swap,
  { rw [finset.not_nonempty_iff_eq_empty] at hne,
    rw hne,
    simp, },
  split,
  { intro hij,
    use i,
    simp only [true_and, eq_self_iff_true, exists_eq_right],
    split,
    { by_contra h,
      push_neg at h,
      rw finset.sup_le_iff at h,
      specialize h (i, 0),
      have hi0 : (i, 0) ∈ t.carrier := t.left_closed' _ _ hij _ (nat.zero_le _),
      simp only [hi0, forall_prop_of_true, add_le_iff_nonpos_right, eq_self_iff_true,
                 one_ne_zero, and_self, finset.mem_filter, nonpos_iff_eq_zero] at h,
      assumption, },
    { by_contra h,
      push_neg at h,
      rw finset.sup_le_iff at h,
      specialize h (i, j),
      simp only [hij, forall_prop_of_true, add_le_iff_nonpos_right, eq_self_iff_true,
                 one_ne_zero, and_self, finset.mem_filter, nonpos_iff_eq_zero] at h,
      assumption, }, },
  { rintro ⟨i, hi, j, hj, rfl, rfl⟩,
    have hh := mem_sup (t.carrier.filter (λ s, s.snd = 0)) _ (λ (s : ℕ × ℕ), s.fst + 1),
    swap,
    { rcases hne with ⟨⟨i, j⟩, hs⟩,
      use (0, 0), simp,
      apply t.up_closed' i 0 _ _ (nat.zero_le _),
      apply t.left_closed' i j hs _ (nat.zero_le _), },
    rcases hh with ⟨⟨i', j'⟩, hh, hh'⟩,
    simp only [finset.mem_filter] at hh,
    cases hh with hh hj',
    subst j',
    simp only [hh'] at hi,
    have hh'' := mem_sup (t.carrier.filter (λ (s : ℕ × ℕ), s.fst = i)) _ (λ (s : ℕ × ℕ), s.snd + 1),
    swap,
    { use (i, 0),
      simp,
      rw lt_succ_iff at hi,
      apply t.up_closed' _ _ hh _ hi, },
    rcases hh'' with ⟨⟨i'', j''⟩, hh'', hh'''⟩,
    simp only [finset.mem_filter] at hh'',
    cases hh'' with hh'' hi'',
    subst i'',
    simp only [hh'''] at hj,
    rw lt_succ_iff at hj,
    apply t.left_closed' i j'' hh'' _ hj, },
end

lemma size_eq (t : young_tableau) : t.size = ∑ i in finset.range t.height, t.width_at i :=
begin
  convert_to (∑ s in t.carrier, 1) = _,
  { simp, refl, },
  rw carrier_eq_bind,
  rw [finset.sum_bind],
  congr,
  ext i,
  rw [finset.sum_image],
  simp,
  simp,
  simp,
  intros i hi j hj hij,
  rw finset.disjoint_iff_ne,
  rintros ⟨ai, aj⟩ ha ⟨bi, bj⟩ hb,
  simp at ha hb,
  rcases ha with ⟨a, ha, rfl, rfl⟩,
  rcases hb with ⟨b, hb, rfl, rfl⟩,
  intro h,
  simp at h,
  exact hij h.1,
end

lemma sum_widths_eq_size (t : young_tableau) : t.widths.sum = t.size :=
begin
  convert_to (finset.range t.height).sum t.width_at = _,
  rw size_eq,
end

def partition (t : young_tableau) : partition t.size :=
{ parts := t.widths,
  parts_pos := begin
    intros j h,
    simp only [widths, width_at, height, mem_range, mem_map] at h,
    by_cases hne : t.carrier.nonempty,
    swap,
    { rw [finset.not_nonempty_iff_eq_empty] at hne,
      simp [hne] at h,
      exfalso,
      rcases h.1 with ⟨x, hx⟩,
      exact not_lt_zero _ hx, },
    rcases hne with ⟨⟨xi, xj⟩, hx⟩,
    rcases h with ⟨i', hi', rfl⟩,
    have h1 := mem_sup (t.carrier.filter (λ (s : ℕ × ℕ), s.snd = 0)) _ (λ (s : ℕ × ℕ), s.fst + 1),
    swap,
    { use (0, 0), simp,
      apply t.up_closed' xi 0 _ _ (nat.zero_le _),
      apply t.left_closed' _ _ hx _ (nat.zero_le _), },
    rcases h1 with ⟨⟨ai, aj⟩, ha, h1⟩,
    simp at ha,
    rcases ha with ⟨ha, haj⟩,
    subst aj,
    simp [h1] at hi',
    have h2 := mem_sup (t.carrier.filter (λ (s : ℕ × ℕ), s.fst = i')) _ (λ (s : ℕ × ℕ), s.snd + 1),
    swap,
    { use (i', 0),
      simp,
      rw lt_succ_iff at hi',
      apply t.up_closed' _ _ ha _ hi', },
    rcases h2 with ⟨⟨bi, bj⟩, hb, h2⟩,
    simp [h2],
  end,
  parts_sum := t.sum_widths_eq_size }

end young_tableau

/-- Whether or not a tableau has a particular partition.  Needs `eq.rec_on` to rewrite
the `n` in the partition to `t.size` when they are equal. -/
def young_tableau.has_partition (t : young_tableau) {n : ℕ} (p : partition n) : Prop :=
∃ (h : n = t.size), t.partition = eq.rec_on h p

/-- All the young tableau with a partition of a particular type. -/
def young_tableau_of {n : ℕ} (p : partition n) := {t : young_tableau // t.has_partition p}

end partition

[Kyle Miller]

In retrospect, it would probably be better to have defined

@[ext]
structure young_tableau (n : ℕ) :=
(filling : ℕ × ℕ → ℕ)
(carrier : finset (ℕ × ℕ))
(size_eq : carrier.card = n)
(is_carrier : ∀ s, filling s ≠ 0 ↔ s ∈ carrier)
(left_closed : ∀ i j, filling (i, j) ≠ 0 → ∀ j', j' ≤ j → filling (i, j') ≠ 0)
(up_closed : ∀ i j, filling (i, j) ≠ 0 → ∀ i', i' ≤ i → filling (i', j) ≠ 0)

for the Young tableaux with n filled squares. This avoids the eq.rec_on.

[Eric Wieser]

Fields 1,2, and 4 are collectively just a finsupp (\N \times \N) \N

[Kyle Miller]

With the above, I made it so that a square is filled iff it wasn't 0, so then a standard tableau has 1,2,...,n, but it's probably better if it's 0,1,...,n-1. (Unfortunately that means it wouldn't just be finsupp.)

Also, it's probably better to split off Young diagrams from Young tableaux. The diagram is the finset of squares, and the tableau is a filling. The following is an experiment with this (mostly things regarding transpositions), and it has the beginnings of constructing a Young diagram from a partition (young_diagram.of_row_partition).

import tactic
import data.nat.choose.basic
import combinatorics.partition

open_locale big_operators

namespace partition

@[ext]
structure young_diagram (n : ℕ) :=
(squares : finset (ℕ × ℕ))
(left_closed : ∀ i j, (i, j) ∈ squares → ∀ j', j' ≤ j → (i, j') ∈ squares)
(up_closed : ∀ i j, (i, j) ∈ squares → ∀ i', i' ≤ i → (i', j) ∈ squares)

namespace young_diagram

@[simp]
lemma mem_image_swap {i j : ℕ} (s : finset (ℕ × ℕ)) : (i, j) ∈ s.image prod.swap ↔ (j, i) ∈ s :=
begin
  simp only [exists_prop, prod.mk.inj_iff, finset.mem_image, prod.swap_prod_mk, prod.exists],
  split,
  { rintro ⟨j, i, h, rfl, rfl⟩, exact h, },
  { intro h, exact ⟨j, i, h, rfl, rfl⟩ },
end

@[simps]
def transpose {n : ℕ} (d : young_diagram n) : young_diagram n :=
{ squares := d.squares.image prod.swap,
  left_closed := λ i j, by { simp only [mem_image_swap], exact d.up_closed j i },
  up_closed := λ i j, by { simp only [mem_image_swap], exact d.left_closed j i } }

variables {n : ℕ} (d : young_diagram n)

lemma transpose_transpose : d.transpose.transpose = d :=
begin
  ext1,
  simp only [transpose_squares],
  rw finset.image_image,
  simp,
end

/-- The number of rows in the diagram. -/
def rows : ℕ := d.squares.sup (λ s, s.1 + 1)
/-- The number of columns in the diagram. -/
def cols : ℕ := d.squares.sup (λ s, s.2 + 1)
/-- The number of squares in row i -/
def row_squares (i : ℕ) : ℕ := (d.squares.filter (λ (s : ℕ × ℕ), s.1 = i)).sup (λ s, s.2 + 1)
/-- The number of squares in column j -/
def col_squares (j : ℕ) : ℕ := (d.squares.filter (λ (s : ℕ × ℕ), s.2 = j)).sup (λ s, s.1 + 1)

lemma rows_eq_first_col_squares : d.rows = d.col_squares 0 :=
begin
  simp [rows, col_squares],
  refine le_antisymm _ (finset.sup_subset (finset.filter_subset _ _) _),
  rw finset.sup_le_iff,
  rintros ⟨i, j⟩ hij,
  have hi0 := d.left_closed _ _ hij 0 (nat.zero_le _),
  have h : (i, 0) ∈ d.squares.filter (λ (s : ℕ × ℕ), s.snd = 0),
  { simp [hi0], },
  change (λ (s : ℕ × ℕ), s.fst + 1) (i, 0) ≤ _,
  apply finset.le_sup h,
end

lemma sup_image_swap_eq (t : finset (ℕ × ℕ)) : (t.image prod.swap).sup (λ s, s.snd + 1) = t.sup (λ s, s.fst + 1) :=
begin
  unfold finset.sup,
  rw finset.fold_image, refl,
  rintros ⟨i, j⟩ _ ⟨i', j'⟩ _,
  simp only [and_imp, prod.mk.inj_iff, prod.swap_prod_mk],
  rintros rfl rfl,
  exact ⟨rfl, rfl⟩,
end

@[simp]
lemma row_squares_of_transpose (i : ℕ) : d.transpose.row_squares i = d.col_squares i :=
begin
  simp only [row_squares, col_squares, transpose_squares],
  have h : (d.squares.image prod.swap).filter (λ (s : ℕ × ℕ), s.fst = i) =
    (d.squares.filter (λ (s : ℕ × ℕ), s.snd = i)).image prod.swap,
  { rw finset.image_filter, refl, },
  rw h, clear h,
  rw sup_image_swap_eq,
end

@[simp]
lemma col_squares_of_transpose (i : ℕ) : d.transpose.col_squares i = d.row_squares i :=
by rw [←transpose_transpose d, row_squares_of_transpose, transpose_transpose]

@[simp]
lemma cols_of_transpose : d.transpose.cols = d.rows :=
by { dsimp [cols, rows], rw sup_image_swap_eq }

@[simp]
lemma rows_of_transpose : d.transpose.rows = d.cols :=
by rw [←transpose_transpose d, cols_of_transpose, transpose_transpose]

@[simp]
lemma cols_eq_first_row_squares : d.cols = d.row_squares 0 :=
by rw [←transpose_transpose d, cols_of_transpose, row_squares_of_transpose, rows_eq_first_col_squares]

lemma row_squares_pos (i : ℕ) (h : i < d.rows) : 0 < d.row_squares i :=
begin
  sorry
end

/-- The partition associated to the rows -/
def row_partition : partition n :=
{ parts := (multiset.range d.rows).map d.row_squares,
  parts_pos := begin
    simp only [and_imp, multiset.mem_range, forall_apply_eq_imp_iff₂, multiset.mem_map, exists_imp_distrib],
    exact d.row_squares_pos,
  end,
  parts_sum := begin
    sorry
  end }

def partition_fn (p : partition n) (i : ℕ) : ℕ :=
let s := p.parts.sort (≥)
in option.get_or_else (s.nth i) 0

/-- inverse of `row_partition` -/
def of_row_partition (p : partition n) : young_diagram n :=
{ squares := (finset.range p.parts.card).bind (λ i, (finset.range (partition_fn p i)).image (λ j, (i, j))),
  left_closed := sorry,
  up_closed := sorry }

end young_diagram

@[ext]
structure young_tableau {n : ℕ} (d : young_diagram n) :=
(filling : ℕ × ℕ → ℕ)
(in_diagram : ∀ s, filling s ≠ 0 → s ∈ d.squares)

namespace young_tableau
variables {n : ℕ} (d : young_diagram n)

@[simps]
def transpose (t : young_tableau d) : young_tableau d.transpose :=
{ filling := λ s, t.filling s.swap,
  in_diagram := λ s h, begin
    have h' := t.in_diagram s.swap h,
    revert h',
    cases s with i j,
    simp,
  end }

/-- `t.filling` is a bijection from `d.squares` to `0,1,...,n-1`. -/
structure is_standard (t : young_tableau d) : Prop :=
(filling_inj : ∀ (s s' : ℕ × ℕ), s ∈ d.squares → s' ∈ d.squares → t.filling s = t.filling s' → s = s')
(filling_surj : ∀ (s : ℕ × ℕ), s ∈ d.squares → t.filling s < n)

end young_tableau

end partition

[Hanting Zhang]

I deleted because I doubled back and started working with a vector-only definition (where I just have a vector of length n and build a lot of API to access the data easily.) Actually, we probably want tableau entries to be positive, since doing tableau calculations like the hook length formula would rely on that. I don't know if starting with diagrams without partitions will work out to be smoother. But looking at what you've done @Kyle Miller , maybe the problem is that we don't have a good API for "finsets of N x N." I can't think of any examples off the top of my head except for young tableau, but "finsets of N x N" with certain graph-theoretic properties should be useful.

[Hanting Zhang]

I'll try some stuff with what you've started. There still needs to be a weakly decreasing condition on the entries. Proving the hook length would be a good test.

[Bhavik Mehta]

When I made partitions a while ago I had a go at this too, my definition was essentially the same as yours (though I included the size in the structure like you realised), but I found it awkward to prove that transposition keeps the number of squares the same, ie that transposition is a well defined function young_diagram n -> young_diagram n. If you can get this working I think it would make a good PR to mathlib