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

source
theorem young_diagram.ext_iff (x y : young_diagram) :
x = y ↔ x.cells = y.cells
source
theorem young_diagram.ext (x y : young_diagram) (h : x.cells = y.cells) :
x = y
source
@[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
source
@[protected, instance]
def young_diagram.prod.set_like  :
set_like young_diagram (ℕ × ℕ)
Equations
source
@[simp]
theorem young_diagram.mem_cells {μ : young_diagram} (c : ℕ × ℕ) :
c ∈ μ.cells ↔ c ∈ μ
source
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).

source
@[simp]
theorem young_diagram.cells_subset_iff {μ ν : young_diagram} :
μ.cells ⊆ ν.cells ↔ μ ≤ ν
source
@[simp]
theorem young_diagram.cells_ssubset_iff {μ ν : young_diagram} :
μ.cells ⊂ ν.cells ↔ μ < ν
source
@[protected, instance]
def young_diagram.has_sup  :
has_sup young_diagram
Equations
source
@[simp]
theorem young_diagram.cells_sup (μ ν : young_diagram) :
(μ ⊔ ν).cells = μ.cells ∪ ν.cells
source
@[simp, norm_cast]
theorem young_diagram.coe_sup (μ ν : young_diagram) :
↑(μ ⊔ ν) = ↑μ ∪ ↑ν
source
@[simp]
theorem young_diagram.mem_sup {μ ν : young_diagram} {x : ℕ × ℕ} :
x ∈ μ ⊔ ν ↔ x ∈ μ ∨ x ∈ ν
source
@[protected, instance]
def young_diagram.has_inf  :
has_inf young_diagram
Equations
source
@[simp]
theorem young_diagram.cells_inf (μ ν : young_diagram) :
(μ ⊓ ν).cells = μ.cells ∩ ν.cells
source
@[simp, norm_cast]
theorem young_diagram.coe_inf (μ ν : young_diagram) :
↑(μ ⊓ ν) = ↑μ ∩ ↑ν
source
@[simp]
theorem young_diagram.mem_inf {μ ν : young_diagram} {x : ℕ × ℕ} :
x ∈ μ ⊓ ν ↔ x ∈ μ ∧ x ∈ ν
source
@[protected, instance]
def young_diagram.order_bot  :
order_bot young_diagram

The empty Young diagram is (⊥ : young_diagram).

Equations
source
@[simp]
theorem young_diagram.cells_bot  :
⊥.cells = ∅
source
@[simp, norm_cast]
theorem young_diagram.coe_bot  :
↑⊥ = ∅
source
@[simp]
theorem young_diagram.not_mem_bot (x : ℕ × ℕ) :
x ∉ ⊥
source
@[protected, instance]
def young_diagram.inhabited  :
inhabited young_diagram
Equations
source
@[protected, instance]
def young_diagram.distrib_lattice  :
distrib_lattice young_diagram
Equations
source
@[protected, reducible]
def young_diagram.card (μ : young_diagram) :
ℕ

Cardinality of a Young diagram

Equations