The Bender-Knuth involutions

Fix a semistandard Young tableau T and a letter v. The Bender-Knuth involution at v rewrites the vs and (v + 1)s of T so as to exchange how often the two letters occur, leaving every other letter untouched. It is the combinatorial mechanism behind the symmetry of the Schur polynomials, and this file builds it.

The construction here is not the usual row-by-row description ("the vs and (v + 1)s that are not vertically paired form, in each row, a block of a copies of v followed by b copies of v + 1; replace it by b copies of v and a copies of v + 1"). It is organized instead around a single counting function, SemistandardYoungTableau.rowCountLt T i x, the number of entries smaller than x in row i. Rows increase weakly, so the entries of row i smaller than x occupy exactly the columns below rowCountLt T i x, and this one function records the whole row. Writing a i = rowCountLt T i v, n i = rowCountLt T i (v + 1) and b i = rowCountLt T i (v + 2), the letters v and v + 1 of row i occupy the columns of Finset.Ico (a i) (b i), split at n i.

A filling with the same entries outside those blocks is then the same thing as a choice of a new splitting point cut i in each row, and SemistandardYoungTableau.recut builds it. Two inequalities per row beyond a i ≤ cut i ≤ b i are enough to make the result semistandard again — this is SemistandardYoungTableau.IsCut, a sufficient condition — and together they place cut i in the interval [max (a i) (b (i + 1)), min (b i) (a (i - 1))], which contains n i. The Bender-Knuth involution recuts each row at the reflection of n i in that interval, and being a reflection is what makes it an involution: the interval is unchanged by a recut, because its endpoints depend only on a and b, which a recut does not move.

Main definitions

• SemistandardYoungTableau.rowCountLt: the number of entries smaller than a given letter in a given row.
• SemistandardYoungTableau.IsCut: the condition on a family of splitting points that makes the recut filling semistandard.
• SemistandardYoungTableau.recut: the tableau obtained by splitting the v/(v + 1) block of each row at a prescribed column.
• SemistandardYoungTableau.benderKnuth: the Bender-Knuth involution at a letter v.

Main results

• SemistandardYoungTableau.benderKnuth_benderKnuth: the Bender-Knuth involution is an involution.
• SemistandardYoungTableau.content_benderKnuth: it exchanges the multiplicities of v and v + 1 and fixes every other one.

References

• E. A. Bender and D. E. Knuth, Enumeration of plane partitions, J. Combinatorial Theory 13 (1972), 40--54, where the involution originates.
• W. Fulton, Young Tableaux, Section 2.2.
• Schur--Weyl roadmap, Layer 7.

Counting the entries of a row

