# 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 #

• YoungDiagram : Young diagrams
• YoungDiagram.card : the number of cells in a Young diagram (its cardinality)
• YoungDiagram.instDistribLatticeYoungDiagram : a distributive lattice instance for Young diagrams ordered by containment, with (⊥ : YoungDiagram) the empty diagram.
• YoungDiagram.row and YoungDiagram.rowLen: rows of a Young diagram and their lengths
• YoungDiagram.col and YoungDiagram.colLen: columns of a Young diagram and their lengths

## 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 YoungDiagram.up_left_mem.

Young diagram

## References #

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

theorem YoungDiagram.ext (x : YoungDiagram) (y : YoungDiagram) (cells : x.cells = y.cells) :
x = y
theorem YoungDiagram.ext_iff (x : YoungDiagram) (y : YoungDiagram) :
x = y x.cells = y.cells
structure YoungDiagram :

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.

• cells : Finset ()

A finite set which represents a finite collection of cells on the ℕ × ℕ grid.

• isLowerSet : IsLowerSet self.cells

Cells are up-left justified, witnessed by the fact that cells is a lower set in ℕ × ℕ.

Instances For
theorem YoungDiagram.isLowerSet (self : YoungDiagram) :
IsLowerSet self.cells

Cells are up-left justified, witnessed by the fact that cells is a lower set in ℕ × ℕ.

@[simp]
theorem YoungDiagram.mem_cells {μ : YoungDiagram} (c : ) :
c μ.cells c μ
@[simp]
theorem YoungDiagram.mem_mk (c : ) (cells : Finset ()) (isLowerSet : IsLowerSet cells) :
c { cells := cells, isLowerSet := isLowerSet } c cells
instance YoungDiagram.decidableMem (μ : YoungDiagram) :
DecidablePred fun (x : ) => x μ
Equations
theorem YoungDiagram.up_left_mem (μ : YoungDiagram) {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]
theorem YoungDiagram.cells_subset_iff {μ : YoungDiagram} {ν : YoungDiagram} :
μ.cells ν.cells μ ν
@[simp]
theorem YoungDiagram.cells_ssubset_iff {μ : YoungDiagram} {ν : YoungDiagram} :
μ.cells ν.cells μ < ν
Equations
@[simp]
theorem YoungDiagram.cells_sup (μ : YoungDiagram) (ν : YoungDiagram) :
(μ ν).cells = μ.cells ν.cells
@[simp]
theorem YoungDiagram.coe_sup (μ : YoungDiagram) (ν : YoungDiagram) :
(μ ν) = μ ν
@[simp]
theorem YoungDiagram.mem_sup {μ : YoungDiagram} {ν : YoungDiagram} {x : } :
x μ ν x μ x ν
Equations
@[simp]
theorem YoungDiagram.cells_inf (μ : YoungDiagram) (ν : YoungDiagram) :
(μ ν).cells = μ.cells ν.cells
@[simp]
theorem YoungDiagram.coe_inf (μ : YoungDiagram) (ν : YoungDiagram) :
(μ ν) = μ ν
@[simp]
theorem YoungDiagram.mem_inf {μ : YoungDiagram} {ν : YoungDiagram} {x : } :
x μ ν x μ x ν

The empty Young diagram is (⊥ : young_diagram).

Equations
@[simp]
@[simp]
theorem YoungDiagram.not_mem_bot (x : ) :
x
Equations
Equations
• One or more equations did not get rendered due to their size.
@[reducible, inline]

Cardinality of a Young diagram

Equations
• μ.card = μ.cells.card
Instances For

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

