# mathlib3documentation

combinatorics.young.young_diagram

# Young diagrams #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• young_diagram : Young diagrams
• young_diagram.card : the number of cells in a Young diagram (its cardinality)
• young_diagram.distrib_lattice : a distributive lattice instance for Young diagrams ordered by containment, with (⊥ : young_diagram) the empty diagram.
• young_diagram.row and young_diagram.row_len: rows of a Young diagram and their lengths
• young_diagram.col and young_diagram.col_len: 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 young_diagram.up_left_mem.

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  :

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]
@[simp, norm_cast]
theorem young_diagram.coe_bot  :
@[simp]
theorem young_diagram.not_mem_bot (x : × ) :
@[protected, instance]
Equations
@[protected, instance]
Equations
• young_diagram.distrib_lattice = young_diagram.distrib_lattice._proof_1 young_diagram.distrib_lattice._proof_2 young_diagram.distrib_lattice._proof_3
@[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]
theorem young_diagram.transpose_eq_iff {μ ν : young_diagram} :
μ = ν
@[protected]
theorem young_diagram.le_of_transpose_le {μ ν : young_diagram} (h_le : μ.transpose ν) :
@[simp]
@[protected]
theorem young_diagram.transpose_mono {μ ν : young_diagram} (h_le : μ ν) :
@[simp]
@[simp]

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

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

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

1. young_diagram.row_lens_sorted : It is weakly decreasing (list.sorted (≥)).
2. young_diagram.row_lens_pos : It is strictly positive.

List of row lengths of a Young diagram

Equations
@[simp]
theorem young_diagram.nth_le_row_lens {μ : young_diagram} {i : } {hi : i < μ.row_lens.length} :
μ.row_lens.nth_le i hi = μ.row_len i
theorem young_diagram.pos_of_mem_row_lens (μ : young_diagram) (x : ) (hx : x μ.row_lens) :
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: young_diagram.equiv_list_row_lens : young_diagram ≃ {w : list ℕ // w.sorted (≥) ∧ ∀ x ∈ w, 0 < x}

The two directions are young_diagram.row_lens (defined above) and young_diagram.of_row_lens.

@[protected]

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

Equations
@[protected]
theorem young_diagram.mem_cells_of_row_lens {w : list } {c : × } :
(h : c.fst < w.length), c.snd < w.nth_le c.fst h

Young diagram from a sorted list

Equations
theorem young_diagram.mem_of_row_lens {w : list } {hw : w} {c : × } :
(h : c.fst < w.length), c.snd < w.nth_le c.fst h
theorem young_diagram.row_lens_length_of_row_lens {w : list } {hw : w} (hpos : (x : ), x w 0 < x) :

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

theorem young_diagram.row_len_of_row_lens {w : list } {hw : w} (i : ) (hi : i < w.length) :
.row_len i = w.nth_le i hi

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

The left_inv direction of the equivalence

theorem young_diagram.row_lens_of_row_lens_eq_self {w : list } {hw : w} (hpos : (x : ), x w 0 < x) :
= w

The right_inv direction of the equivalence

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

Equations
@[simp]
@[simp]
theorem young_diagram.equiv_list_row_lens_symm_apply (ww : {w // (x : ), x w 0 < x}) :