Corners of a Young diagram

A corner of a Young diagram μ is a cell of μ with neither the cell to its right nor the cell below it in μ. Equivalently, the corners are the maximal cells of μ (YoungDiagram.IsCorner.eq_of_le): they are exactly the cells c for which removing c alone leaves a set of cells that is still a Young diagram. So they index the ways of building μ one cell at a time, and hence the recursions that count standard Young tableaux. The corners are also exactly the cells of hook length 1, which is YoungDiagram.isCorner_iff_hookLength_eq_one in TauCeti.Combinatorics.Young.HookLength.Basic, downstream of this file.

Deletion is YoungDiagram.erase. It is defined without any hypothesis on the cell — it removes the whole principal upper set of c, that is c together with every cell weakly below and to the right of it — so that it can be summed over the corners of μ with no dependent index. At a corner, and only at a cell of μ that is a corner, nothing but c itself is removed (YoungDiagram.IsCorner.cells_erase), and at a cell outside μ nothing is removed at all.

Main definitions

• YoungDiagram.IsCorner: the predicate cutting out the corners of a diagram.
• YoungDiagram.corners: the corners of a diagram, as a Finset.
• YoungDiagram.erase: the diagram with the principal upper set of a cell removed.

Main results

• YoungDiagram.IsCorner.cells_erase: erasing a corner deletes exactly that cell, and YoungDiagram.IsCorner.card_erase: it drops the number of cells by one.
• YoungDiagram.exists_isCorner: a nonempty Young diagram has a corner, so the corner recursions are not vacuous.
• YoungDiagram.IsCorner.eq_of_fst_eq: the corners of a diagram sit in distinct rows, and YoungDiagram.IsCorner.fst_lt_colLen_zero: those rows are rows of the diagram.
• YoungDiagram.corners_transpose and YoungDiagram.erase_transpose: corners and deletion commute with transposition.

References

• W. Fulton, Young Tableaux, Section 1.1.
• B. E. Sagan, The Symmetric Group, Section 3.10, where the corner recursion for standard Young tableaux is the starting point of the hook-length formula.
• Schur--Weyl roadmap, Layer 5, whose hookLengthFormula milestone is proved by induction along the corners of μ.

Corners

def YoungDiagram.IsCorner (μ : YoungDiagram) (c : ℕ × ℕ) : Prop

A corner of a Young diagram: a cell of μ with neither the cell to its right nor the cell below it in μ. These are exactly the maximal cells of μ (YoungDiagram.IsCorner.eq_of_le), equivalently the cells whose removal on its own leaves a set of cells that is still a Young diagram.

Equations

• μ.IsCorner c = (c ∈ μ ∧ (c.1, c.2 + 1) ∉ μ ∧ (c.1 + 1, c.2) ∉ μ)

theorem YoungDiagram.isCorner_def (μ : YoungDiagram) (c : ℕ × ℕ) : μ.IsCorner c ↔ c ∈ μ ∧ (c.1, c.2 + 1) ∉ μ ∧ (c.1 + 1, c.2) ∉ μ

The defining conjunction of YoungDiagram.IsCorner, for introducing and eliminating the predicate.

@[instance_reducible]

instance YoungDiagram.instDecidableIsCorner (μ : YoungDiagram) (c : ℕ × ℕ) : Decidable (μ.IsCorner c)

Equations

• μ.instDecidableIsCorner c = decidable_of_iff (c ∈ μ ∧ (c.1, c.2 + 1) ∉ μ ∧ (c.1 + 1, c.2) ∉ μ) ⋯

theorem YoungDiagram.IsCorner.mem {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsCorner c) : c ∈ μ

theorem YoungDiagram.IsCorner.right_notMem {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsCorner c) : (c.1, c.2 + 1) ∉ μ

theorem YoungDiagram.IsCorner.below_notMem {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsCorner c) : (c.1 + 1, c.2) ∉ μ

theorem YoungDiagram.IsCorner.eq_of_le {μ : YoungDiagram} {c d : ℕ × ℕ} (h : μ.IsCorner c) (hd : d ∈ μ) (hcd : c ≤ d) : d = c

A corner is a maximal cell: the only cell of μ weakly below and to the right of a corner is the corner itself.

theorem YoungDiagram.IsCorner.le_iff {μ : YoungDiagram} {c d : ℕ × ℕ} (h : μ.IsCorner c) (hd : d ∈ μ) : c ≤ d ↔ d = c

def YoungDiagram.corners (μ : YoungDiagram) : Finset (ℕ × ℕ)

The corners of a Young diagram, as a finite set of cells.

Equations

• μ.corners = Finset.filter μ.IsCorner μ.cells

@[simp]

theorem YoungDiagram.mem_corners {μ : YoungDiagram} {c : ℕ × ℕ} : c ∈ μ.corners ↔ μ.IsCorner c

theorem YoungDiagram.corners_subset_cells (μ : YoungDiagram) : μ.corners ⊆ μ.cells

theorem YoungDiagram.exists_isCorner {μ : YoungDiagram} (hμ : 0 < μ.card) : ∃ (c : ℕ × ℕ), μ.IsCorner c

A nonempty Young diagram has a corner: a cell maximizing i + j has neither the cell to its right nor the cell below it in the diagram.

