mathlib3 documentation

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.

Tags #

Young diagram

References #

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

theorem young_diagram.ext_iff (x y : young_diagram) :

x = y ↔ x.cells = y.cells

theorem young_diagram.ext (x y : young_diagram) (h : x.cells = y.cells) :

x = y

@[ext]

structure young_diagram :

cells : finset (ℕ × ℕ)
is_lower_set : is_lower_set ↑(self.cells)

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]

def young_diagram.prod.set_like :

set_like young_diagram (ℕ × ℕ)

Equations

young_diagram.prod.set_like = {coe := ↑young_diagram.cells, coe_injective' := young_diagram.prod.set_like._proof_1}

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

def young_diagram.decidable_mem (μ : young_diagram) :

decidable_pred (λ (_x : ℕ × ℕ), _x ∈ μ)

Equations

μ.decidable_mem = show decidable_pred (λ (_x : ℕ × ℕ), _x ∈ μ.cells), from λ (a : ℕ × ℕ), finset.decidable_mem a μ.cells

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]

theorem young_diagram.cells_subset_iff {μ ν : young_diagram} :

μ.cells ⊆ ν.cells ↔ μ ≤ ν

@[simp]

theorem young_diagram.cells_ssubset_iff {μ ν : young_diagram} :

μ.cells ⊂ ν.cells ↔ μ < ν

@[protected, instance]

def young_diagram.has_sup :

has_sup young_diagram

Equations

young_diagram.has_sup = {sup := λ (μ ν : young_diagram), {cells := μ.cells ∪ ν.cells, is_lower_set := _}}

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

def young_diagram.has_inf :

has_inf young_diagram

Equations

young_diagram.has_inf = {inf := λ (μ ν : young_diagram), {cells := μ.cells ∩ ν.cells, is_lower_set := _}}

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

def young_diagram.order_bot :

order_bot young_diagram

The empty Young diagram is (⊥ : young_diagram).

Equations

young_diagram.order_bot = {bot := {cells := ∅, is_lower_set := young_diagram.order_bot._proof_1}, bot_le := young_diagram.order_bot._proof_2}

@[simp]

theorem young_diagram.cells_bot :

⊥.cells = ∅

@[simp, norm_cast]

theorem young_diagram.coe_bot :

@[simp]

theorem young_diagram.not_mem_bot (x : ℕ × ℕ) :

@[protected, instance]

def young_diagram.inhabited :

inhabited young_diagram

Equations

young_diagram.inhabited = {default := ⊥}

@[protected, instance]

def young_diagram.distrib_lattice :

distrib_lattice young_diagram

Equations

young_diagram.distrib_lattice = function.injective.distrib_lattice young_diagram.cells young_diagram.distrib_lattice._proof_1 young_diagram.distrib_lattice._proof_2 young_diagram.distrib_lattice._proof_3

@[protected, reducible]

def young_diagram.card (μ : young_diagram) :

Cardinality of a Young diagram

Equations

μ.card = μ.cells.card

def young_diagram.transpose (μ : young_diagram) :

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

Equations

μ.transpose = {cells := ⇑((equiv.prod_comm ℕ ℕ).finset_congr) μ.cells, is_lower_set := _}

@[simp]

theorem young_diagram.mem_transpose {μ : young_diagram} {c : ℕ × ℕ} :

c ∈ μ.transpose ↔ c.swap ∈ μ

@[simp]

theorem young_diagram.transpose_transpose (μ : young_diagram) :

μ.transpose.transpose = μ

theorem young_diagram.transpose_eq_iff_eq_transpose {μ ν : young_diagram} :

μ.transpose = ν ↔ μ = ν.transpose

@[simp]

theorem young_diagram.transpose_eq_iff {μ ν : young_diagram} :

μ.transpose = ν.transpose ↔ μ = ν

@[protected]

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

μ ≤ ν.transpose

@[simp]

theorem young_diagram.transpose_le_iff {μ ν : young_diagram} :

μ.transpose ≤ ν.transpose ↔ μ ≤ ν

@[protected]

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

μ.transpose ≤ ν.transpose

@[simp]

theorem young_diagram.transpose_order_iso_apply (μ : young_diagram) :

⇑young_diagram.transpose_order_iso μ = μ.transpose

@[simp]

theorem young_diagram.transpose_order_iso_symm_apply (μ : young_diagram) :

⇑(rel_iso.symm young_diagram.transpose_order_iso) μ = μ.transpose

def young_diagram.transpose_order_iso :

young_diagram ≃o young_diagram

