Counting the cells of a Young diagram by rows

Mathlib's YoungDiagram.rowLens records the lengths of the rows of a Young diagram. This file counts the cells of a diagram row by row: the first k row lengths sum to the number of cells lying in the first k rows, whether those lengths are summed as ∑ i ∈ Finset.range k, μ.rowLen i or as (μ.rowLens.take k).sum. Since the rows exhaust the cells, the row lengths also determine the diagram (YoungDiagram.rowLen_injective). Cutting the same count column by column, YoungDiagram.card_filter_fst_lt_filter_snd_eq counts the cells of the first k rows lying in a fixed column; summing that count over the columns gives the counting core YoungDiagram.card_filter_le_sum_take_rowLens, which bounds the elements of row less than k in a finite type labelled by a row and injected into the cells, no two of them sharing both a row and a column, by the cells of the first k rows. The same row-by-row reading applies to any property of the cells, not only to counting them all: YoungDiagram.card_filter_cells counts the cells satisfying a predicate one row at a time, and YoungDiagram.prod_cells_eq_prod_range reads a product over the cells the same way.

The partial sums are the shape of every dominance statement about partitions, since dominance compares partial sums of decreasingly sorted parts, and the sorted parts of a partition are the row lengths of its Young diagram.

Reading the rows also describes containment: one diagram is contained in another exactly when each of its rows is shorter (YoungDiagram.le_iff_forall_rowLen_le), from which a diagram has only finitely many sub-diagrams (YoungDiagram.finite_Iic).

The file closes with the two degenerate shapes, at the bottom and at the top of the dominance order. A diagram with at most one column has its cells described one row at a time by YoungDiagram.mem_iff_of_rowLen_le_one and counted by YoungDiagram.card_eq_colLen_of_rowLen_le_one; a diagram with at most one row is described by YoungDiagram.mem_iff_of_colLen_le_one and counted by YoungDiagram.card_eq_rowLen_of_colLen_le_one.

theorem YoungDiagram.rowLen_eq_zero_of_colLen_le {μ : YoungDiagram} {i : ℕ} (hi : μ.colLen 0 ≤ i) : μ.rowLen i = 0

A row past the last one of a Young diagram is empty.

@[simp]

theorem YoungDiagram.rowLen_bot (i : ℕ) : ⊥.rowLen i = 0

The empty Young diagram has no cells, so every row of it is empty.

@[simp]

theorem YoungDiagram.colLen_bot (j : ℕ) : ⊥.colLen j = 0

The empty Young diagram has no cells, so every column of it is empty.

theorem YoungDiagram.rowLen_injective : Function.Injective rowLen

A Young diagram is determined by its row lengths.

theorem YoungDiagram.getD_rowLens (μ : YoungDiagram) (i : ℕ) : μ.rowLens.getD i 0 = μ.rowLen i

Reading the length of a row off YoungDiagram.rowLens, with 0 for the rows past the last one.

theorem YoungDiagram.sort_coe_rowLens (μ : YoungDiagram) : ((↑μ.rowLens).sort fun (x1 x2 : ℕ) => x1 ≥ x2) = μ.rowLens

Sorting the row lengths of a Young diagram, as a multiset, recovers the row lengths: they are already decreasing.

theorem YoungDiagram.sum_range_rowLen_eq_card_filter_fst (μ : YoungDiagram) (k : ℕ) : ∑ i ∈ Finset.range k, μ.rowLen i = {c ∈ μ.cells | c.1 < k}.card

The first k row lengths of a Young diagram count its cells in the first k rows.

theorem YoungDiagram.card_eq_sum_range_rowLen (μ : YoungDiagram) {N : ℕ} (hN : μ.colLen 0 ≤ N) : μ.card = ∑ i ∈ Finset.range N, μ.rowLen i

The cells of a Young diagram, counted over any range of rows that contains all of them. This is YoungDiagram.sum_rowLens_eq_card with the range of summation chosen by hand instead of being the exact number of rows μ.colLen 0.

theorem YoungDiagram.card_filter_cells (μ : YoungDiagram) (p : ℕ × ℕ → Prop) [DecidablePred p] {N : ℕ} (hN : μ.colLen 0 ≤ N) : (Finset.filter p μ.cells).card = ∑ i ∈ Finset.range N, {j ∈ Finset.range (μ.rowLen i) | p (i, j)}.card

The cells of a Young diagram carrying a given property, counted row by row. The range of summation is any range of rows containing all of them, as in YoungDiagram.card_eq_sum_range_rowLen; a row past the last one contributes nothing, being empty.

theorem YoungDiagram.prod_cells_eq_prod_range {M : Type u_1} [CommMonoid M] (μ : YoungDiagram) {N : ℕ} (hN : μ.colLen 0 ≤ N) (f : ℕ × ℕ → M) : ∏ c ∈ μ.cells, f c = ∏ i ∈ Finset.range N, ∏ j ∈ Finset.range (μ.rowLen i), f (i, j)

A product over the cells of a Young diagram, read row by row. The cells are fibred over their row index by Prod.fst, and the fibre of i is the row YoungDiagram.row μ i, which is {i} ×ˢ Finset.range (μ.rowLen i). The range of rows is any range containing all of them, as in YoungDiagram.card_eq_sum_range_rowLen; a row past the last one contributes an empty product.

