Partition ↔ YoungDiagram equivalence

This file provides the equivalence Nat.Partition n ≃ {μ : YoungDiagram | μ.card = n}, which is the missing bridge between Mathlib's Nat.Partition type and the YoungDiagram type used in the coefficient-level commutation relation.

Main results

• partitionEquiv: Nat.Partition n ≃ {μ : YoungDiagram // μ.card = n}
• card_ofRowLens_eq_sum: the cardinality of ofRowLens w equals w.sum
• rowLens_sum_eq_card: μ.rowLens.sum = μ.card
• sort_coe_sortedGE_eq_reverse: sorting a decreasing list by ≤ gives its reverse

Auxiliary lemmas

theorem YoungEigenvalues.sort_coe_sortedGE_eq_reverse (l : List ℕ) (hl : l.SortedGE) : ((↑l).sort fun (x1 x2 : ℕ) => x1 ≤ x2) = l.reverse

Sorting a SortedGE list by ≤ gives its reverse.

card of ofRowLens

theorem YoungEigenvalues.card_cellsOfRowLens (w : List ℕ) : (YoungDiagram.cellsOfRowLens w).card = w.sum

theorem YoungEigenvalues.card_ofRowLens_eq_sum (w : List ℕ) (hw : w.SortedGE) : (YoungDiagram.ofRowLens w hw).card = w.sum

theorem YoungEigenvalues.rowLens_sum_eq_card (μ : YoungDiagram) : μ.rowLens.sum = μ.card

Partition ≃ YoungDiagram equivalence

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

Convert a Nat.Partition n to a YoungDiagram by sorting its parts in decreasing order and using them as row lengths.

theorem YoungEigenvalues.card_partToYD {n : ℕ} (p : n.Partition) : (partToYD p).card = n

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

Convert a YoungDiagram with n cells to a Nat.Partition n.

theorem YoungEigenvalues.ydToPart_partToYD {n : ℕ} (p : n.Partition) : ydToPart (partToYD p) ⋯ = p

ydToPart is a left inverse of partToYD.

theorem YoungEigenvalues.partToYD_injective {n : ℕ} : Function.Injective partToYD

partToYD is injective.

theorem YoungEigenvalues.partToYD_ydToPart {n : ℕ} (μ : YoungDiagram) (hμ : μ.card = n) : partToYD (ydToPart μ hμ) = μ

partToYD composed with ydToPart is the identity.

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

The equivalence Nat.Partition n ≃ {μ : YoungDiagram // μ.card = n}.