def SemistandardYoungTableau.rowCountLt {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (i x : ℕ) : ℕ

The number of entries smaller than x in row i of a tableau. As rows increase weakly, these entries occupy exactly the columns below this number — the content of SemistandardYoungTableau.lt_rowCountLt_iff — so a single such counting function records the whole row.

Equations

• T.rowCountLt i x = {j ∈ Finset.range (μ.rowLen i) | T i j < x}.card

theorem SemistandardYoungTableau.filter_lt_eq_range {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (i x : ℕ) : {j ∈ Finset.range (μ.rowLen i) | T i j < x} = Finset.range (T.rowCountLt i x)

The entries of a row smaller than x occupy an initial segment of columns, of length SemistandardYoungTableau.rowCountLt.

theorem SemistandardYoungTableau.lt_rowCountLt_iff {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i j x : ℕ} (hj : j < μ.rowLen i) : j < T.rowCountLt i x ↔ T i j < x

The columns of a row carrying an entry smaller than x are exactly those below SemistandardYoungTableau.rowCountLt.

theorem SemistandardYoungTableau.rowCountLt_le_rowLen {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (i x : ℕ) : T.rowCountLt i x ≤ μ.rowLen i

A row has at most as many entries smaller than x as it has cells.

theorem SemistandardYoungTableau.rowCountLt_mono {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (i : ℕ) {x y : ℕ} (hxy : x ≤ y) : T.rowCountLt i x ≤ T.rowCountLt i y

Counting entries below a larger letter counts more of them.

theorem SemistandardYoungTableau.rowCountLt_succ_le {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (i x : ℕ) : T.rowCountLt (i + 1) (x + 1) ≤ T.rowCountLt i x

The column inequality, in the form everything below rests on: entries increase strictly down a column, so row i + 1 has no more entries smaller than x + 1 than row i has entries smaller than x.

theorem SemistandardYoungTableau.rowCountLt_eq_zero_of_colLen_le {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i : ℕ} (hi : μ.colLen 0 ≤ i) (x : ℕ) : T.rowCountLt i x = 0

A row past the height of the shape has no entries at all.

The block of a letter and its successor

def SemistandardYoungTableau.InBlock {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (v i j : ℕ) : Prop

The cells of T carrying the letter v or the letter v + 1: the ones a Bender-Knuth involution at v may move.

Equations

• T.InBlock v i j = ((i, j) ∈ μ ∧ v ≤ T i j ∧ T i j ≤ v + 1)

@[instance_reducible]

instance SemistandardYoungTableau.instDecidableInBlock {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (v i j : ℕ) : Decidable (T.InBlock v i j)

Equations

• T.instDecidableInBlock v i j = SemistandardYoungTableau.instDecidableInBlock._aux_1 T v i j

theorem SemistandardYoungTableau.inBlock_iff {μ : YoungDiagram} (T : SemistandardYoungTableau μ) {i j : ℕ} (v : ℕ) (hj : (i, j) ∈ μ) : T.InBlock v i j ↔ T.rowCountLt i v ≤ j ∧ j < T.rowCountLt i (v + 2)

The block of a row is the interval of columns from rowCountLt T i v to rowCountLt T i (v + 2).

theorem SemistandardYoungTableau.not_inBlock_of_notMem {μ : YoungDiagram} {T : SemistandardYoungTableau μ} {v i j : ℕ} (hj : (i, j) ∉ μ) : ¬T.InBlock v i j

A cell outside the shape is outside the block.

Recutting a block

structure SemistandardYoungTableau.IsCut {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (v : ℕ) (cut : ℕ → ℕ) : Prop

The recut condition: a family of splitting points, one per row, produces a semistandard filling — SemistandardYoungTableau.recut — as soon as each cut i lies inside the block of row i and no vertically adjacent pair of a v above a v + 1 is broken. The last two clauses say the latter: such a pair sits in the columns of Finset.Ico (rowCountLt T i v) (rowCountLt T (i + 1) (v + 2)), so its v keeps its letter when cut i is at least the right endpoint, and its v + 1 keeps its letter when cut (i + 1) is at most the left one.

This is a sufficient condition, not a necessary one: a row whose block is empty carries no letter that a recut can move, so the recut filling ignores cut i there while the condition still pins it down. Every family of splitting points used here — the tableau's own, and the reflected ones of SemistandardYoungTableau.benderKnuth — satisfies it.

• le_cut (i : ℕ) : T.rowCountLt i v ≤ cut i

  The splitting point of a row is at least the start of its block.

• cut_le (i : ℕ) : cut i ≤ T.rowCountLt i (v + 2)

  The splitting point of a row is at most the end of its block.

• succ_le_cut (i : ℕ) : T.rowCountLt (i + 1) (v + 2) ≤ cut i

  The v of a vertically adjacent pair keeps its letter.

• cut_succ_le (i : ℕ) : cut (i + 1) ≤ T.rowCountLt i v

  The v + 1 of a vertically adjacent pair keeps its letter.

def SemistandardYoungTableau.recut {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (v : ℕ) (cut : ℕ → ℕ) (hcut : T.IsCut v cut) : SemistandardYoungTableau μ

The recut tableau: the semistandard tableau agreeing with T outside the v/(v + 1) blocks, whose blocks are split at the prescribed columns.

Equations

• T.recut v cut hcut = { entry := SemistandardYoungTableau.recutEntry✝ T v cut, row_weak' := ⋯, col_strict' := ⋯, zeros' := ⋯ }

@[simp]

theorem SemistandardYoungTableau.recut_apply {μ : YoungDiagram} {T : SemistandardYoungTableau μ} {v : ℕ} {cut : ℕ → ℕ} (hcut : T.IsCut v cut) (i j : ℕ) : (T.recut v cut hcut) i j = if T.InBlock v i j then if j < cut i then v else v + 1 else T i j

The entries of a recut tableau: inside the block of a row, v before the splitting point and v + 1 after it; everywhere else, the old entry.

theorem SemistandardYoungTableau.recut_apply_of_inBlock {μ : YoungDiagram} {T : SemistandardYoungTableau μ} {v : ℕ} {cut : ℕ → ℕ} (hcut : T.IsCut v cut) {i j : ℕ} (h : T.InBlock v i j) : (T.recut v cut hcut) i j = if j < cut i then v else v + 1

Inside the block, the entry of a recut tableau is v before the splitting point and v + 1 after it.

theorem SemistandardYoungTableau.recut_apply_of_not_inBlock {μ : YoungDiagram} {T : SemistandardYoungTableau μ} {v : ℕ} {cut : ℕ → ℕ} (hcut : T.IsCut v cut) {i j : ℕ} (h : ¬T.InBlock v i j) : (T.recut v cut hcut) i j = T i j

Outside the block, the entry of a recut tableau is the old entry.

theorem SemistandardYoungTableau.inBlock_recut_iff {μ : YoungDiagram} {T : SemistandardYoungTableau μ} {v : ℕ} {cut : ℕ → ℕ} (hcut : T.IsCut v cut) (i j : ℕ) : (T.recut v cut hcut).InBlock v i j ↔ T.InBlock v i j

A recut moves no letter into or out of the block, so the two tableaux have the same blocks.

The row counts of a recut tableau

theorem SemistandardYoungTableau.rowCountLt_recut_of_le {μ : YoungDiagram} {T : SemistandardYoungTableau μ} {v x : ℕ} {cut : ℕ → ℕ} (hcut : T.IsCut v cut) (i : ℕ) (hx : x ≤ v) : (T.recut v cut hcut).rowCountLt i x = T.rowCountLt i x

Below the block, a recut changes no row count.

theorem SemistandardYoungTableau.rowCountLt_recut_of_ge {μ : YoungDiagram} {T : SemistandardYoungTableau μ} {v x : ℕ} {cut : ℕ → ℕ} (hcut : T.IsCut v cut) (i : ℕ) (hx : v + 2 ≤ x) : (T.recut v cut hcut).rowCountLt i x = T.rowCountLt i x

Above the block, a recut changes no row count.

theorem SemistandardYoungTableau.rowCountLt_recut_succ {μ : YoungDiagram} {T : SemistandardYoungTableau μ} {v : ℕ} {cut : ℕ → ℕ} (hcut : T.IsCut v cut) (i : ℕ) : (T.recut v cut hcut).rowCountLt i (v + 1) = cut i

A recut is exactly a change of splitting point: in the recut tableau, the block of row i is split at cut i.

theorem SemistandardYoungTableau.isCut_rowCountLt {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (v : ℕ) : T.IsCut v fun (i : ℕ) => T.rowCountLt i (v + 1)

Recutting at the splitting points of T itself changes nothing.

@[simp]

theorem SemistandardYoungTableau.recut_rowCountLt {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (v : ℕ) : T.recut v (fun (i : ℕ) => T.rowCountLt i (v + 1)) ⋯ = T

theorem SemistandardYoungTableau.IsCut.recut {μ : YoungDiagram} {T : SemistandardYoungTableau μ} {v : ℕ} {cut cut' : ℕ → ℕ} (hcut : T.IsCut v cut) (hcut' : T.IsCut v cut') : (T.recut v cut hcut).IsCut v cut'

A recut condition for T is a recut condition for any recut of T: the constraints depend only on the row counts below and above the block, which a recut leaves alone.

theorem SemistandardYoungTableau.recut_recut {μ : YoungDiagram} {T : SemistandardYoungTableau μ} {v : ℕ} {cut cut' : ℕ → ℕ} (hcut : T.IsCut v cut) (hcut' : T.IsCut v cut') : (T.recut v cut hcut).recut v cut' ⋯ = T.recut v cut' hcut'

Recutting twice is recutting once.

The content of a recut tableau

theorem SemistandardYoungTableau.filter_recut_eq {μ : YoungDiagram} {T : SemistandardYoungTableau μ} {v : ℕ} {cut : ℕ → ℕ} (hcut : T.IsCut v cut) (i : ℕ) : {j ∈ Finset.range (μ.rowLen i) | (T.recut v cut hcut) i j = v} = Finset.Ico (T.rowCountLt i v) (cut i)

Inside a row, the cells of a recut tableau carrying the letter v are those from the start of the block to the splitting point.

theorem SemistandardYoungTableau.filter_recut_eq_succ {μ : YoungDiagram} {T : SemistandardYoungTableau μ} {v : ℕ} {cut : ℕ → ℕ} (hcut : T.IsCut v cut) (i : ℕ) : {j ∈ Finset.range (μ.rowLen i) | (T.recut v cut hcut) i j = v + 1} = Finset.Ico (cut i) (T.rowCountLt i (v + 2))

Inside a row, the cells of a recut tableau carrying the letter v + 1 are those from the splitting point to the end of the block.

theorem SemistandardYoungTableau.content_recut_of_ne {μ : YoungDiagram} {T : SemistandardYoungTableau μ} {v x : ℕ} {cut : ℕ → ℕ} (hcut : T.IsCut v cut) (hx : x ≠ v) (hx' : x ≠ v + 1) : (T.recut v cut hcut).content x = T.content x

A recut moves no letter other than v and v + 1.

theorem SemistandardYoungTableau.content_recut {μ : YoungDiagram} {T : SemistandardYoungTableau μ} {v : ℕ} {cut : ℕ → ℕ} (hcut : T.IsCut v cut) : (T.recut v cut hcut).content v = ∑ i ∈ Finset.range (μ.colLen 0), (cut i - T.rowCountLt i v)

How often the letter v occurs in a recut tableau, counted row by row.

theorem SemistandardYoungTableau.content_recut_succ {μ : YoungDiagram} {T : SemistandardYoungTableau μ} {v : ℕ} {cut : ℕ → ℕ} (hcut : T.IsCut v cut) : (T.recut v cut hcut).content (v + 1) = ∑ i ∈ Finset.range (μ.colLen 0), (T.rowCountLt i (v + 2) - cut i)

How often the letter v + 1 occurs in a recut tableau, counted row by row.

theorem SemistandardYoungTableau.content_eq_sum {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (v : ℕ) : T.content v = ∑ i ∈ Finset.range (μ.colLen 0), (T.rowCountLt i (v + 1) - T.rowCountLt i v)

How often the letter v occurs in a tableau, counted row by row: it is the recut count at the tableau's own splitting points.

theorem SemistandardYoungTableau.content_succ_eq_sum {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (v : ℕ) : T.content (v + 1) = ∑ i ∈ Finset.range (μ.colLen 0), (T.rowCountLt i (v + 2) - T.rowCountLt i (v + 1))

How often the letter v + 1 occurs in a tableau, counted row by row.

theorem SemistandardYoungTableau.content_recut_add {μ : YoungDiagram} {T : SemistandardYoungTableau μ} {v : ℕ} {cut : ℕ → ℕ} (hcut : T.IsCut v cut) : (T.recut v cut hcut).content v + (T.recut v cut hcut).content (v + 1) = T.content v + T.content (v + 1)

A recut preserves how many cells carry one of the two letters v and v + 1; it only moves the boundary between them.

The Bender-Knuth involution

def SemistandardYoungTableau.benderKnuth {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (v : ℕ) : SemistandardYoungTableau μ

The Bender-Knuth involution at the letter v: the recut of T at the reflected splitting points.

Equations

• T.benderKnuth v = T.recut v (SemistandardYoungTableau.bkCut✝ T v) ⋯

theorem SemistandardYoungTableau.benderKnuth_apply_of_not_inBlock {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (v : ℕ) {i j : ℕ} (h : ¬T.InBlock v i j) : (T.benderKnuth v) i j = T i j

Outside the block, the involution leaves the entry alone.

theorem SemistandardYoungTableau.benderKnuth_apply_eq_or {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (v i j : ℕ) : (T.benderKnuth v) i j = T i j ∨ (T.benderKnuth v) i j = v ∨ (T.benderKnuth v) i j = v + 1

The involution writes no letter other than the ones already there and the two it exchanges.

theorem SemistandardYoungTableau.inBlock_benderKnuth_iff {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (v i j : ℕ) : (T.benderKnuth v).InBlock v i j ↔ T.InBlock v i j

The involution moves no letter into or out of the block, so it leaves the block alone.

theorem SemistandardYoungTableau.rowCountLt_benderKnuth_of_le {μ : YoungDiagram} {x : ℕ} (T : SemistandardYoungTableau μ) (v i : ℕ) (hx : x ≤ v) : (T.benderKnuth v).rowCountLt i x = T.rowCountLt i x

theorem SemistandardYoungTableau.rowCountLt_benderKnuth_of_ge {μ : YoungDiagram} {x : ℕ} (T : SemistandardYoungTableau μ) (v i : ℕ) (hx : v + 2 ≤ x) : (T.benderKnuth v).rowCountLt i x = T.rowCountLt i x

@[simp]

theorem SemistandardYoungTableau.benderKnuth_benderKnuth {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (v : ℕ) : (T.benderKnuth v).benderKnuth v = T

The Bender-Knuth involution is an involution.

theorem SemistandardYoungTableau.benderKnuth_involutive (μ : YoungDiagram) (v : ℕ) : Function.Involutive fun (T : SemistandardYoungTableau μ) => T.benderKnuth v

The effect on the content

theorem SemistandardYoungTableau.content_benderKnuth_self {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (v : ℕ) : (T.benderKnuth v).content v = T.content (v + 1)

The Bender-Knuth involution exchanges the two letters it is named for: after it, the letter v occurs as often as v + 1 did.

theorem SemistandardYoungTableau.content_benderKnuth_succ {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (v : ℕ) : (T.benderKnuth v).content (v + 1) = T.content v

The Bender-Knuth involution exchanges the two letters it is named for: after it, the letter v + 1 occurs as often as v did.

theorem SemistandardYoungTableau.content_benderKnuth_of_ne {μ : YoungDiagram} {x : ℕ} (T : SemistandardYoungTableau μ) (v : ℕ) (hx : x ≠ v) (hx' : x ≠ v + 1) : (T.benderKnuth v).content x = T.content x

The Bender-Knuth involution leaves every other letter alone.

@[simp]

theorem SemistandardYoungTableau.content_benderKnuth {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (v x : ℕ) : (T.benderKnuth v).content x = T.content ((Equiv.swap v (v + 1)) x)

The Bender-Knuth involution exchanges the multiplicities of v and v + 1 and fixes every other one.