The corner recursion for standard Young tableaux

The largest label of a standard Young tableau of shape μ sits at a corner of μ (TauCeti.StandardYoungTableau.isCorner_maxCell), and deleting that cell leaves a standard Young tableau of the smaller shape. This is a bijection, and summing it over the corners gives the corner recursion

standardCount μ = ∑ c ∈ corners μ, standardCount (erase μ c)

for a nonempty diagram μ (TauCeti.standardCount_eq_sum_corners). It is the recursion the hook-length formula is proved by, and the one that makes standardCount computable from the shape alone.

The bijection is stated fibrewise, as an equivalence between the tableaux whose largest label sits at a given corner c and the tableaux of shape erase μ c, so that no type in this file depends on a tableau and no transport along an equality of shapes is needed; that is why TauCeti.StandardYoungTableau.restrict takes the corner and the equation naming it as parameters rather than reading them off its argument.

Main definitions

• TauCeti.StandardYoungTableau.maxCell: the cell carrying the largest label.
• TauCeti.StandardYoungTableau.restrict: delete the corner carrying the largest label.
• TauCeti.StandardYoungTableau.extend: the inverse, labelling a corner with the largest label.
• TauCeti.StandardYoungTableau.cornerFiberEquiv: the two as an equivalence.

Main results

• TauCeti.StandardYoungTableau.isCorner_maxCell: the largest label of a standard Young tableau sits at a corner.
• TauCeti.standardCount_eq_sum_corners: the corner recursion.

References

• W. Fulton, Young Tableaux, Section 1.1.
• B. E. Sagan, The Symmetric Group, Section 3.10, where the corner recursion opens the proof of the hook-length formula.
• Schur--Weyl roadmap, Layer 5, whose hookLengthFormula milestone is the induction this recursion drives.

The cell carrying the largest label

def TauCeti.StandardYoungTableau.maxCell {μ : YoungDiagram} (hμ : 0 < μ.card) (T : StandardYoungTableau μ) : ℕ × ℕ

The cell of a standard Young tableau of a nonempty shape that carries the largest label, μ.card - 1.

Equations

• TauCeti.StandardYoungTableau.maxCell hμ T = ↑((Equiv.symm T.toTableau) ⟨μ.card - 1, ⋯⟩)

theorem TauCeti.StandardYoungTableau.maxCell_mem {μ : YoungDiagram} (hμ : 0 < μ.card) (T : StandardYoungTableau μ) : maxCell hμ T ∈ μ

theorem TauCeti.StandardYoungTableau.apply_maxCell {μ : YoungDiagram} (hμ : 0 < μ.card) (T : StandardYoungTableau μ) : ↑(T ⟨maxCell hμ T, ⋯⟩) + 1 = μ.card

The label at TauCeti.StandardYoungTableau.maxCell is the largest one.

theorem TauCeti.StandardYoungTableau.isCorner_maxCell {μ : YoungDiagram} (hμ : 0 < μ.card) (T : StandardYoungTableau μ) : μ.IsCorner (maxCell hμ T)

The largest label of a standard Young tableau sits at a corner. Neither the cell to its right nor the cell below it can be in the diagram, since either would carry a strictly larger label.

theorem TauCeti.StandardYoungTableau.maxCell_eq_iff {μ : YoungDiagram} {c : ℕ × ℕ} (hμ : 0 < μ.card) (T : StandardYoungTableau μ) (hc : c ∈ μ) : maxCell hμ T = c ↔ ↑(T ⟨c, hc⟩) + 1 = μ.card

A cell carries the largest label exactly when it is the cell TauCeti.StandardYoungTableau.maxCell.

Deleting the corner carrying the largest label

noncomputable def TauCeti.StandardYoungTableau.restrict {μ : YoungDiagram} {c : ℕ × ℕ} (hc : μ.IsCorner c) (T : StandardYoungTableau μ) (hT : ↑(T ⟨c, ⋯⟩) + 1 = μ.card) : StandardYoungTableau (μ.erase c)

Deleting the corner carrying the largest label from a standard Young tableau. The corner c and the fact that it carries the largest label are parameters rather than being read off T, so that the shape of the result does not depend on T.

Equations

