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.

Tags

Young diagram

References

theorem YoungDiagram.ext_iff (x : YoungDiagram) (y : YoungDiagram) : x = y ↔ x.cells = y.cells

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

structure YoungDiagram : 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.

• 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 ℕ × ℕ.

instance YoungDiagram.instSetLikeYoungDiagramProdNat : SetLike YoungDiagram (ℕ × ℕ)

Equations

• YoungDiagram.instSetLikeYoungDiagramProdNat = { coe := fun (y : YoungDiagram) => ↑y.cells, coe_injective' := YoungDiagram.instSetLikeYoungDiagramProdNat.proof_1 }

@[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

• YoungDiagram.decidableMem μ = inferInstanceAs (DecidablePred fun (x : ℕ × ℕ) => x ∈ μ.cells)

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 ↔ μ < ν

instance YoungDiagram.instSupYoungDiagram : Sup YoungDiagram

Equations

• YoungDiagram.instSupYoungDiagram = { sup := fun (μ ν : YoungDiagram) => { cells := μ.cells ∪ ν.cells, isLowerSet := ⋯ } }

@[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 ∈ ν

instance YoungDiagram.instInfYoungDiagram : Inf YoungDiagram

Equations

• YoungDiagram.instInfYoungDiagram = { inf := fun (μ ν : YoungDiagram) => { cells := μ.cells ∩ ν.cells, isLowerSet := ⋯ } }

@[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 ∈ ν

instance YoungDiagram.instOrderBotYoungDiagramToLEToPreorderInstPartialOrderProdNatInstSetLikeYoungDiagramProdNat : OrderBot YoungDiagram

The empty Young diagram is (⊥ : young_diagram).

Equations

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

@[simp]

theorem YoungDiagram.cells_bot : ⊥.cells = ∅

theorem YoungDiagram.coe_bot : ↑⊥.cells = ∅

@[simp]

theorem YoungDiagram.not_mem_bot (x : ℕ × ℕ) : x ∉ ⊥

instance YoungDiagram.instInhabitedYoungDiagram : Inhabited YoungDiagram

Equations

• YoungDiagram.instInhabitedYoungDiagram = { default := ⊥ }

instance YoungDiagram.instDistribLatticeYoungDiagram : DistribLattice YoungDiagram

Equations

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

@[reducible]

def YoungDiagram.card (μ : YoungDiagram) : ℕ

Cardinality of a Young diagram

Equations

• YoungDiagram.card μ = μ.cells.card

def YoungDiagram.transpose (μ : YoungDiagram) : YoungDiagram

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

Equations

• YoungDiagram.transpose μ = { cells := (Equiv.finsetCongr (Equiv.prodComm ℕ ℕ)) μ.cells, isLowerSet := ⋯ }

@[simp]

theorem YoungDiagram.mem_transpose {μ : YoungDiagram} {c : ℕ × ℕ} : c ∈ YoungDiagram.transpose μ ↔ Prod.swap c ∈ μ

@[simp]

theorem YoungDiagram.transpose_transpose (μ : YoungDiagram) : YoungDiagram.transpose (YoungDiagram.transpose μ) = μ

theorem YoungDiagram.transpose_eq_iff_eq_transpose {μ : YoungDiagram} {ν : YoungDiagram} : YoungDiagram.transpose μ = ν ↔ μ = YoungDiagram.transpose ν

@[simp]

theorem YoungDiagram.transpose_eq_iff {μ : YoungDiagram} {ν : YoungDiagram} : YoungDiagram.transpose μ = YoungDiagram.transpose ν ↔ μ = ν

theorem YoungDiagram.le_of_transpose_le {μ : YoungDiagram} {ν : YoungDiagram} (h_le : YoungDiagram.transpose μ ≤ ν) : μ ≤ YoungDiagram.transpose ν

@[simp]

theorem YoungDiagram.transpose_le_iff {μ : YoungDiagram} {ν : YoungDiagram} : YoungDiagram.transpose μ ≤ YoungDiagram.transpose ν ↔ μ ≤ ν

theorem YoungDiagram.transpose_mono {μ : YoungDiagram} {ν : YoungDiagram} (h_le : μ ≤ ν) : YoungDiagram.transpose μ ≤ YoungDiagram.transpose ν

@[simp]

theorem YoungDiagram.transposeOrderIso_symm_apply (μ : YoungDiagram) : (RelIso.symm YoungDiagram.transposeOrderIso) μ = YoungDiagram.transpose μ

@[simp]

theorem YoungDiagram.transposeOrderIso_apply (μ : YoungDiagram) : YoungDiagram.transposeOrderIso μ = YoungDiagram.transpose μ

def YoungDiagram.transposeOrderIso : YoungDiagram ≃o YoungDiagram

Transposing Young diagrams is an OrderIso.

Equations

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

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) ∉ μ.

def YoungDiagram.row (μ : YoungDiagram) (i : ℕ) : Finset (ℕ × ℕ)

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

Equations

• YoungDiagram.row μ i = Finset.filter (fun (c : ℕ × ℕ) => c.1 = i) μ.cells

theorem YoungDiagram.mem_row_iff {μ : YoungDiagram} {i : ℕ} {c : ℕ × ℕ} : c ∈ YoungDiagram.row μ i ↔ c ∈ μ ∧ c.1 = i

theorem YoungDiagram.mk_mem_row_iff {μ : YoungDiagram} {i : ℕ} {j : ℕ} : (i, j) ∈ YoungDiagram.row μ i ↔ (i, j) ∈ μ

theorem YoungDiagram.exists_not_mem_row (μ : YoungDiagram) (i : ℕ) : ∃ (j : ℕ), (i, j) ∉ μ

def YoungDiagram.rowLen (μ : YoungDiagram) (i : ℕ) : ℕ

Length of a row of a Young diagram

Equations

• YoungDiagram.rowLen μ i = Nat.find ⋯

theorem YoungDiagram.mem_iff_lt_rowLen {μ : YoungDiagram} {i : ℕ} {j : ℕ} : (i, j) ∈ μ ↔ j < YoungDiagram.rowLen μ i

theorem YoungDiagram.row_eq_prod {μ : YoungDiagram} {i : ℕ} : YoungDiagram.row μ i = {i} ×ˢ Finset.range (YoungDiagram.rowLen μ i)

theorem YoungDiagram.rowLen_eq_card (μ : YoungDiagram) {i : ℕ} : YoungDiagram.rowLen μ i = (YoungDiagram.row μ i).card

theorem YoungDiagram.rowLen_anti (μ : YoungDiagram) (i1 : ℕ) (i2 : ℕ) (hi : i1 ≤ i2) : YoungDiagram.rowLen μ i2 ≤ YoungDiagram.rowLen μ i1

Columns and column lengths of Young diagrams.

This section has an identical API to the rows section.

def YoungDiagram.col (μ : YoungDiagram) (j : ℕ) : Finset (ℕ × ℕ)

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

Equations

• YoungDiagram.col μ j = Finset.filter (fun (c : ℕ × ℕ) => c.2 = j) μ.cells

theorem YoungDiagram.mem_col_iff {μ : YoungDiagram} {j : ℕ} {c : ℕ × ℕ} : c ∈ YoungDiagram.col μ j ↔ c ∈ μ ∧ c.2 = j

theorem YoungDiagram.mk_mem_col_iff {μ : YoungDiagram} {i : ℕ} {j : ℕ} : (i, j) ∈ YoungDiagram.col μ j ↔ (i, j) ∈ μ

theorem YoungDiagram.exists_not_mem_col (μ : YoungDiagram) (j : ℕ) : ∃ (i : ℕ), (i, j) ∉ μ.cells

def YoungDiagram.colLen (μ : YoungDiagram) (j : ℕ) : ℕ

Length of a column of a Young diagram

Equations

• YoungDiagram.colLen μ j = Nat.find ⋯

@[simp]

theorem YoungDiagram.colLen_transpose (μ : YoungDiagram) (j : ℕ) : YoungDiagram.colLen (YoungDiagram.transpose μ) j = YoungDiagram.rowLen μ j

@[simp]

theorem YoungDiagram.rowLen_transpose (μ : YoungDiagram) (i : ℕ) : YoungDiagram.rowLen (YoungDiagram.transpose μ) i = YoungDiagram.colLen μ i

theorem YoungDiagram.mem_iff_lt_colLen {μ : YoungDiagram} {i : ℕ} {j : ℕ} : (i, j) ∈ μ ↔ i < YoungDiagram.colLen μ j

theorem YoungDiagram.col_eq_prod {μ : YoungDiagram} {j : ℕ} : YoungDiagram.col μ j = Finset.range (YoungDiagram.colLen μ j) ×ˢ {j}

theorem YoungDiagram.colLen_eq_card (μ : YoungDiagram) {j : ℕ} : YoungDiagram.colLen μ j = (YoungDiagram.col μ j).card

theorem YoungDiagram.colLen_anti (μ : YoungDiagram) (j1 : ℕ) (j2 : ℕ) (hj : j1 ≤ j2) : YoungDiagram.colLen μ j2 ≤ YoungDiagram.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.

def YoungDiagram.rowLens (μ : YoungDiagram) : List ℕ

List of row lengths of a Young diagram

Equations

• YoungDiagram.rowLens μ = List.map (YoungDiagram.rowLen μ) (List.range (YoungDiagram.colLen μ 0))

@[simp]

theorem YoungDiagram.get_rowLens {μ : YoungDiagram} {i : Fin (List.length (YoungDiagram.rowLens μ))} : List.get (YoungDiagram.rowLens μ) i = YoungDiagram.rowLen μ ↑i

@[simp]

theorem YoungDiagram.length_rowLens {μ : YoungDiagram} : List.length (YoungDiagram.rowLens μ) = YoungDiagram.colLen μ 0

theorem YoungDiagram.rowLens_sorted (μ : YoungDiagram) : List.Sorted (fun (x x_1 : ℕ) => x ≥ x_1) (YoungDiagram.rowLens μ)

theorem YoungDiagram.pos_of_mem_rowLens (μ : YoungDiagram) (x : ℕ) (hx : x ∈ YoungDiagram.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.

def YoungDiagram.cellsOfRowLens : List ℕ → Finset (ℕ × ℕ)

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.
• YoungDiagram.cellsOfRowLens [] = ∅

theorem YoungDiagram.mem_cellsOfRowLens {w : List ℕ} {c : ℕ × ℕ} : c ∈ YoungDiagram.cellsOfRowLens w ↔ ∃ (h : c.1 < List.length w), c.2 < List.get w { val := c.1, isLt := h }

def YoungDiagram.ofRowLens (w : List ℕ) (hw : List.Sorted (fun (x x_1 : ℕ) => x ≥ x_1) w) : YoungDiagram

Young diagram from a sorted list

Equations

• YoungDiagram.ofRowLens w hw = { cells := YoungDiagram.cellsOfRowLens w, isLowerSet := ⋯ }

theorem YoungDiagram.mem_ofRowLens {w : List ℕ} {hw : List.Sorted (fun (x x_1 : ℕ) => x ≥ x_1) w} {c : ℕ × ℕ} : c ∈ YoungDiagram.ofRowLens w hw ↔ ∃ (h : c.1 < List.length w), c.2 < List.get w { val := c.1, isLt := h }

theorem YoungDiagram.rowLens_length_ofRowLens {w : List ℕ} {hw : List.Sorted (fun (x x_1 : ℕ) => x ≥ x_1) w} (hpos : ∀ x ∈ w, 0 < x) : List.length (YoungDiagram.rowLens (YoungDiagram.ofRowLens w hw)) = List.length w

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

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

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

theorem YoungDiagram.ofRowLens_to_rowLens_eq_self {μ : YoungDiagram} : YoungDiagram.ofRowLens (YoungDiagram.rowLens μ) ⋯ = μ

The left_inv direction of the equivalence

theorem YoungDiagram.rowLens_ofRowLens_eq_self {w : List ℕ} {hw : List.Sorted (fun (x x_1 : ℕ) => x ≥ x_1) w} (hpos : ∀ x ∈ w, 0 < x) : YoungDiagram.rowLens (YoungDiagram.ofRowLens w hw) = w

The right_inv direction of the equivalence

@[simp]

theorem YoungDiagram.equivListRowLens_symm_apply (ww : { w : List ℕ // List.Sorted (fun (x x_1 : ℕ) => x ≥ x_1) w ∧ ∀ x ∈ w, 0 < x }) : YoungDiagram.equivListRowLens.symm ww = YoungDiagram.ofRowLens ↑ww ⋯

@[simp]

theorem YoungDiagram.equivListRowLens_apply_coe (μ : YoungDiagram) : ↑(YoungDiagram.equivListRowLens μ) = YoungDiagram.rowLens μ

def YoungDiagram.equivListRowLens : YoungDiagram ≃ { w : List ℕ // List.Sorted (fun (x x_1 : ℕ) => x ≥ x_1) w ∧ ∀ x ∈ w, 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.