Addable cells of a Young diagram and their contents

A cell c is addable to a Young diagram μ if c ∉ μ while every cell strictly below c in the product order lies in μ; equivalently, adding c alone to μ gives a Young diagram, in which c is a corner. Addable cells are the dual of the corners of YoungDiagram.IsCorner: they index the edges μ ⊂ μ + c of the Young graph leaving μ, and hence the one-box branching rules for symmetric groups and Hecke algebras.

The content of the cell (i, j) is j - i, its column index minus its row index. On a fixed Young diagram the contents of the addable cells are well separated: two distinct addable cells of μ have contents differing by at least 2 and by at most μ.card + 1. The upper bound is sharp: for every d ≥ 2, some diagram μ with μ.card + 1 = d has two addable cells whose contents differ by exactly d (for d = 2 this also attains the lower bound). On the semisimple Hecke algebra Hₙ(q) with Q = q² the Jucys–Murphy elements act on the new box of a one-box branching μ ⊂ μ + c by the eigenvalue Q ^ content c. The bounds above therefore say exactly when those eigenvalues separate the branches: for every diagram of size less than n the map c ↦ Q ^ content c is injective on addable cells if and only if Q ^ d ≠ 1 for 2 ≤ d ≤ n.

Main definitions

• YoungDiagram.IsAddable: the predicate cutting out the addable cells of a diagram.
• YoungDiagram.addables: the addable cells of a diagram, as a finite set of cells.
• YoungDiagram.addCell: the diagram with the principal lower set of a cell added; at an addable cell exactly that cell is added.

The content YoungDiagram.cellContent of a cell is defined in TauCeti.Combinatorics.Young.Diagram.

Main results

• YoungDiagram.isAddable_iff_isLowerSet: a cell outside μ is addable exactly when adding it to μ gives a Young diagram.
• YoungDiagram.addCell_le_iff: addCell μ c is the least diagram containing μ and c.
• YoungDiagram.IsAddable.rowLen_addCell and YoungDiagram.IsAddable.colLen_addCell: adding an addable cell lengthens its row and its column by one and leaves the others unchanged.
• YoungDiagram.isAddable_iff_rowLen: the cell (i, j) is addable exactly when j is the length of row i and, unless i = 0, row i is shorter than row i - 1.
• YoungDiagram.IsAddable.isCorner_addCell and YoungDiagram.IsCorner.isAddable_erase, with YoungDiagram.IsAddable.erase_addCell and YoungDiagram.IsCorner.addCell_erase: adding an addable cell and removing a corner are mutually inverse.
• YoungDiagram.IsAddable.two_le_cellContent_sub and YoungDiagram.IsAddable.cellContent_sub_le: contents of distinct addable cells differ by at least 2 and at most μ.card + 1.
• YoungDiagram.injOn_zpow_cellContent_iff: the powers Q ^ content c separate the addable cells of every diagram of size less than n if and only if Q ^ d ≠ 1 for 2 ≤ d ≤ n.

References

• W. Fulton, Young Tableaux, Section 1.1.
• A. Okounkov, A. Vershik, A new approach to representation theory of symmetric groups, Selecta Math. 2 (1996), 581–605, Section 5, where contents of addable cells give the spectrum of the Jucys–Murphy elements.
• A. Ram, Seminormal representations of Weyl groups and Iwahori-Hecke algebras, Proc. London Math. Soc. 75 (1997), 99–133, for the Hecke eigenvalues Q ^ content.

Addable cells

def YoungDiagram.IsAddable (μ : YoungDiagram) (c : ℕ × ℕ) : Prop

A cell c is addable to μ if it is not a cell of μ while every cell strictly below it in the product order is. These are exactly the cells outside μ whose addition on its own to μ gives a Young diagram (YoungDiagram.isAddable_iff_isLowerSet).

theorem YoungDiagram.isAddable_def (μ : YoungDiagram) (c : ℕ × ℕ) : μ.IsAddable c ↔ c ∉ μ ∧ ∀ d < c, d ∈ μ

The defining conjunction of YoungDiagram.IsAddable, for introducing and eliminating the predicate.

@[instance_reducible]

instance YoungDiagram.instDecidableIsAddable (μ : YoungDiagram) (c : ℕ × ℕ) : Decidable (μ.IsAddable c)

theorem YoungDiagram.IsAddable.notMem {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsAddable c) : c ∉ μ

theorem YoungDiagram.IsAddable.mem_of_lt {μ : YoungDiagram} {c d : ℕ × ℕ} (h : μ.IsAddable c) (hd : d < c) : d ∈ μ

theorem YoungDiagram.IsAddable.mem_left {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsAddable c) {j : ℕ} (hj : c.2 = j + 1) : (c.1, j) ∈ μ

The cell to the left of an addable cell lies in the diagram.