Equations
• μ.transpose = { cells := ().finsetCongr μ.cells, isLowerSet := }
Instances For
@[simp]
theorem YoungDiagram.mem_transpose {μ : YoungDiagram} {c : } :
c μ.transpose c.swap μ
@[simp]
theorem YoungDiagram.transpose_transpose (μ : YoungDiagram) :
μ.transpose.transpose = μ
theorem YoungDiagram.transpose_eq_iff_eq_transpose {μ : YoungDiagram} {ν : YoungDiagram} :
μ.transpose = ν μ = ν.transpose
@[simp]
theorem YoungDiagram.transpose_eq_iff {μ : YoungDiagram} {ν : YoungDiagram} :
μ.transpose = ν.transpose μ = ν
theorem YoungDiagram.le_of_transpose_le {μ : YoungDiagram} {ν : YoungDiagram} (h_le : μ.transpose ν) :
μ ν.transpose
@[simp]
theorem YoungDiagram.transpose_le_iff {μ : YoungDiagram} {ν : YoungDiagram} :
μ.transpose ν.transpose μ ν
theorem YoungDiagram.transpose_mono {μ : YoungDiagram} {ν : YoungDiagram} (h_le : μ ν) :
μ.transpose ν.transpose
@[simp]
@[simp]
theorem YoungDiagram.transposeOrderIso_apply (μ : YoungDiagram) :
YoungDiagram.transposeOrderIso μ = μ.transpose

Transposing Young diagrams is an OrderIso.

Equations
• One or more equations did not get rendered due to their size.
Instances For

### Rows and row lengths of Young diagrams. #

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

Note: #3 is not convenient for defining μ.rowLen; instead, μ.rowLen 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
Instances For
theorem YoungDiagram.mem_row_iff {μ : YoungDiagram} {i : } {c : } :
c μ.row i c μ c.1 = i
theorem YoungDiagram.mk_mem_row_iff {μ : YoungDiagram} {i : } {j : } :
(i, j) μ.row i (i, j) μ
theorem YoungDiagram.exists_not_mem_row (μ : YoungDiagram) (i : ) :
∃ (j : ), (i, j)μ

Length of a row of a Young diagram

Equations
• μ.rowLen i =
Instances For
theorem YoungDiagram.mem_iff_lt_rowLen {μ : YoungDiagram} {i : } {j : } :
(i, j) μ j < μ.rowLen i
theorem YoungDiagram.row_eq_prod {μ : YoungDiagram} {i : } :
μ.row i = {i} ×ˢ Finset.range (μ.rowLen i)
theorem YoungDiagram.rowLen_eq_card (μ : YoungDiagram) {i : } :
μ.rowLen i = (μ.row i).card
theorem YoungDiagram.rowLen_anti (μ : YoungDiagram) (i1 : ) (i2 : ) (hi : i1 i2) :
μ.rowLen i2 μ.rowLen 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
Instances For
theorem YoungDiagram.mem_col_iff {μ : YoungDiagram} {j : } {c : } :
c μ.col j c μ c.2 = j
theorem YoungDiagram.mk_mem_col_iff {μ : YoungDiagram} {i : } {j : } :
(i, j) μ.col j (i, j) μ
theorem YoungDiagram.exists_not_mem_col (μ : YoungDiagram) (j : ) :
∃ (i : ), (i, j)μ.cells

Length of a column of a Young diagram

Equations
• μ.colLen j =
Instances For
@[simp]
theorem YoungDiagram.colLen_transpose (μ : YoungDiagram) (j : ) :
μ.transpose.colLen j = μ.rowLen j
@[simp]
theorem YoungDiagram.rowLen_transpose (μ : YoungDiagram) (i : ) :
μ.transpose.rowLen i = μ.colLen i
theorem YoungDiagram.mem_iff_lt_colLen {μ : YoungDiagram} {i : } {j : } :
(i, j) μ i < μ.colLen j
theorem YoungDiagram.col_eq_prod {μ : YoungDiagram} {j : } :
μ.col j = Finset.range (μ.colLen j) ×ˢ {j}
theorem YoungDiagram.colLen_eq_card (μ : YoungDiagram) {j : } :
μ.colLen j = (μ.col j).card
theorem YoungDiagram.colLen_anti (μ : YoungDiagram) (j1 : ) (j2 : ) (hj : j1 j2) :
μ.colLen j2 μ.colLen j1