theorem YoungDiagram.corners_nonempty {μ : YoungDiagram} (hμ : 0 < μ.card) : μ.corners.Nonempty

Deleting a corner

def YoungDiagram.erase (μ : YoungDiagram) (c : ℕ × ℕ) : YoungDiagram

The Young diagram obtained from μ by deleting the cell c together with every cell weakly below and to the right of it.

The definition is total, so that it can be summed over the corners of μ without a dependent index. It is Finset.erase on cells exactly at a corner (YoungDiagram.IsCorner.cells_erase), and it leaves μ unchanged at a cell outside μ (YoungDiagram.erase_eq_self_of_notMem); at a cell of μ that is not a corner it deletes the entire principal upper set of c in μ, which is the price of totality.

Equations

• μ.erase c = { cells := {d ∈ μ.cells | ¬c ≤ d}, isLowerSet := ⋯ }

@[simp]

theorem YoungDiagram.mem_erase {μ : YoungDiagram} {c d : ℕ × ℕ} : d ∈ μ.erase c ↔ d ∈ μ ∧ ¬c ≤ d

theorem YoungDiagram.mem_of_mem_erase {μ : YoungDiagram} {c d : ℕ × ℕ} (h : d ∈ μ.erase c) : d ∈ μ

theorem YoungDiagram.erase_le (μ : YoungDiagram) (c : ℕ × ℕ) : μ.erase c ≤ μ

@[simp]

theorem YoungDiagram.erase_eq_self_of_notMem {μ : YoungDiagram} {c : ℕ × ℕ} (h : c ∉ μ) : μ.erase c = μ

theorem YoungDiagram.IsCorner.mem_erase_iff {μ : YoungDiagram} {c d : ℕ × ℕ} (h : μ.IsCorner c) : d ∈ μ.erase c ↔ d ∈ μ ∧ d ≠ c

@[simp]

theorem YoungDiagram.IsCorner.cells_erase {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsCorner c) : (μ.erase c).cells = μ.cells.erase c

theorem YoungDiagram.IsCorner.notMem_erase {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsCorner c) : c ∉ μ.erase c

@[simp]

theorem YoungDiagram.IsCorner.card_erase {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsCorner c) : (μ.erase c).card + 1 = μ.card

Erasing a corner drops the number of cells by exactly one.

theorem YoungDiagram.IsCorner.card_pos {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsCorner c) : 0 < μ.card

Rows and columns after erasure

@[simp]

theorem YoungDiagram.IsCorner.row_erase {μ : YoungDiagram} {c : ℕ × ℕ} {i : ℕ} (h : μ.IsCorner c) : (μ.erase c).row i = (μ.row i).erase c

Erasing a corner erases that cell from every row finset. Only its own row contains it.

@[simp]

theorem YoungDiagram.IsCorner.col_erase {μ : YoungDiagram} {c : ℕ × ℕ} {j : ℕ} (h : μ.IsCorner c) : (μ.erase c).col j = (μ.col j).erase c

Erasing a corner erases that cell from every column finset. Only its own column contains it.

@[simp]

theorem YoungDiagram.IsCorner.rowLen_erase {μ : YoungDiagram} {c : ℕ × ℕ} {i : ℕ} (h : μ.IsCorner c) : (μ.erase c).rowLen i = if c.1 = i then μ.rowLen i - 1 else μ.rowLen i

Erasing a corner shortens its row by one and leaves every other row unchanged.

@[simp]

theorem YoungDiagram.IsCorner.colLen_erase {μ : YoungDiagram} {c : ℕ × ℕ} {j : ℕ} (h : μ.IsCorner c) : (μ.erase c).colLen j = if c.2 = j then μ.colLen j - 1 else μ.colLen j

Erasing a corner shortens its column by one and leaves every other column unchanged.

theorem YoungDiagram.IsCorner.rowLen_eq_snd_add_one {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsCorner c) : μ.rowLen c.1 = c.2 + 1

A corner is the final cell of its row.

theorem YoungDiagram.IsCorner.colLen_eq_fst_add_one {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsCorner c) : μ.colLen c.2 = c.1 + 1

A corner is the final cell of its column.

theorem YoungDiagram.IsCorner.eq_of_fst_eq {μ : YoungDiagram} {c d : ℕ × ℕ} (hc : μ.IsCorner c) (hd : μ.IsCorner d) (h : c.1 = d.1) : c = d

A corner is the final cell of its row, so it is determined by the row it lies in: the corners of a diagram sit in distinct rows.

theorem YoungDiagram.IsCorner.fst_lt_colLen_zero {μ : YoungDiagram} {c : ℕ × ℕ} (h : μ.IsCorner c) : c.1 < μ.colLen 0

The row of a corner is one of the rows of the diagram.

Transposition

@[simp]

theorem YoungDiagram.isCorner_transpose {μ : YoungDiagram} {c : ℕ × ℕ} : μ.transpose.IsCorner c ↔ μ.IsCorner c.swap

@[simp]

theorem YoungDiagram.corners_transpose (μ : YoungDiagram) : μ.transpose.corners = Finset.image Prod.swap μ.corners

@[simp]

theorem YoungDiagram.erase_transpose (μ : YoungDiagram) (c : ℕ × ℕ) : μ.transpose.erase c = (μ.erase c.swap).transpose