Partitions and Young diagrams

This file relates partitions of n and Young diagrams with n cells by a pair of direct constructions: TauCeti.diagramOf builds the Young diagram whose rows are the decreasingly sorted parts of a partition, and TauCeti.toPartition reads the row lengths of a sized diagram back as a partition. The two constructions are inverse to each other, which packages as the equivalence TauCeti.partitionEquivYoungDiagram.

References

• Mathlib PR #39722 (Kevin Gomez) — the open Mathlib PR linking Nat.Partition to YoungDiagram, whose direct ofPartition/toPartition design this file adopts, in place of composing equivalences.

def TauCeti.diagramOf {n : ℕ} (μ : n.Partition) : YoungDiagram

The Young diagram of a partition: its rows are the decreasingly sorted parts.

Equations

• TauCeti.diagramOf μ = YoungDiagram.ofRowLens (μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2) ⋯

@[simp]

theorem TauCeti.rowLens_diagramOf {n : ℕ} (μ : n.Partition) : (diagramOf μ).rowLens = μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2

The row lengths of a partition's Young diagram are its decreasingly sorted parts.

@[simp]

theorem TauCeti.card_diagramOf {n : ℕ} (μ : n.Partition) : (diagramOf μ).card = n

The Young diagram of a partition has the size of the partition.

@[simp]

theorem TauCeti.rowLen_diagramOf {n : ℕ} (ν : n.Partition) (i : ℕ) : (diagramOf ν).rowLen i = (ν.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2).getD i 0

The row lengths of the Young diagram of a partition are its decreasingly sorted parts, padded by zeros.

theorem TauCeti.rowLen_diagramOf_ones_le_one (n i : ℕ) : (diagramOf (Nat.Partition.ones n)).rowLen i ≤ 1

The Young diagram of the partition (1ⁿ) is a single column: every part is 1, so every row has at most one cell.

theorem TauCeti.colLen_diagramOf_indiscrete_le_one (n : ℕ) : (diagramOf (Nat.Partition.indiscrete n)).colLen 0 ≤ 1

The Young diagram of the partition (n) has at most one row: for n > 0 its only part is n, so there is nothing below the first row, and for n = 0 the diagram is empty.

theorem TauCeti.rowLen_diagramOf_singletonSecondRow_one (n : ℕ) : (diagramOf (Nat.Partition.singletonSecondRow n)).rowLen 1 = 1

The second row of the Young diagram of the partition (n+1, 1) is a single cell.

theorem TauCeti.rowLen_diagramOf_singletonSecondRow_two (n : ℕ) : (diagramOf (Nat.Partition.singletonSecondRow n)).rowLen 2 = 0

The Young diagram of the partition (n+1, 1) has no third row.

@[simp]

theorem TauCeti.colLen_zero_diagramOf {n : ℕ} (ν : n.Partition) : (diagramOf ν).colLen 0 = ν.parts.card

The Young diagram of a partition has one row per part: its rows are the parts, so the length of its first column counts them.

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

The partition of the cells of a Young diagram: its parts are the row lengths.

Equations

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

@[simp]

theorem TauCeti.toPartition_parts {n : ℕ} (μ : YoungDiagram) (h : μ.card = n) : (toPartition μ h).parts = ↑μ.rowLens

The parts of the partition of a sized Young diagram are its row lengths.

@[simp]

theorem TauCeti.toPartition_diagramOf {n : ℕ} (μ : n.Partition) : toPartition (diagramOf μ) ⋯ = μ

Reading back the row lengths of the Young diagram of a partition recovers the partition.

@[simp]

theorem TauCeti.diagramOf_toPartition {n : ℕ} (μ : YoungDiagram) (h : μ.card = n) : diagramOf (toPartition μ h) = μ

The Young diagram whose rows are the row lengths of a sized Young diagram is that diagram.

def TauCeti.partitionEquivYoungDiagram (n : ℕ) : n.Partition ≃ { μ : YoungDiagram // μ.card = n }

Partitions of n are equivalent to Young diagrams with n cells.

Equations

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

@[simp]

theorem TauCeti.partitionEquivYoungDiagram_apply (n : ℕ) (μ : n.Partition) : (partitionEquivYoungDiagram n) μ = ⟨diagramOf μ, ⋯⟩

The Young diagram associated to a partition by the equivalence is TauCeti.diagramOf.

@[simp]

theorem TauCeti.partitionEquivYoungDiagram_symm_apply (n : ℕ) (μ : { μ : YoungDiagram // μ.card = n }) : (partitionEquivYoungDiagram n).symm μ = toPartition ↑μ ⋯

The partition associated to a sized Young diagram by the equivalence is TauCeti.toPartition.

theorem TauCeti.diagramOf_injective {n : ℕ} : Function.Injective diagramOf

The Young diagram construction is injective on partitions of a fixed size.

def TauCeti.shapePartition (μ : YoungDiagram) : μ.card.Partition

The shape partition of a Young diagram: the partition of μ.card whose parts are the row lengths.

Equations

• TauCeti.shapePartition μ = TauCeti.toPartition μ ⋯

@[simp]

theorem TauCeti.toPartition_eq_shapePartition (μ : YoungDiagram) : toPartition μ ⋯ = shapePartition μ

A partition built from a Young diagram along the trivial equality of sizes is its shape partition.

@[simp]

theorem TauCeti.diagramOf_shapePartition (μ : YoungDiagram) : diagramOf (shapePartition μ) = μ

The Young diagram of the shape partition of a Young diagram is that diagram.

@[simp]

theorem TauCeti.shapePartition_parts (μ : YoungDiagram) : (shapePartition μ).parts = ↑μ.rowLens

The parts of the shape partition are the row lengths of the diagram.

theorem TauCeti.shapePartition_parts_sort (μ : YoungDiagram) : ((shapePartition μ).parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2) = μ.rowLens

Sorting the parts of the shape partition into decreasing order returns the row lengths, which are already decreasing. This is not a simp lemma: simp reaches the same normal form through shapePartition_parts and TauCeti.YoungDiagram.sort_coe_rowLens.