Young diagrams of a fixed size

Shape n is the type of Young diagrams with exactly n cells. It carries decidable equality and a Fintype instance, obtained from the correspondence with Nat.Partition n that reads off the row lengths. This is the tree's standard idiom for "sum over the partitions of n".

Counting cells by rows

theorem RS.rowLens_injective : Function.Injective YoungDiagram.rowLens

Young diagrams are determined by their lists of row lengths.

Shapes

def RS.Shape (n : ℕ) : Type

The Young diagrams with n cells.

Equations

• RS.Shape n = { μ : YoungDiagram // μ.card = n }

@[simp]

theorem RS.Shape.card_val {n : ℕ} (μ : Shape n) : (↑μ).card = n

A shape's diagram has exactly n cells.

theorem RS.Shape.ext {n : ℕ} {μ ν : Shape n} (h : ↑μ = ↑ν) : μ = ν

Shapes are equal as soon as their diagrams are.

theorem RS.Shape.ext_iff {n : ℕ} {μ ν : Shape n} : μ = ν ↔ ↑μ = ↑ν

@[instance_reducible]

instance RS.instDecidableEqShape (n : ℕ) : DecidableEq (Shape n)

Equality of shapes is decidable, cell set by cell set.

Equations

• RS.instDecidableEqShape n μ ν = decidable_of_iff ((↑μ).cells = (↑ν).cells) ⋯

The correspondence with partitions

noncomputable def RS.shapeEquivPartition (n : ℕ) : Shape n ≃ n.Partition

Young diagrams of size n correspond to partitions of n, by reading off the row lengths.

Equations

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

@[simp]

theorem RS.shapeEquivPartition_apply_parts {n : ℕ} (μ : Shape n) : ((shapeEquivPartition n) μ).parts = ↑(↑μ).rowLens

The multiset of parts of the partition attached to a shape is the multiset of its row lengths.

@[instance_reducible]

noncomputable instance RS.instFintypeShape (n : ℕ) : Fintype (Shape n)

There are finitely many Young diagrams with n cells: as many as there are partitions of n.

Equations

• RS.instFintypeShape n = Fintype.ofEquiv n.Partition (RS.shapeEquivPartition n).symm