• TauCeti.StandardYoungTableau.restrict hc T hT = { toTableau := Equiv.ofBijective (TauCeti.StandardYoungTableau.restrictFun✝ hc T hT) ⋯, row_strict' := ⋯, col_strict' := ⋯ }

@[simp]

theorem TauCeti.StandardYoungTableau.restrict_apply_val {μ : YoungDiagram} {c : ℕ × ℕ} (hc : μ.IsCorner c) (T : StandardYoungTableau μ) (hT : ↑(T ⟨c, ⋯⟩) + 1 = μ.card) (d : ↥(μ.erase c).cells) : ↑((restrict hc T hT) d) = ↑(T ⟨↑d, ⋯⟩)

Labelling a corner with the largest label

noncomputable def TauCeti.StandardYoungTableau.extend {μ : YoungDiagram} {c : ℕ × ℕ} (hc : μ.IsCorner c) (T : StandardYoungTableau (μ.erase c)) : StandardYoungTableau μ

Restoring a deleted corner: extend a standard Young tableau of shape erase μ c to one of shape μ by giving the corner c the largest label.

Equations

• TauCeti.StandardYoungTableau.extend hc T = { toTableau := Equiv.ofBijective (TauCeti.StandardYoungTableau.extendFun✝ hc T) ⋯, row_strict' := ⋯, col_strict' := ⋯ }

@[simp]

theorem TauCeti.StandardYoungTableau.extend_apply_val_of_eq {μ : YoungDiagram} {c : ℕ × ℕ} (hc : μ.IsCorner c) (T : StandardYoungTableau (μ.erase c)) (d : ↥μ.cells) (h : ↑d = c) : ↑((extend hc T) d) = μ.card - 1

@[simp]

theorem TauCeti.StandardYoungTableau.extend_apply_val_of_ne {μ : YoungDiagram} {c : ℕ × ℕ} (hc : μ.IsCorner c) (T : StandardYoungTableau (μ.erase c)) (d : ↥μ.cells) (h : ↑d ≠ c) : ↑((extend hc T) d) = ↑(T ⟨↑d, ⋯⟩)

theorem TauCeti.StandardYoungTableau.extend_apply_self {μ : YoungDiagram} {c : ℕ × ℕ} (hc : μ.IsCorner c) (T : StandardYoungTableau (μ.erase c)) : ↑((extend hc T) ⟨c, ⋯⟩) + 1 = μ.card

The extended tableau does carry its largest label at the restored corner, so it lies in the fibre that TauCeti.StandardYoungTableau.restrict is defined on.

This is deliberately not a simp lemma: TauCeti.StandardYoungTableau.extend_apply_val_of_eq rewrites its left-hand side to μ.card - 1 + 1, so its statement is not in simp-normal form.

@[simp]

theorem TauCeti.StandardYoungTableau.restrict_extend {μ : YoungDiagram} {c : ℕ × ℕ} (hc : μ.IsCorner c) (T : StandardYoungTableau (μ.erase c)) : restrict hc (extend hc T) ⋯ = T

@[simp]

theorem TauCeti.StandardYoungTableau.extend_restrict {μ : YoungDiagram} {c : ℕ × ℕ} (hc : μ.IsCorner c) (T : StandardYoungTableau μ) (hT : ↑(T ⟨c, ⋯⟩) + 1 = μ.card) : extend hc (restrict hc T hT) = T

noncomputable def TauCeti.StandardYoungTableau.cornerFiberEquiv {μ : YoungDiagram} {c : ℕ × ℕ} (hc : μ.IsCorner c) : { T : StandardYoungTableau μ // ↑(T ⟨c, ⋯⟩) + 1 = μ.card } ≃ StandardYoungTableau (μ.erase c)

The corner bijection: the standard Young tableaux of shape μ whose largest label sits at the corner c are the standard Young tableaux of shape erase μ c.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.standardCount_eq_sum_corners {μ : YoungDiagram} (hμ : 0 < μ.card) : standardCount μ = ∑ c ∈ μ.corners, standardCount (μ.erase c)

The corner recursion for standard Young tableaux: the standard Young tableaux of a nonempty shape μ are counted by their corners, a tableau being recorded by the corner carrying its largest label together with what is left after deleting that corner.