### The list of row lengths of a Young diagram #

This section defines μ.rowLens : List ℕ, the list of row lengths of a Young diagram μ.

1. YoungDiagram.rowLens_sorted : It is weakly decreasing (List.Sorted (· ≥ ·)).
2. YoungDiagram.rowLens_pos : It is strictly positive.

List of row lengths of a Young diagram

Equations
Instances For
@[simp]
theorem YoungDiagram.get_rowLens {μ : YoungDiagram} {i : Fin μ.rowLens.length} :
μ.rowLens.get i = μ.rowLen i
@[simp]
theorem YoungDiagram.length_rowLens {μ : YoungDiagram} :
μ.rowLens.length = μ.colLen 0
theorem YoungDiagram.rowLens_sorted (μ : YoungDiagram) :
List.Sorted (fun (x x_1 : ) => x x_1) μ.rowLens
theorem YoungDiagram.pos_of_mem_rowLens (μ : YoungDiagram) (x : ) (hx : x μ.rowLens) :
0 < x

### Equivalence between Young diagrams and lists of natural numbers #

This section defines the equivalence between Young diagrams μ and weakly decreasing lists w of positive natural numbers, corresponding to row lengths of the diagram: YoungDiagram.equivListRowLens : YoungDiagram ≃ {w : List ℕ // w.Sorted (· ≥ ·) ∧ ∀ x ∈ w, 0 < x}

The two directions are YoungDiagram.rowLens (defined above) and YoungDiagram.ofRowLens.

The cells making up a YoungDiagram from a list of row lengths

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem YoungDiagram.mem_cellsOfRowLens {w : } {c : } :
∃ (h : c.1 < w.length), c.2 < w.get c.1, h
def YoungDiagram.ofRowLens (w : ) (hw : List.Sorted (fun (x x_1 : ) => x x_1) w) :

Young diagram from a sorted list

Equations
• = { cells := , isLowerSet := }
Instances For
theorem YoungDiagram.mem_ofRowLens {w : } {hw : List.Sorted (fun (x x_1 : ) => x x_1) w} {c : } :
c ∃ (h : c.1 < w.length), c.2 < w.get c.1, h
theorem YoungDiagram.rowLens_length_ofRowLens {w : } {hw : List.Sorted (fun (x x_1 : ) => x x_1) w} (hpos : xw, 0 < x) :
().rowLens.length = w.length

The number of rows in ofRowLens w hw is the length of w

theorem YoungDiagram.rowLen_ofRowLens {w : } {hw : List.Sorted (fun (x x_1 : ) => x x_1) w} (i : Fin w.length) :
().rowLen i = w.get i

The length of the ith row in ofRowLens w hw is the ith entry of w

The left_inv direction of the equivalence

theorem YoungDiagram.rowLens_ofRowLens_eq_self {w : } {hw : List.Sorted (fun (x x_1 : ) => x x_1) w} (hpos : xw, 0 < x) :
().rowLens = w

The right_inv direction of the equivalence

@[simp]
theorem YoungDiagram.equivListRowLens_symm_apply (ww : { w : // List.Sorted (fun (x x_1 : ) => x x_1) w xw, 0 < x }) :
=
@[simp]
theorem YoungDiagram.equivListRowLens_apply_coe (μ : YoungDiagram) :
(YoungDiagram.equivListRowLens μ) = μ.rowLens
def YoungDiagram.equivListRowLens :
YoungDiagram { w : // List.Sorted (fun (x x_1 : ) => x x_1) w xw, 0 < x }

Equivalence between Young diagrams and weakly decreasing lists of positive natural numbers. A Young diagram μ is equivalent to a list of row lengths.

Equations
• One or more equations did not get rendered due to their size.
Instances For