theorem YoungDiagram.IsAddable.mem_above {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsAddable c) {i : ℕ} (hi : c.1 = i + 1) : (i, c.2) ∈ μ

The cell above an addable cell lies in the diagram.

theorem YoungDiagram.IsAddable.snd_eq_rowLen {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsAddable c) : c.2 = μ.rowLen c.1

An addable cell sits at the end of its row.

theorem YoungDiagram.IsAddable.fst_eq_colLen {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsAddable c) : c.1 = μ.colLen c.2

An addable cell sits at the end of its column.

theorem YoungDiagram.IsAddable.eq_of_fst_eq {μ : YoungDiagram} {c d : ℕ × ℕ} (hc : μ.IsAddable c) (hd : μ.IsAddable d) (h : c.1 = d.1) : c = d

The addable cells of a diagram sit in distinct rows.

theorem YoungDiagram.IsAddable.fst_le_colLen_zero {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsAddable c) : c.1 ≤ μ.colLen 0

An addable cell lies in one of the rows of the diagram or in the row just below them.

def YoungDiagram.addables (μ : YoungDiagram) : Finset (ℕ × ℕ)

The addable cells of a Young diagram, as a finite set of cells: each is the cell just past the end of one of the rows 0, …, μ.colLen 0.

@[simp]

theorem YoungDiagram.mem_addables {μ : YoungDiagram} {c : ℕ × ℕ} : c ∈ μ.addables ↔ μ.IsAddable c