theorem YoungDiagram.sum_take_rowLens_eq_card_filter_fst (μ : YoungDiagram) (k : ℕ) : (List.take k μ.rowLens).sum = {c ∈ μ.cells | c.1 < k}.card

The first k entries of YoungDiagram.rowLens count the cells in the first k rows. This is YoungDiagram.sum_range_rowLen_eq_card_filter_fst with the truncation taken on the list of row lengths, the form in which partial sums enter the dominance order on partitions.

theorem YoungDiagram.card_filter_fst_lt_filter_snd_eq (lam : YoungDiagram) (k j : ℕ) : {c ∈ {c ∈ lam.cells | c.1 < k} | c.2 = j}.card = min k (lam.colLen j)

The cells of a Young diagram lying in a fixed column and in one of the first k rows are the top min k (colLen j) cells of that column.

theorem YoungDiagram.card_filter_le_sum_take_rowLens {α : Type u_1} [Fintype α] (lam : YoungDiagram) (r : α → ℕ) (f : α → ℕ × ℕ) (hmem : ∀ (a : α), f a ∈ lam.cells) (hinj : Function.Injective f) (hcol : ∀ (a b : α), r a = r b → (f a).2 = (f b).2 → a = b) (k : ℕ) : {a : α | r a < k}.card ≤ (List.take k lam.rowLens).sum

The counting core of the dominance lemma. Let the elements of a finite type α be labelled by a row r a : ℕ and placed in the cells of a Young diagram lam by an injection f, in such a way that the row of an element together with the column of its cell determines the element. Then the elements of row less than k are no more numerous than the cells of lam in its first k rows.

The hypothesis hcol is the condition that elements sharing a row occupy pairwise distinct columns; it is what bounds by k the number of elements landing in any one column.

theorem YoungDiagram.rowLen_le_of_le {μ ν : YoungDiagram} (h : ν ≤ μ) (i : ℕ) : ν.rowLen i ≤ μ.rowLen i

A row of a sub-diagram is no longer than the corresponding row.

theorem YoungDiagram.le_of_forall_rowLen_le {μ ν : YoungDiagram} (h : ∀ (i : ℕ), ν.rowLen i ≤ μ.rowLen i) : ν ≤ μ

A Young diagram is contained in another as soon as each of its rows is shorter.

theorem YoungDiagram.le_iff_forall_rowLen_le {μ ν : YoungDiagram} : ν ≤ μ ↔ ∀ (i : ℕ), ν.rowLen i ≤ μ.rowLen i

Containment of Young diagrams is containment of rows.

theorem YoungDiagram.le_rowLen_of_forall_mem {ν : YoungDiagram} {i k : ℕ} (h : ∀ j < k, (i, j) ∈ ν) : k ≤ ν.rowLen i

A row of a Young diagram is at least as long as any initial segment of cells it contains.

theorem YoungDiagram.finite_Iic (μ : YoungDiagram) : (Set.Iic μ).Finite

A Young diagram has finitely many sub-diagrams, each being determined by its set of cells.

theorem YoungDiagram.mem_iff_of_rowLen_le_one {μ : YoungDiagram} (h : μ.rowLen 0 ≤ 1) {i j : ℕ} : (i, j) ∈ μ ↔ i < μ.colLen 0 ∧ j = 0

The cells of a Young diagram with at most one column. Every row is then either empty or the single cell in column 0, so a cell is a cell of the first column, and the diagram reaches exactly as far down as that column does.

theorem YoungDiagram.cells_eq_of_rowLen_le_one {μ : YoungDiagram} (h : μ.rowLen 0 ≤ 1) : μ.cells = Finset.range (μ.colLen 0) ×ˢ {0}

The cells of a Young diagram with at most one column are exactly the cells (i, 0) with i < μ.colLen 0: the whole of its first column, and nothing else.

theorem YoungDiagram.card_eq_colLen_of_rowLen_le_one {μ : YoungDiagram} (h : μ.rowLen 0 ≤ 1) : μ.card = μ.colLen 0

A Young diagram with at most one column has one cell in each of its μ.colLen 0 rows.

theorem YoungDiagram.mem_iff_of_colLen_le_one {μ : YoungDiagram} (h : μ.colLen 0 ≤ 1) {i j : ℕ} : (i, j) ∈ μ ↔ i = 0 ∧ j < μ.rowLen 0

The cells of a Young diagram with at most one row. Every column is then either empty or the single cell in row 0, so a cell is a cell of the first row, and the diagram reaches exactly as far right as that row does.

theorem YoungDiagram.cells_eq_of_colLen_le_one {μ : YoungDiagram} (h : μ.colLen 0 ≤ 1) : μ.cells = {0} ×ˢ Finset.range (μ.rowLen 0)

The cells of a Young diagram with at most one row are exactly the cells (0, j) with j < μ.rowLen 0: the whole of its first row, and nothing else.

theorem YoungDiagram.card_eq_rowLen_of_colLen_le_one {μ : YoungDiagram} (h : μ.colLen 0 ≤ 1) : μ.card = μ.rowLen 0

A Young diagram with at most one row has one cell in each of its μ.rowLen 0 columns.