Finite sets of cells, closed in the row direction

A finite set D : Finset (ι × κ) of cells has its rows indexed by ι and its columns indexed by κ. This file counts the cells of D one row at a time (TauCeti.CellDiagram.rowLen), imposes closure in the row direction (TauCeti.CellDiagram.IsRowLowerSet: with every cell, D contains the cells directly above it), and builds the set of cells lying under a prescribed tuple of row lengths (TauCeti.CellDiagram.ofRowLens).

Main definitions

• TauCeti.CellDiagram.rowLen: the number of cells of a set lying in a given row.
• TauCeti.CellDiagram.IsRowLowerSet: the lower-set property in the row direction.
• TauCeti.CellDiagram.ofRowLens: the cells lying under a tuple of row lengths.

Main results

• TauCeti.CellDiagram.isRowLowerSet_ofRowLens: the cells under a weakly decreasing tuple of row lengths are closed in the row direction.
• TauCeti.CellDiagram.rowLen_ofRowLens and TauCeti.CellDiagram.card_ofRowLens: the rows of those cells have lengths min (a i) m, and there are ∑ i, min (a i) m cells in all. When ∀ i, a i ≤ m, the corresponding of_le corollaries give the prescribed row lengths and total.

Implementation notes

Mathlib's YoungDiagram is a set of cells in ℕ × ℕ closed downwards in both directions, and its rows are indexed by ℕ. The rows here are indexed by an abstract type ι, and only closure in the row direction is imposed, because that is the condition the consumers need: it is exactly what makes the raising operators of gl ι annihilate the wedge of the basis vectors indexed by the cells, in TauCeti.isGlHighestWeightVector_basisWedge.

Counting the cells of a row

def TauCeti.CellDiagram.rowLen {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] (D : Finset (ι × κ)) (i : ι) : ℕ

The number of cells of D lying in row i.

Equations

• TauCeti.CellDiagram.rowLen D i = {p ∈ D | p.1 = i}.card

theorem TauCeti.CellDiagram.rowLen_eq_card_filter {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] (D : Finset (ι × κ)) (i : ι) : rowLen D i = {p ∈ D | p.1 = i}.card

TauCeti.CellDiagram.rowLen unfolded. The definition is not exposed, so this is how the row lengths are computed outside this file.

theorem TauCeti.CellDiagram.rowLen_eq_card_filter_mem {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [Fintype κ] [DecidableEq κ] (D : Finset (ι × κ)) (i : ι) : rowLen D i = {c : κ | (i, c) ∈ D}.card

The cells of D in row i, counted by their column index.

Closure in the row direction

def TauCeti.CellDiagram.IsRowLowerSet {ι : Type u_1} {κ : Type u_2} [LT ι] (D : Finset (ι × κ)) : Prop

A set of cells is a row lower set when with every cell it contains all the cells directly above it: if (j, c) is a cell and i < j, then (i, c) is a cell. In other words D is a lower set in its row index. This is one of the two conditions on the shape of a Young diagram, the one in the row direction; closure in the column direction is not imposed.

Equations

• TauCeti.CellDiagram.IsRowLowerSet D = ∀ p ∈ D, ∀ i < p.1, (i, p.2) ∈ D

theorem TauCeti.CellDiagram.isRowLowerSet_iff {ι : Type u_1} {κ : Type u_2} [LT ι] {D : Finset (ι × κ)} : IsRowLowerSet D ↔ ∀ p ∈ D, ∀ i < p.1, (i, p.2) ∈ D

TauCeti.CellDiagram.IsRowLowerSet unfolded. The definition is not exposed, so this is how the condition is introduced and eliminated outside this file.

The cells under a tuple of row lengths

def TauCeti.CellDiagram.ofRowLens {ι : Type u_1} [Fintype ι] (a : ι → ℕ) (m : ℕ) : Finset (ι × Fin m)

The cells lying under the row lengths a: those cells (i, c) whose column index c is smaller than the i-th row length. The columns are drawn from Fin m, so a row longer than m is truncated.

Equations

• TauCeti.CellDiagram.ofRowLens a m = {p : ι × Fin m | ↑p.2 < a p.1}

@[simp]

theorem TauCeti.CellDiagram.mem_ofRowLens_iff {ι : Type u_1} [Fintype ι] {a : ι → ℕ} {m : ℕ} {p : ι × Fin m} : p ∈ ofRowLens a m ↔ ↑p.2 < a p.1

theorem TauCeti.CellDiagram.isRowLowerSet_ofRowLens {ι : Type u_1} [Fintype ι] [Preorder ι] {a : ι → ℕ} (ha : Antitone a) (m : ℕ) : IsRowLowerSet (ofRowLens a m)

The cells under a weakly decreasing tuple of row lengths are closed in the row direction.

@[simp]

theorem TauCeti.CellDiagram.rowLen_ofRowLens {ι : Type u_1} [Fintype ι] [DecidableEq ι] (a : ι → ℕ) (m : ℕ) (i : ι) : rowLen (ofRowLens a m) i = min (a i) m

A row of the cells under a has the requested length, truncated to the available width m.

theorem TauCeti.CellDiagram.rowLen_ofRowLens_of_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {a : ι → ℕ} {m : ℕ} (hm : ∀ (i : ι), a i ≤ m) (i : ι) : rowLen (ofRowLens a m) i = a i

The rows of the cells under a have the lengths a prescribes when there are enough columns to hold them.

@[simp]

theorem TauCeti.CellDiagram.card_ofRowLens {ι : Type u_1} [Fintype ι] (a : ι → ℕ) (m : ℕ) : (ofRowLens a m).card = ∑ i : ι, min (a i) m

The number of cells under a is the sum of the row lengths truncated to width m.

theorem TauCeti.CellDiagram.card_ofRowLens_of_le {ι : Type u_1} [Fintype ι] {a : ι → ℕ} {m : ℕ} (hm : ∀ (i : ι), a i ≤ m) : (ofRowLens a m).card = ∑ i : ι, a i

The cells under a are one for each unit of each row length when there are enough columns to hold them.