# mathlibdocumentation

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 #

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

## 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  :
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
@[protected, instance]
Equations
@[simp]
theorem young_diagram.mem_cells {μ : young_diagram} (c : × ) :
c μ.cells c μ
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