Young diagrams from a bounded family of row lengths

Mathlib builds a Young diagram from a weakly decreasing List ℕ of row lengths (YoungDiagram.ofRowLens) and reads that list back off a diagram (YoungDiagram.rowLens); the two are inverse only after the positive entries are singled out, since rowLens never records a row of length 0.

Indexing the row lengths by Fin n rather than by a list removes that mismatch: a weakly decreasing f : Fin n → ℕ is allowed to end in zeros, and YoungDiagram.ofRowLensFin turns any such family into the diagram whose i-th row has length f i for i < n and which has no row beyond. Reading the first n row lengths back off is then an honest inverse on the diagrams with at most n rows — the form consumed when partitions with a bounded number of rows are matched against weight data for GL n.

Main definitions

• YoungDiagram.ofRowLensFin: the Young diagram with prescribed weakly decreasing row lengths f : Fin n → ℕ and no further rows.

Main results

• YoungDiagram.rowLen_ofRowLensFin and YoungDiagram.rowLen_ofRowLensFin_eq_zero_of_le: the row lengths of ofRowLensFin f hf are f on Fin n and 0 beyond it.
• YoungDiagram.colLen_zero_ofRowLensFin_le and YoungDiagram.ofRowLensFin_rowLen: ofRowLensFin lands in the diagrams with at most n rows, and is there inverse to reading off the first n row lengths.
• YoungDiagram.card_ofRowLensFin: its number of cells is ∑ i, f i.

def YoungDiagram.ofRowLensFin {n : ℕ} (f : Fin n → ℕ) (hf : Antitone f) : YoungDiagram

The Young diagram whose first n rows have the prescribed weakly decreasing lengths f : Fin n → ℕ, and which has no row beyond. Unlike YoungDiagram.ofRowLens, the family f may take the value 0; such an entry simply contributes an empty row.

Equations

• YoungDiagram.ofRowLensFin f hf = YoungDiagram.ofRowLens (List.ofFn f) ⋯

@[simp]

theorem YoungDiagram.rowLen_ofRowLensFin {n : ℕ} (f : Fin n → ℕ) (hf : Antitone f) (i : Fin n) : (ofRowLensFin f hf).rowLen ↑i = f i

The rows of ofRowLensFin f hf indexed by Fin n have the prescribed lengths.

@[simp]

theorem YoungDiagram.rowLen_ofRowLensFin_eq_zero_of_le {n : ℕ} (f : Fin n → ℕ) (hf : Antitone f) {i : ℕ} (hi : n ≤ i) : (ofRowLensFin f hf).rowLen i = 0

The rows of ofRowLensFin f hf past the n prescribed ones are empty.

theorem YoungDiagram.colLen_zero_ofRowLensFin_le {n : ℕ} (f : Fin n → ℕ) (hf : Antitone f) : (ofRowLensFin f hf).colLen 0 ≤ n

ofRowLensFin f hf has at most n rows.

theorem YoungDiagram.ofRowLensFin_rowLen {n : ℕ} (μ : YoungDiagram) (hμ : μ.colLen 0 ≤ n) : ofRowLensFin (fun (i : Fin n) => μ.rowLen ↑i) ⋯ = μ

Reading the first n row lengths off a Young diagram with at most n rows recovers it.

@[simp]

theorem YoungDiagram.card_ofRowLensFin {n : ℕ} (f : Fin n → ℕ) (hf : Antitone f) : (ofRowLensFin f hf).card = ∑ i : Fin n, f i

ofRowLensFin f hf has ∑ i, f i cells.