Young's Lattice: Raising and Lowering Operators (Lemma 8.2) #
This file formalizes Lemma 8.2 from the textbook: the commutation relation
D_{i+1} U_i - U_{i-1} D_i = I_i for raising/lowering operators on Young's lattice.
Definitions from the Book (Section 8) #
Young's lattice Y is a graded poset where level Y_i consists of all partitions of i,
represented as YoungDiagrams with card = i. The covering relation holds iff
the larger diagram is obtained from the smaller by adding exactly one cell.
The raising operator U_i : ℤ[Y_i] → ℤ[Y_{i+1}] maps a partition λ to the formal sum
of all partitions covering it: U_i(λ) = ∑_{μ : λ ⋖ μ} μ.
The lowering operator D_i : ℤ[Y_i] → ℤ[Y_{i-1}] maps a partition λ to the formal sum
of all partitions it covers: D_i(λ) = ∑_{ν : ν ⋖ λ} ν.
Main results #
YoungDiagram.raisingOp/YoungDiagram.loweringOp: Definitions of U and D as maps fromYoungDiagramto the free ℤ-moduleYoungDiagram →₀ ℤ.YoungDiagram.DU_apply/YoungDiagram.UD_apply: The coefficients of the compositionsD ∘ UandU ∘ Dapplied to basis elements.YoungDiagram.young_commutation_coeff: Lemma 8.2 — The commutation relationDU(lam)(mu) - UD(lam)(mu) = δ_{lam,mu}at the coefficient level.
References #
- Section 8 of the textbook (Young's Lattice)
Row length basic lemmas #
Row lengths of a Young diagram form an antitone sequence.
Addable rows and removable rows #
The addable rows of a Young diagram μ are the row indices where a cell can be
added to produce a valid Young diagram. The removable rows are the row indices
where a cell can be removed.
If r is the number of distinct parts of μ, then μ has r + 1 addable rows
and r removable rows.
Addable rows: indices i ∈ {0, ..., colLen 0} where i = 0 or rowLen drops.
Instances For
Removable rows: indices i ∈ {0, ..., colLen 0 - 1} where rowLen drops after i.
Instances For
Bijection between removable rows and non-zero addable rows #
Addable rows = {0} ∪ (removable rows shifted by +1).
Key lemma: A Young diagram has exactly one more addable row than removable row.
If r is the number of distinct parts, there are r + 1 addable and r removable rows.
Constructing Young diagrams by adding/removing cells #
Add a cell at position (i, μ.rowLen i) to a Young diagram μ, given that
i is an addable row (either i = 0 or μ.rowLen (i-1) > μ.rowLen i).
Instances For
Covering sets in Young's lattice #
The finset of Young diagrams covering μ (obtained by adding one cell).
These are the diagrams σ with μ ⋖ σ in Young's lattice.
Instances For
The finset of Young diagrams covered by μ (obtained by removing one cell).
These are the diagrams ν with ν ⋖ μ in Young's lattice.
Instances For
Raising and lowering operators #
The raising operator U sends a Young diagram λ to the formal ℤ-linear combination
∑_{σ : λ ⋖ σ} σ ∈ YoungDiagram →₀ ℤ, where the sum is over all diagrams covering λ.
The lowering operator D sends λ to ∑_{ν : ν ⋖ λ} ν.
The book defines U_i : ℝ[Y_i] → ℝ[Y_{i+1}] and D_i : ℝ[Y_i] → ℝ[Y_{i-1}] by extending
these maps linearly. Here we define them on basis elements using Finsupp (formal linear
combinations with integer coefficients).
The raising operator U on a basis element: U(lam) = ∑_{σ ∈ coversUp(lam)} σ.
Instances For
The lowering operator D on a basis element: D(lam) = ∑_{ν ∈ coversDown(lam)} ν.
Instances For
The coefficient of mu in (D ∘ U)(lam):
Apply U to lam to get a formal sum of covering diagrams σ, then apply D to each σ
and read off the coefficient of mu. This equals the number of intermediate diagrams
σ ⊢ (i+1) with lam ⋖ σ and σ ⋗ mu.
Instances For
The coefficient of mu in (U ∘ D)(lam):
Apply D to lam to get a formal sum of covered diagrams ν, then apply U to each ν
and read off the coefficient of mu. This equals the number of intermediate diagrams
ν ⊢ (i-1) with lam ⋗ ν and ν ⋖ mu.
Instances For
Closed-form coefficient formulas #
The textbook proof of Lemma 8.2 establishes that the composition coefficients DU_apply
and UD_apply take specific values depending on the relationship between lam and mu:
- Case
lam = mu:DU_apply = r + 1,UD_apply = r, wherer = |removableRows(lam)|. - Case
lam ≠ mu, symmetric diff of size 2: both equal 1. - Otherwise: both equal 0.
The following definitions capture these closed forms. The main theorem is proved using these formulas, which encode the combinatorial content of the textbook's case analysis.
Semantic DU and UD coefficients #
DUCoeff lam mu counts the number of σ ∈ coversUp(lam) such that mu ∈ coversDown(σ),
and UDCoeff lam mu counts the number of ρ ∈ coversDown(lam) such that mu ∈ coversUp(ρ).
These are the true operator-composition coefficients.
DUCoeff lam mu is the coefficient of mu in D_{i+1}(U_i(lam)):
the number of diagrams σ in coversUp(lam) such that mu ∈ coversDown(σ).
Instances For
UDCoeff lam mu is the coefficient of mu in U_{i-1}(D_i(lam)):
the number of diagrams ρ in coversDown(lam) such that mu ∈ coversUp(ρ).
Instances For
Case-split characterizations #
The book proves by case analysis that the semantic definitions equal these closed forms.
Case-split formula for DUCoeff.
Instances For
Case-split formula for UDCoeff.
Instances For
Helper lemmas for intermediate_unique_of_symm_diff #
If mu.cells \ lam.cells has cardinality 1, extract the unique cell (j, lam.rowLen j)
and show j ∈ lam.addableRows.
Given the sdiff singletons, lam.addCell j hadd is in the intermediate filter.
Any σ in the intermediate filter must equal lam.addCell j hadd.
If lam.cells \ mu.cells has cardinality 1, extract the unique cell (k, lam.rowLen k - 1)
and show k ∈ lam.removableRows.
Given the sdiff singletons, lam.removeCell k hrem is in the UD intermediate filter.
Any ρ in the UD intermediate filter must equal lam.removeCell k hrem.
When lam ≠ mu, DUCoeff = UDCoeff (both check the same symmetric
difference condition and return the same value).
Lemma 8.2: The commutation relation #
Lemma 8.2. For any i ≥ 0, D_{i+1} U_i - U_{i-1} D_i = I_i,
where I_i is the identity on ℤ[Y_i].
At the coefficient level: for any Young diagrams lam and mu,
the coefficient of mu in (D_{i+1} ∘ U_i)(lam) minus the coefficient of mu
in (U_{i-1} ∘ D_i)(lam) equals 1 if lam = mu, and 0 otherwise.
The coefficients DUCoeff and UDCoeff are defined semantically as counts of
intermediate diagrams via coversUp/coversDown.
Proof (from the textbook):
- Case 1 (
mu ≠ lam, obtainable):muis obtained fromlamby adding one cellsthen removing a different cellt. There is exactly one such intermediateσ = lam + s, givingDU_apply = 1. Conversely, one can removetthen adds, givingUD_apply = 1. So the difference is1 - 1 = 0. - Case 2 (
mu ≠ lam, not obtainable): Both coefficients are 0. - Case 3 (
mu = lam): There arer + 1ways to add then remove a cell (one per addable row), andrways to remove then add (one per removable row). The difference is(r + 1) - r = 1.