Transposing Young diagrams is an order_iso.

Equations

young_diagram.transpose_order_iso = {to_equiv := {to_fun := young_diagram.transpose, inv_fun := young_diagram.transpose, left_inv := young_diagram.transpose_order_iso._proof_1, right_inv := young_diagram.transpose_order_iso._proof_2}, map_rel_iff' := young_diagram.transpose_order_iso._proof_3}

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

def young_diagram.row (μ : young_diagram) (i : ℕ) :

finset (ℕ × ℕ)

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

Equations

μ.row i = finset.filter (λ (c : ℕ × ℕ), c.fst = i) μ.cells

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

def young_diagram.row_len (μ : young_diagram) (i : ℕ) :

Length of a row of a Young diagram

Equations

μ.row_len i = nat.find _

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.

def young_diagram.col (μ : young_diagram) (j : ℕ) :

finset (ℕ × ℕ)

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

Equations

μ.col j = finset.filter (λ (c : ℕ × ℕ), c.snd = j) μ.cells

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

def young_diagram.col_len (μ : young_diagram) (j : ℕ) :

Length of a column of a Young diagram

Equations

μ.col_len j = nat.find _

@[simp]

theorem young_diagram.col_len_transpose (μ : young_diagram) (j : ℕ) :

μ.transpose.col_len j = μ.row_len j

@[simp]

theorem young_diagram.row_len_transpose (μ : young_diagram) (i : ℕ) :

μ.transpose.row_len i = μ.col_len i

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

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

def young_diagram.row_lens (μ : young_diagram) :

List of row lengths of a Young diagram

Equations

μ.row_lens = list.map μ.row_len (list.range (μ.col_len 0))

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

@[simp]

theorem young_diagram.length_row_lens {μ : young_diagram} :

μ.row_lens.length = μ.col_len 0

theorem young_diagram.row_lens_sorted (μ : young_diagram) :

list.sorted ge μ.row_lens

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]

def young_diagram.cells_of_row_lens :

list ℕ → finset (ℕ × ℕ)

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 : ℕ × ℕ} :

c ∈ young_diagram.cells_of_row_lens w ↔ ∃ (h : c.fst < w.length), c.snd < w.nth_le c.fst h

def young_diagram.of_row_lens (w : list ℕ) (hw : list.sorted ge w) :

Young diagram from a sorted list

Equations

young_diagram.of_row_lens w hw = {cells := young_diagram.cells_of_row_lens w, is_lower_set := _}

theorem young_diagram.mem_of_row_lens {w : list ℕ} {hw : list.sorted ge w} {c : ℕ × ℕ} :

c ∈ young_diagram.of_row_lens w hw ↔ ∃ (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 : list.sorted ge w} (hpos : ∀ (x : ℕ), x ∈ w → 0 < x) :

(young_diagram.of_row_lens w hw).row_lens.length = w.length

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 : list.sorted ge w} (i : ℕ) (hi : i < w.length) :

(young_diagram.of_row_lens w hw).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

theorem young_diagram.of_row_lens_to_row_lens_eq_self {μ : young_diagram} :

young_diagram.of_row_lens μ.row_lens _ = μ

The left_inv direction of the equivalence

theorem young_diagram.row_lens_of_row_lens_eq_self {w : list ℕ} {hw : list.sorted ge w} (hpos : ∀ (x : ℕ), x ∈ w → 0 < x) :

(young_diagram.of_row_lens w hw).row_lens = w

The right_inv direction of the equivalence

def young_diagram.equiv_list_row_lens :

young_diagram ≃ {w // list.sorted ge w ∧ ∀ (x : ℕ), 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

young_diagram.equiv_list_row_lens = {to_fun := λ (μ : young_diagram), ⟨μ.row_lens, _⟩, inv_fun := λ (ww : {w // list.sorted ge w ∧ ∀ (x : ℕ), x ∈ w → 0 < x}), young_diagram.of_row_lens ww.val _, left_inv := young_diagram.equiv_list_row_lens._proof_3, right_inv := young_diagram.equiv_list_row_lens._proof_4}

@[simp]

theorem young_diagram.equiv_list_row_lens_apply_coe (μ : young_diagram) :

↑(⇑young_diagram.equiv_list_row_lens μ) = μ.row_lens

@[simp]

theorem young_diagram.equiv_list_row_lens_symm_apply (ww : {w // list.sorted ge w ∧ ∀ (x : ℕ), x ∈ w → 0 < x}) :

⇑(young_diagram.equiv_list_row_lens.symm) ww = young_diagram.of_row_lens ww.val _