theorem YoungDiagram.isAddable_iff_rowLen {μ : YoungDiagram} {i j : ℕ} : μ.IsAddable (i, j) ↔ j = μ.rowLen i ∧ ∀ (i' : ℕ), i = i' + 1 → j < μ.rowLen i'

Addable cells by row lengths. The cell (i, j) is addable to μ exactly when j is the length of row i and, unless i = 0, row i is strictly shorter than row i - 1.

@[simp]

theorem YoungDiagram.isAddable_transpose {μ : YoungDiagram} {c : ℕ × ℕ} : μ.transpose.IsAddable c ↔ μ.IsAddable c.swap

Transposition exchanges the addable cells of μ and μ.transpose.

Adding a cell

def YoungDiagram.addCell (μ : YoungDiagram) (c : ℕ × ℕ) : YoungDiagram

The Young diagram obtained from μ by adding the cell c together with every cell below it in the product order. It is defined without a hypothesis on c, dually to YoungDiagram.erase; at an addable cell exactly the cell c is added (YoungDiagram.IsAddable.cells_addCell_eq_insert).

theorem YoungDiagram.cells_addCell (μ : YoungDiagram) (c : ℕ × ℕ) : (μ.addCell c).cells = μ.cells ∪ Finset.range (c.1 + 1) ×ˢ Finset.range (c.2 + 1)

@[simp]

theorem YoungDiagram.mem_addCell {μ : YoungDiagram} {c d : ℕ × ℕ} : d ∈ μ.addCell c ↔ d ∈ μ ∨ d ≤ c

theorem YoungDiagram.le_addCell (μ : YoungDiagram) (c : ℕ × ℕ) : μ ≤ μ.addCell c

theorem YoungDiagram.mem_addCell_self (μ : YoungDiagram) (c : ℕ × ℕ) : c ∈ μ.addCell c

@[simp]

theorem YoungDiagram.addCell_le_iff {μ : YoungDiagram} {c : ℕ × ℕ} {ν : YoungDiagram} : μ.addCell c ≤ ν ↔ μ ≤ ν ∧ c ∈ ν

addCell μ c is the least Young diagram containing μ and the cell c.

theorem YoungDiagram.IsAddable.mem_addCell_iff {μ : YoungDiagram} {c d : ℕ × ℕ} (h : μ.IsAddable c) : d ∈ μ.addCell c ↔ d ∈ μ ∨ d = c

Adding an addable cell adds exactly that cell.

@[simp]

theorem YoungDiagram.IsAddable.cells_addCell_eq_insert {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsAddable c) : (μ.addCell c).cells = insert c μ.cells

@[simp]

theorem YoungDiagram.IsAddable.card_addCell {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsAddable c) : (μ.addCell c).card = μ.card + 1

Adding an addable cell raises the number of cells by one.

@[simp]

theorem YoungDiagram.IsAddable.rowLen_addCell {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsAddable c) (i : ℕ) : (μ.addCell c).rowLen i = if c.1 = i then μ.rowLen i + 1 else μ.rowLen i

Adding an addable cell lengthens its row by one and leaves every other row unchanged.

@[simp]

theorem YoungDiagram.IsAddable.colLen_addCell {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsAddable c) (j : ℕ) : (μ.addCell c).colLen j = if c.2 = j then μ.colLen j + 1 else μ.colLen j

Adding an addable cell lengthens its column by one and leaves every other column unchanged.

theorem YoungDiagram.IsAddable.isCorner_addCell {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsAddable c) : (μ.addCell c).IsCorner c

An addable cell is a corner of the diagram obtained by adding it.

@[simp]

theorem YoungDiagram.IsAddable.erase_addCell {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsAddable c) : (μ.addCell c).erase c = μ

Removing an addable cell after adding it recovers the diagram.

theorem YoungDiagram.isAddable_iff_isLowerSet {μ : YoungDiagram} {c : ℕ × ℕ} : μ.IsAddable c ↔ c ∉ μ ∧ IsLowerSet (insert c ↑μ.cells)

A cell is addable to μ exactly when it lies outside μ and adding it to the cells of μ gives a lower set, that is, the cells of a Young diagram.

theorem YoungDiagram.IsCorner.isAddable_erase {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsCorner c) : (μ.erase c).IsAddable c

A corner of μ is addable to the diagram obtained by removing it.

@[simp]

theorem YoungDiagram.IsCorner.addCell_erase {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsCorner c) : (μ.erase c).addCell c = μ

Adding a corner back after removing it recovers the diagram.

@[simp]

theorem YoungDiagram.addCell_transpose (μ : YoungDiagram) (c : ℕ × ℕ) : μ.transpose.addCell c = (μ.addCell c.swap).transpose

Contents

theorem YoungDiagram.IsAddable.two_le_cellContent_sub {μ : YoungDiagram} {c d : ℕ × ℕ} (hc : μ.IsAddable c) (hd : μ.IsAddable d) (h : c.1 < d.1) : 2 ≤ cellContent c - cellContent d

Addable contents are 2-separated. If the addable cell c lies in a higher row than the addable cell d, then the content of c exceeds that of d by at least 2.

theorem YoungDiagram.IsAddable.cellContent_sub_le {μ : YoungDiagram} {c d : ℕ × ℕ} (hc : μ.IsAddable c) (hd : μ.IsAddable d) : cellContent c - cellContent d ≤ ↑μ.card + 1

Addable contents are bounded. The contents of two addable cells of μ differ by at most μ.card + 1.

theorem YoungDiagram.IsAddable.natAbs_cellContent_sub_mem {μ : YoungDiagram} {c d : ℕ × ℕ} (hc : μ.IsAddable c) (hd : μ.IsAddable d) (hne : c ≠ d) : (cellContent c - cellContent d).natAbs ∈ Finset.Icc 2 (μ.card + 1)

Distinct addable cells of μ have contents at distance between 2 and μ.card + 1.

theorem YoungDiagram.injOn_cellContent (μ : YoungDiagram) : Set.InjOn cellContent {c : ℕ × ℕ | μ.IsAddable c}

Distinct addable cells of a Young diagram have distinct contents.

theorem YoungDiagram.exists_isAddable_cellContent_sub_eq {d : ℕ} (hd : 2 ≤ d) : ∃ (μ : YoungDiagram), μ.card + 1 = d ∧ ∃ (c : ℕ × ℕ) (c' : ℕ × ℕ), μ.IsAddable c ∧ μ.IsAddable c' ∧ cellContent c - cellContent c' = ↑d

The upper content bound is sharp. For 2 ≤ d, some diagram of size d - 1 has two addable cells whose contents differ by exactly d: the one-row diagram with d - 1 cells has the addable cells (0, d - 1) and (1, 0).

Separation by the powers of a parameter

theorem YoungDiagram.injOn_zpow_cellContent {μ : YoungDiagram} {G : Type u_1} [Group G] {Q : G} {n : ℕ} (hQ : ∀ (d : ℕ), 2 ≤ d → d ≤ n → Q ^ d ≠ 1) (hμ : μ.card < n) : Set.InjOn (fun (c : ℕ × ℕ) => Q ^ cellContent c) {c : ℕ × ℕ | μ.IsAddable c}

Separation of Q-contents. If Q ^ d ≠ 1 for 2 ≤ d ≤ n, then on every Young diagram of size less than n the powers Q ^ content c of distinct addable cells are distinct.

theorem YoungDiagram.injOn_zpow_cellContent_iff {G : Type u_1} [Group G] {Q : G} {n : ℕ} : (∀ (μ : YoungDiagram), μ.card < n → Set.InjOn (fun (c : ℕ × ℕ) => Q ^ cellContent c) {c : ℕ × ℕ | μ.IsAddable c}) ↔ ∀ (d : ℕ), 2 ≤ d → d ≤ n → Q ^ d ≠ 1

The separation criterion is sharp. The powers Q ^ content c separate the addable cells of every Young diagram of size less than n if and only if Q ^ d ≠ 1 for 2 ≤ d ≤ n.