Young diagram of a partition

This file defines the equivalence between Young diagrams μ with cardinality n and partitions of n, where each row of the diagram becomes a part of the partition. The two directions are YoungDiagram.toPartition and YoungDiagram.ofPartition.

Using this equivalence, the conjugate of a partition is also defined. Given the Young diagram μ representing a partition λ, its conjugate λ' is the partition obtained by flipping μ about the main diagonal, i.e. the columns of μ are the parts of λ'. This is implemented here directly via YoungDiagram.transpose.

def YoungDiagram.toPartition {n : ℕ} (μ : YoungDiagram) (h : μ.card = n) : n.Partition

Convert a Young diagram to a partition.

Equations

• μ.toPartition h = { parts := ↑μ.rowLens, parts_pos := ⋯, parts_sum := ⋯ }

def YoungDiagram.ofPartition {n : ℕ} (p : n.Partition) : YoungDiagram

Convert a partition to a Young diagram.

Equations

• YoungDiagram.ofPartition p = YoungDiagram.ofRowLens (p.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2) ⋯

@[simp]

theorem YoungDiagram.rowLens_ofPartition_eq_sort_parts {n : ℕ} (p : n.Partition) : (ofPartition p).rowLens = p.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2

@[simp]

theorem YoungDiagram.card_ofPartition {n : ℕ} (p : n.Partition) : (ofPartition p).card = n

@[simp]

theorem YoungDiagram.ofPartition_toPartition {n : ℕ} {μ : YoungDiagram} (h : μ.card = n) : ofPartition (μ.toPartition h) = μ

@[simp]

theorem YoungDiagram.toPartition_ofPartition {n : ℕ} {p : n.Partition} : (ofPartition p).toPartition ⋯ = p

def YoungDiagram.equivPartition {n : ℕ} : { μ : YoungDiagram // μ.card = n } ≃ n.Partition

Equivalence between Young diagrams of cardinality n and partitions of n.

Equations

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

def Nat.Partition.conjugate {n : ℕ} (p : n.Partition) : n.Partition

Conjugate a partition (equivalent to transposing its Young diagram).

Equations

• p.conjugate = (YoungDiagram.ofPartition p).transpose.toPartition ⋯

@[simp]

theorem Nat.Partition.conjugate_conjugate {n : ℕ} (p : n.Partition) : p.conjugate.conjugate = p

Conjugation is an involution.