mathlib documentation

combinatorics.young_diagram

Young diagrams #

A Young diagram is a finite set of up-left justified boxes:

□□□□□
□□□
□□□
□

This Young diagram corresponds to the [5, 3, 3, 1] partition of 12.

We represent it as a lower set in ℕ × ℕ in the product partial order. We write (i, j) ∈ μ to say that (i, j) (in matrix coordinates) is in the Young diagram μ.

Main definitions #

Notation #

In "English notation", a Young diagram is drawn so that (i1, j1) ≤ (i2, j2) means (i1, j1) is weakly up-and-left of (i2, j2). This terminology is used below, e.g. in young_diagram.up_left_mem.

Tags #

Young diagram

References #

https://en.wikipedia.org/wiki/Young_tableau

theorem young_diagram.ext (x y : young_diagram) (h : x.cells = y.cells) :
x = y
@[ext]
structure young_diagram  :
Type

A Young diagram is a finite collection of cells on the ℕ × ℕ grid such that whenever a cell is present, so are all the ones above and to the left of it. Like matrices, an (i, j) cell is a cell in row i and column j, where rows are enumerated downward and columns rightward.

Young diagrams are modeled as finite sets in ℕ × ℕ that are lower sets with respect to the standard order on products.

Instances for young_diagram
@[protected, instance]
Equations
@[simp]
theorem young_diagram.mem_cells {μ : young_diagram} (c : × ) :
c μ.cells c μ
@[simp]
theorem young_diagram.mem_mk (c : × ) (cells : finset ( × )) (is_lower_set : _root_.is_lower_set cells) :
c {cells := cells, is_lower_set := is_lower_set} c cells
@[protected, instance]
Equations
theorem young_diagram.up_left_mem (μ : young_diagram) {i1 i2 j1 j2 : } (hi : i1 i2) (hj : j1 j2) (hcell : (i2, j2) μ) :
(i1, j1) μ

In "English notation", a Young diagram is drawn so that (i1, j1) ≤ (i2, j2) means (i1, j1) is weakly up-and-left of (i2, j2).

@[simp]
@[simp]
theorem young_diagram.cells_ssubset_iff {μ ν : young_diagram} :
μ.cells ν.cells μ < ν
@[protected, instance]
Equations
@[simp]
theorem young_diagram.cells_sup (μ ν : young_diagram) :
ν).cells = μ.cells ν.cells
@[simp, norm_cast]
theorem young_diagram.coe_sup (μ ν : young_diagram) :
ν) = μ ν
@[simp]
theorem young_diagram.mem_sup {μ ν : young_diagram} {x : × } :
x μ ν x μ x ν
@[protected, instance]
Equations
@[simp]
theorem young_diagram.cells_inf (μ ν : young_diagram) :
ν).cells = μ.cells ν.cells
@[simp, norm_cast]
theorem young_diagram.coe_inf (μ ν : young_diagram) :
ν) = μ ν
@[simp]
theorem young_diagram.mem_inf {μ ν : young_diagram} {x : × } :
x μ ν x μ x ν
@[protected, instance]

The empty Young diagram is (⊥ : young_diagram).

Equations
@[simp, norm_cast]
@[simp]
theorem young_diagram.not_mem_bot (x : × ) :
@[protected, instance]
Equations
@[protected, reducible]

Cardinality of a Young diagram

Equations

The transpose of a Young diagram is obtained by swapping i's with j's.

Equations
@[simp]
@[simp]
@[protected]
theorem young_diagram.le_of_transpose_le {μ ν : young_diagram} (h_le : μ.transpose ν) :
@[protected]
theorem young_diagram.transpose_mono {μ ν : young_diagram} (h_le : μ ν) :

Transposing Young diagrams is an order_iso.

Equations

Rows and row lengths of Young diagrams. #

This section defines μ.row and μ.row_len, with the following API: 1. (i, j) ∈ μ ↔ j < μ.row_len i 2. μ.row i = {i} ×ˢ (finset.range (μ.row_len i)) 3. μ.row_len i = (μ.row i).card 4. ∀ {i1 i2}, i1 ≤ i2 → μ.row_len i2 ≤ μ.row_len i1

Note: #3 is not convenient for defining μ.row_len; instead, μ.row_len is defined as the smallest j such that (i, j) ∉ μ.

The i-th row of a Young diagram consists of the cells whose first coordinate is i.

Equations
theorem young_diagram.mem_row_iff {μ : young_diagram} {i : } {c : × } :
c μ.row i c μ c.fst = i
theorem young_diagram.mk_mem_row_iff {μ : young_diagram} {i j : } :
(i, j) μ.row i (i, j) μ
@[protected]
theorem young_diagram.exists_not_mem_row (μ : young_diagram) (i : ) :
∃ (j : ), (i, j) μ

Length of a row of a Young diagram

Equations
theorem young_diagram.mem_iff_lt_row_len {μ : young_diagram} {i j : } :
(i, j) μ j < μ.row_len i
theorem young_diagram.row_eq_prod {μ : young_diagram} {i : } :
μ.row i = {i} ×ˢ finset.range (μ.row_len i)
theorem young_diagram.row_len_eq_card (μ : young_diagram) {i : } :
μ.row_len i = (μ.row i).card
theorem young_diagram.row_len_anti (μ : young_diagram) (i1 i2 : ) (hi : i1 i2) :
μ.row_len i2 μ.row_len i1

Columns and column lengths of Young diagrams. #

This section has an identical API to the rows section.

The j-th column of a Young diagram consists of the cells whose second coordinate is j.

Equations
theorem young_diagram.mem_col_iff {μ : young_diagram} {j : } {c : × } :
c μ.col j c μ c.snd = j
theorem young_diagram.mk_mem_col_iff {μ : young_diagram} {i j : } :
(i, j) μ.col j (i, j) μ
@[protected]
theorem young_diagram.exists_not_mem_col (μ : young_diagram) (j : ) :
∃ (i : ), (i, j) μ.cells

Length of a column of a Young diagram

Equations
theorem young_diagram.mem_iff_lt_col_len {μ : young_diagram} {i j : } :
(i, j) μ i < μ.col_len j
theorem young_diagram.col_eq_prod {μ : young_diagram} {j : } :
μ.col j = finset.range (μ.col_len j) ×ˢ {j}
theorem young_diagram.col_len_eq_card (μ : young_diagram) {j : } :
μ.col_len j = (μ.col j).card
theorem young_diagram.col_len_anti (μ : young_diagram) (j1 j2 : ) (hj : j1 j2) :
μ.col_len j2 μ.col_len j1