Sum of Squares of Standard Young Tableaux Equals Factorial (Corollary 8.4)

This file states Corollary 8.4 from Stanley's Algebraic Combinatorics:

$$\alpha(D^n U^n, \emptyset) = \sum_{\lambda \vdash n} (f^\lambda)^2 = n!$$

where the sum is over all partitions λ of n, and f^λ denotes the number of standard Young tableaux of shape λ, and α(w, λ) counts Hasse walks of type w from ∅ to λ.

Main results

• youngDiagramsOfSize : the Finset of all Young diagrams with n cells.
• walkTypeCount_dnUn_eq_sum_numSYT_sq : the first equality α(D^n U^n, ∅) = ∑(f^λ)².
• sum_numSYT_sq_eq_factorial : the second equality ∑(f^λ)² = n!.

References

• Stanley, Algebraic Combinatorics, Corollary 8.4

The finite set of partitions of n

theorem YoungDiagram.cells_subset_range_sq (μ : YoungDiagram) : μ.cells ⊆ Finset.range μ.card ×ˢ Finset.range μ.card

The cells of a Young diagram are contained in Finset.range card ×ˢ Finset.range card.

theorem finite_youngDiagrams_of_size (n : ℕ) : {μ : YoungDiagram | μ.card = n}.Finite

There are finitely many Young diagrams of any given size.

noncomputable def youngDiagramsOfSize (n : ℕ) : Finset YoungDiagram

The Finset of all Young diagrams of size n (i.e., partitions of n).

@[simp]

theorem mem_youngDiagramsOfSize {n : ℕ} {μ : YoungDiagram} : μ ∈ youngDiagramsOfSize n ↔ μ.card = n

Corollary 8.4

def dnUn (n : ℕ) : List HasseWalks.HStep

The word D^n U^n as a List HStep.

In the code's convention, steps[0] is the first step applied (corresponding to the rightmost operator in the book's notation D^n U^n = A_{2n} ⋯ A_1). For D^n U^n, the walk first goes UP n steps (A₁ through Aₙ are all U), then DOWN n steps (A_{n+1} through A_{2n} are all D).

theorem hasseWalk_d_from_bot_isEmpty (rest : List HasseWalks.HStep) (target : YoungDiagram) : IsEmpty (HasseWalks.HasseWalk (HasseWalks.HStep.D :: rest) ⊥ target)

Any HasseWalk starting with D from ⊥ is impossible.

theorem walkTypeCount_D_cons_bot (rest : List HasseWalks.HStep) (μ : YoungDiagram) : WalkTypeCount.walkTypeCount (HasseWalks.HStep.D :: rest) μ = 0

theorem walkTypeCount_nil_bot : WalkTypeCount.walkTypeCount [] ⊥ = 1

theorem youngDiagramsOfSize_zero : youngDiagramsOfSize 0 = {⊥}

theorem WalkTypeCount.applyStepWord_append (w₁ w₂ : List HasseWalks.HStep) (f : YoungDiagram →₀ ℤ) : applyStepWord (w₁ ++ w₂) f = applyStepWord w₂ (applyStepWord w₁ f)

applyStepWord distributes over list append: processing w₁ ++ w₂ is the same as processing w₁ first, then w₂.

theorem walkTypeCount_dnUn_eq_sum_over_partitions (n : ℕ) : WalkTypeCount.walkTypeCount (dnUn n) ⊥ = ∑ μ ∈ youngDiagramsOfSize n, WalkTypeCount.walkTypeCount (List.replicate n HasseWalks.HStep.U) μ * Nat.card (HasseWalks.HasseWalk (List.replicate n HasseWalks.HStep.D) μ ⊥)

theorem hasseWalkCount_allD_to_bot_eq_numSYT (n : ℕ) (μ : YoungDiagram) (hμ : μ.card = n) : Nat.card (HasseWalks.HasseWalk (List.replicate n HasseWalks.HStep.D) μ ⊥) = HasseWalkFormula.numSYT μ

theorem walkTypeCount_allU_eq_numSYT (n : ℕ) (μ : YoungDiagram) (hμ : μ.card = n) : WalkTypeCount.walkTypeCount (List.replicate n HasseWalks.HStep.U) μ = HasseWalkFormula.numSYT μ

theorem walkTypeCount_dnUn_eq_sum_numSYT_sq (n : ℕ) : WalkTypeCount.walkTypeCount (dnUn n) ⊥ = ∑ μ ∈ youngDiagramsOfSize n, HasseWalkFormula.numSYT μ ^ 2

Corollary 8.4, first equality (Stanley, Algebraic Combinatorics). α(D^n U^n, ∅) = ∑_{λ⊢n} (f^λ)².

The book derives this from Theorem 8.3: for the word w = D^n U^n the down-step product ∏_{i ∈ S_w}(b_i - a_i) equals n!, and Theorem 8.3 gives α(w, λ) = f^λ · ∏(b_i - a_i). Summing over all λ ⊢ n and using the fact that α(D^n U^n, ∅) counts all walks that return to ∅, one obtains the identity.

theorem dnUn_downStepProduct_eq_factorial (n : ℕ) : WalkTypeCount.downStepProduct (dnUn n) = ↑n.factorial

theorem isValidStepWord_dnUn (n : ℕ) : WalkTypeCount.IsValidStepWord (dnUn n) 0

dnUn n is a valid 0-word: it has net displacement 0 and all prefixes have non-negative running level.

theorem walkTypeCount_dnUn_bot_eq_factorial (n : ℕ) : WalkTypeCount.walkTypeCount (dnUn n) ⊥ = n.factorial

theorem sum_numSYT_sq_eq_factorial (n : ℕ) : ∑ μ ∈ youngDiagramsOfSize n, HasseWalkFormula.numSYT μ ^ 2 = n.factorial

Corollary 8.4, second equality (Stanley, Algebraic Combinatorics). ∑_{λ⊢n} (f^λ)² = n!.

The book derives this from Theorem 8.3 applied to the word w = D^n U^n: the down-step positions are S_w = {n, …, 2n−1} with a_i = 2n − 1 − i and b_i = n, so the product ∏{i=1}^{n} (b_i − a_i) = ∏{i=1}^{n} i = n!. Combining with the first equality α(D^n U^n, ∅) = ∑(f^λ)² from walkTypeCount_dnUn_eq_sum_numSYT_sq and the walk count walkTypeCount_dnUn_bot_eq_factorial, the result follows by transitivity.