Eigenvalues of Young's Lattice Bipartite Graph (Theorem 8.8)

This file formalizes Theorem 8.8 from Stanley's Algebraic Combinatorics: the eigenvalues of the bipartite graph Y_{j-1,j} (Young's lattice restricted to consecutive ranks j-1 and j) are ±√s for 1 ≤ s ≤ j, each with multiplicity p(j-s) - p(j-s-1), plus eigenvalue 0 with multiplicity p(j) - p(j-1), where p(i) is the number of partitions of i.

Main results

• YoungEigenvalues.DU_apply: From DU - UD = I, derive D(U(w)) = U(D(w)) + w.
• YoungEigenvalues.iterated_DU_ker: Equation (43): for v ∈ ker D, D(U^{k+1}(v)) = (k+1) · U^k(v).
• YoungEigenvalues.abstract_eigenvalue_multiplicities: Theorem 8.8 in abstract form, for generic vector spaces with operators satisfying the commutation relation.
• YoungEigenvalues.PartitionSpace: Concrete level space ℝY_j = (Nat.Partition j →₀ ℝ).
• YoungEigenvalues.finrank_partitionSpace: dim(PartitionSpace j) = p(j).
• YoungEigenvalues.young_lattice_eigenvalue_multiplicities: Theorem 8.8 (full) specialized to Young's lattice level spaces PartitionSpace j, with multiplicity data and completeness.

Proof strategy

The adjacency matrix A of Y_{j-1,j} acts on ℝY_{j-1} ⊕ ℝY_j by A(a, b) = (D(b), U(a)). The commutation relation DU - UD = I (Lemma 8.2) implies the iterated formula D(U^{k+1}(v)) = (k+1) · U^k(v) for v ∈ ker D. From this, the vector w = (±√s · U^{s-1}(v), U^s(v)) satisfies A(w) = ±√s · w, giving eigenvalue Real.sqrt s (resp. -Real.sqrt s).

References

• Section 8, Theorem 8.8 of the textbook

Partition count function

noncomputable def YoungEigenvalues.p (n : ℕ) : ℕ

The number of partitions of n, i.e., |Y_n| in Young's lattice.

Abstract commutation algebra

We work with abstract endomorphisms U, D : V →ₗ[ℝ] V satisfying the commutation relation D * U - U * D = 1 (i.e., DU - UD = Id), which is the operator form of Lemma 8.2 on Young's lattice.

theorem YoungEigenvalues.DU_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (U D : Module.End ℝ V) (hcomm : D * U - U * D = 1) (w : V) : D (U w) = U (D w) + w

From the commutation relation DU - UD = I, derive the pointwise identity D(U(w)) = U(D(w)) + w for all w.

theorem YoungEigenvalues.iterated_DU_ker {V : Type u_1} [AddCommGroup V] [Module ℝ V] (U D : Module.End ℝ V) (hcomm : D * U - U * D = 1) (v : V) (hv : D v = 0) (k : ℕ) : D ((U ^ (k + 1)) v) = ↑(k + 1) • (U ^ k) v

Equation (43). For v ∈ ker D and operators satisfying DU - UD = I, the iterated commutation relation D(U^{k+1}(v)) = (k+1) · U^k(v) holds. This is proved by induction on k, using DU_apply at each step.

Multiplicities and completeness (Theorem 8.8, full statement)

The full statement of Theorem 8.8 includes multiplicity data:

• Eigenvalue 0 with multiplicity p(j) - p(j-1) (from ker(D_j)).
• For each 0 ≤ s ≤ j-1, eigenvalues ±√(j-s) with multiplicity p(s) - p(s-1) (from ker(D_s)), where p(-1) = 0 by convention.
• Total eigenvalue count equals p(j-1) + p(j), matching the number of vertices.

The multiplicity p(s) - p(s-1) equals dim(ker(D_s)) since U_s is injective and D_s is surjective (from DU - UD = I), giving dim(ker D_s) = dim ℝY_s - dim ℝY_{s-1}.

theorem YoungEigenvalues.p_mono (n : ℕ) : p n ≤ p (n + 1)

The number of partitions is nondecreasing: p(n) ≤ p(n + 1) for all n. This follows from the injectivity of the raising operator U, which gives an injection from partitions of n to partitions of n + 1 by adding a box to the first row. (Consequence of Lemma 8.2: U is injective since DU - UD = I.)

theorem YoungEigenvalues.p_le_p {a b : ℕ} (h : a ≤ b) : p a ≤ p b

Extended version of p_mono: p(a) ≤ p(b) whenever a ≤ b.

noncomputable def YoungEigenvalues.kerDimDiff (s : ℕ) : ℕ

The multiplicity of the eigenvalue pair ±√(j-s) in the spectrum of Y_{j-1,j}, equal to dim(ker D_s) = p(s) - p(s-1) with the convention p(-1) = 0. For s = j, this gives the multiplicity of eigenvalue 0: p(j) - p(j-1).

@[simp]

theorem YoungEigenvalues.kerDimDiff_zero : kerDimDiff 0 = p 0

kerDimDiff at 0 equals p(0), i.e., 1 (there is one partition of 0).

theorem YoungEigenvalues.kerDimDiff_pos {s : ℕ} (hs : 1 ≤ s) : kerDimDiff s = p s - p (s - 1)

kerDimDiff at a positive index is p(s) - p(s-1).

theorem YoungEigenvalues.kerDimDiff_sum_eq (n : ℕ) (hn : 1 ≤ n) : (Finset.range n).sum kerDimDiff = p (n - 1)

The telescoping sum: ∑_{s=0}^{n-1} kerDimDiff(s) = p(n-1) for n ≥ 1, or equivalently ∑_{s=0}^{j-1} dim(ker D_s) = p(j-1) — the total multiplicity contributed by the nonzero eigenvalues ±√(j-s).

Adjacency operator on two separate spaces

In the book, the adjacency matrix A of the bipartite graph Y_{j-1,j} acts on ℝY_{j-1} ⊕ ℝY_j, which are vector spaces of different dimensions p(j-1) and p(j). The operator U : ℝY_{j-1} → ℝY_j raises the rank and D : ℝY_j → ℝY_{j-1} lowers it.

We define adjOp₂ to faithfully model this: it acts on V₁ × V₂ where V₁ and V₂ may have different dimensions.

noncomputable def YoungEigenvalues.adjOp₂ {V₁ : Type u_2} {V₂ : Type u_3} [AddCommGroup V₁] [Module ℝ V₁] [AddCommGroup V₂] [Module ℝ V₂] (U : V₁ →ₗ[ℝ] V₂) (D : V₂ →ₗ[ℝ] V₁) : Module.End ℝ (V₁ × V₂)

The adjacency operator of the bipartite graph Y_{j-1,j}, acting on V₁ × V₂ where V₁ ≅ ℝY_{j-1} and V₂ ≅ ℝY_j are (potentially) different-dimensional spaces. Maps (a, b) ↦ (D(b), U(a)).

noncomputable def YoungEigenvalues.eigenspace_adjOp₂_equiv_DU {V₁ : Type u_2} {V₂ : Type u_3} [AddCommGroup V₁] [Module ℝ V₁] [AddCommGroup V₂] [Module ℝ V₂] [FiniteDimensional ℝ V₁] [FiniteDimensional ℝ V₂] (U : V₁ →ₗ[ℝ] V₂) (D : V₂ →ₗ[ℝ] V₁) (μ : ℝ) (hμ : μ ≠ 0) (s : ℝ) (hμs : μ * μ = s) : ↥((adjOp₂ U D).eigenspace μ) ≃ₗ[ℝ] ↥(Module.End.eigenspace (D ∘ₗ U) s)

For μ ≠ 0 with μ * μ = s, the eigenspace of adjOp₂ U D at eigenvalue μ is linearly isomorphic to the eigenspace of D ∘ U at eigenvalue s. This is the key reduction: eigenvectors (a, b) of adjOp₂ satisfy D b = μ a and U a = μ b, hence D(U a) = μ · D b = μ² a = s a.

Eigenspace shift lemmas for the commutation relation

From the commutation relation D∘U = I + U_prev∘D_prev (Lemma 8.2 at rank j-1), we derive that the eigenspace of D∘U at eigenvalue s equals the eigenspace of U_prev∘D_prev at eigenvalue s - 1. For s = 1 this gives ker(D_prev), and for s ≥ 2 we use the AB/BA eigenspace isomorphism to reduce to D_prev∘U_prev.

theorem YoungEigenvalues.eigenspace_id_add_eq {W : Type u_2} [AddCommGroup W] [Module ℝ W] (G : Module.End ℝ W) (s : ℝ) : (LinearMap.id + G).eigenspace s = G.eigenspace (s - 1)

If F = I + G (as endomorphisms on V₁), then the eigenspace of F at s equals the eigenspace of G at s - 1. This is because F(w) = s•w ↔ w + G(w) = s•w ↔ G(w) = (s-1)•w.

noncomputable def YoungEigenvalues.eigenspace_comp_comm_nonzero_equiv {W₁ : Type u_2} {W₂ : Type u_3} [AddCommGroup W₁] [Module ℝ W₁] [AddCommGroup W₂] [Module ℝ W₂] (A : W₁ →ₗ[ℝ] W₂) (B : W₂ →ₗ[ℝ] W₁) (μ : ℝ) (hμ : μ ≠ 0) : ↥(Module.End.eigenspace (B ∘ₗ A) μ) ≃ₗ[ℝ] ↥(Module.End.eigenspace (A ∘ₗ B) μ)

For nonzero eigenvalue μ, the eigenspaces of B∘A (on W₁) and A∘B (on W₂) are linearly isomorphic. If B(A(w)) = μ•w, then v := A(w) satisfies A(B(v)) = μ•v. Forward: w ↦ A(w), backward: v ↦ μ⁻¹ • B(v).

theorem YoungEigenvalues.DU_eigenspace_dim_from_commutation (j : ℕ) (hj : 2 ≤ j) {V₁ : Type u_2} {V₂ : Type u_3} [AddCommGroup V₁] [Module ℝ V₁] [AddCommGroup V₂] [Module ℝ V₂] [FiniteDimensional ℝ V₁] [FiniteDimensional ℝ V₂] (hdim1 : Module.finrank ℝ V₁ = p (j - 1)) (U : V₁ →ₗ[ℝ] V₂) (D : V₂ →ₗ[ℝ] V₁) {V₀ : Type u_4} [AddCommGroup V₀] [Module ℝ V₀] [FiniteDimensional ℝ V₀] (U_prev : V₀ →ₗ[ℝ] V₁) (D_prev : V₁ →ₗ[ℝ] V₀) (hcomm : ∀ (w : V₁), D (U w) = w + U_prev (D_prev w)) (hdim0 : Module.finrank ℝ V₀ = p (j - 2)) (hU_prev_inj : Function.Injective ⇑U_prev) (hD_prev_surj : Function.Surjective ⇑D_prev) (hDpUp_eig : ∀ (t : ℕ), 1 ≤ t → t ≤ j - 1 → Module.finrank ℝ ↥(Module.End.eigenspace (D_prev ∘ₗ U_prev) ↑t) = kerDimDiff (j - 1 - t)) (s : ℕ) : 1 ≤ s → s ≤ j → Module.finrank ℝ ↥(Module.End.eigenspace (D ∘ₗ U) ↑s) = kerDimDiff (j - s)

From the commutation relation D(U(w)) = w + U_prev(D_prev(w)) at rank j-1 (Lemma 8.2), the eigenspace dimensions of D∘U are derived as follows:

• The eigenspace of D∘U at s equals the eigenspace of U_prev∘D_prev at s-1.
• For s = 1: this is ker(U_prev ∘ D_prev) = ker(D_prev) (since U_prev is injective), with dimension p(j-1) - p(j-2) by rank-nullity.
• For s ≥ 2: the nonzero eigenspace of U_prev∘D_prev at s-1 is isomorphic to the eigenspace of D_prev∘U_prev at s-1, with dimension given by the inductive hypothesis hDpUp_eig.

theorem YoungEigenvalues.abstract_eigenvalue_multiplicities (j : ℕ) (hj : 2 ≤ j) (V₁ : Type u_2) (V₂ : Type u_3) [AddCommGroup V₁] [Module ℝ V₁] [AddCommGroup V₂] [Module ℝ V₂] [FiniteDimensional ℝ V₁] [FiniteDimensional ℝ V₂] (hdim1 : Module.finrank ℝ V₁ = p (j - 1)) (hdim2 : Module.finrank ℝ V₂ = p j) (U : V₁ →ₗ[ℝ] V₂) (D : V₂ →ₗ[ℝ] V₁) (hU_inj : Function.Injective ⇑U) (hD_surj : Function.Surjective ⇑D) {V₀ : Type u_4} [AddCommGroup V₀] [Module ℝ V₀] [FiniteDimensional ℝ V₀] (U_prev : V₀ →ₗ[ℝ] V₁) (D_prev : V₁ →ₗ[ℝ] V₀) (hcomm : ∀ (w : V₁), D (U w) = w + U_prev (D_prev w)) (hdim0 : Module.finrank ℝ V₀ = p (j - 2)) (hU_prev_inj : Function.Injective ⇑U_prev) (hD_prev_surj : Function.Surjective ⇑D_prev) (hDpUp_eig : ∀ (t : ℕ), 1 ≤ t → t ≤ j - 1 → Module.finrank ℝ ↥(Module.End.eigenspace (D_prev ∘ₗ U_prev) ↑t) = kerDimDiff (j - 1 - t)) : Module.finrank ℝ ↥((adjOp₂ U D).eigenspace 0) = p j - p (j - 1) ∧ (∀ (s : ℕ), 1 ≤ s → s ≤ j → Module.finrank ℝ ↥((adjOp₂ U D).eigenspace √↑s) = kerDimDiff (j - s)) ∧ (∀ (s : ℕ), 1 ≤ s → s ≤ j → Module.finrank ℝ ↥((adjOp₂ U D).eigenspace (-√↑s)) = kerDimDiff (j - s)) ∧ p j - p (j - 1) + 2 * (Finset.range j).sum kerDimDiff = p (j - 1) + p j

Theorem 8.8 (abstract form) (Stanley). Fix j ≥ 1. Let V₁, V₂ be ℝ-vector spaces of dimensions p(j-1) and p(j) respectively, with operators U : V₁ →ₗ[ℝ] V₂ (the raising operator U_{j-1}) and D : V₂ →ₗ[ℝ] V₁ (the lowering operator D_j).

The commutation relation (Lemma 8.2, Equation 41) at rank j-1 states: D_j ∘ U_{j-1} - U_{j-2} ∘ D_{j-1} = I_{j-1}, i.e., D(U(w)) = w + U_prev(D_prev(w)) for all w ∈ V₁, where D_prev = D_{j-1} : V₁ → V₀ and U_prev = U_{j-2} : V₀ → V₁ are operators through the previous-rank space V₀ ≅ ℝY_{j-2}.

From the commutation relation (applied at all ranks), U is injective and D is surjective (deduced from Lemma 8.2), giving dim(ker D) = dim V₂ - dim V₁ = p(j) - p(j-1).

The eigenspace dimensions of D∘U are derived from the commutation relation:

• D∘U = I + U_prev∘D_prev shifts eigenvalues by 1,
• For s = 1: eigenspace(D∘U, 1) = ker(D_prev), with dim = p(j-1) - p(j-2).
• For s ≥ 2: eigenspace(D∘U, s) ≅ eigenspace(D_prev∘U_prev, s-1) via the AB/BA nonzero eigenspace isomorphism, with dimension given by the inductive hypothesis hDpUp_eig at the previous level.

Then the adjacency operator A on V₁ × V₂ defined by A(a,b) = (D(b), U(a)) has eigenvalues:

• 0 with multiplicity p(j) - p(j-1) (eigenspace dimension);
• ±√s for 1 ≤ s ≤ j, each with multiplicity p(j-s) - p(j-s-1); and these account for all eigenvalues: the total multiplicity sums to p(j-1) + p(j) = dim(V₁ × V₂).

This is the abstract version; see young_lattice_eigenvalue_multiplicities for the concrete specialization to Young's lattice partition spaces.

Bridge from abstract operators to Young's lattice

@[reducible, inline]

abbrev YoungEigenvalues.PartitionSpace (j : ℕ) : Type

The concrete vector space ℝY_j of formal ℝ-linear combinations of partitions of j.

theorem YoungEigenvalues.finrank_partitionSpace (j : ℕ) : Module.finrank ℝ (PartitionSpace j) = p j

The dimension of PartitionSpace j equals p(j).

theorem YoungEigenvalues.leftInverse_of_comp_eq_id {R : Type u_2} [Semiring R] {V₁ : Type u_3} {V₂ : Type u_4} [AddCommMonoid V₁] [Module R V₁] [AddCommMonoid V₂] [Module R V₂] (U : V₁ →ₗ[R] V₂) (D : V₂ →ₗ[R] V₁) (hDU : D ∘ₗ U = LinearMap.id) : Function.LeftInverse ⇑D ⇑U

From D ∘ U = id, D is a left inverse of U.

theorem YoungEigenvalues.injective_of_comp_eq_id {R : Type u_2} [Semiring R] {V₁ : Type u_3} {V₂ : Type u_4} [AddCommMonoid V₁] [Module R V₁] [AddCommMonoid V₂] [Module R V₂] (U : V₁ →ₗ[R] V₂) (D : V₂ →ₗ[R] V₁) (hDU : D ∘ₗ U = LinearMap.id) : Function.Injective ⇑U

From D ∘ U = id, U is injective.

theorem YoungEigenvalues.surjective_of_comp_eq_id {R : Type u_2} [Semiring R] {V₁ : Type u_3} {V₂ : Type u_4} [AddCommMonoid V₁] [Module R V₁] [AddCommMonoid V₂] [Module R V₂] (U : V₁ →ₗ[R] V₂) (D : V₂ →ₗ[R] V₁) (hDU : D ∘ₗ U = LinearMap.id) : Function.Surjective ⇑D

From D ∘ U = id, D is surjective.

theorem YoungEigenvalues.young_lattice_eigenvalue_multiplicities (j : ℕ) (hj : 2 ≤ j) (U : PartitionSpace (j - 1) →ₗ[ℝ] PartitionSpace j) (D : PartitionSpace j →ₗ[ℝ] PartitionSpace (j - 1)) (hU_inj : Function.Injective ⇑U) (hD_surj : Function.Surjective ⇑D) (U_prev : PartitionSpace (j - 2) →ₗ[ℝ] PartitionSpace (j - 1)) (D_prev : PartitionSpace (j - 1) →ₗ[ℝ] PartitionSpace (j - 2)) (hcomm : ∀ (w : PartitionSpace (j - 1)), D (U w) = w + U_prev (D_prev w)) (hU_prev_inj : Function.Injective ⇑U_prev) (hD_prev_surj : Function.Surjective ⇑D_prev) (hDpUp_eig : ∀ (t : ℕ), 1 ≤ t → t ≤ j - 1 → Module.finrank ℝ ↥(Module.End.eigenspace (D_prev ∘ₗ U_prev) ↑t) = kerDimDiff (j - 1 - t)) : Module.finrank ℝ ↥((adjOp₂ U D).eigenspace 0) = p j - p (j - 1) ∧ (∀ (s : ℕ), 1 ≤ s → s ≤ j → Module.finrank ℝ ↥((adjOp₂ U D).eigenspace √↑s) = kerDimDiff (j - s)) ∧ (∀ (s : ℕ), 1 ≤ s → s ≤ j → Module.finrank ℝ ↥((adjOp₂ U D).eigenspace (-√↑s)) = kerDimDiff (j - s)) ∧ p j - p (j - 1) + 2 * (Finset.range j).sum kerDimDiff = p (j - 1) + p j

Theorem 8.8 specialized to Young's lattice PartitionSpace types, for j ≥ 2.

Closing the induction: Theorem 8.8 without the inductive hypothesis

structure YoungEigenvalues.YoungLatticeOps (i : ℕ) : Type

Bundled raising and lowering operators at level i of Young's lattice.

• U : PartitionSpace i →ₗ[ℝ] PartitionSpace (i + 1)
• D : PartitionSpace (i + 1) →ₗ[ℝ] PartitionSpace i
• hU_inj : Function.Injective ⇑self.U
• hD_surj : Function.Surjective ⇑self.D

structure YoungEigenvalues.YoungLatticeFamily : Type

A family of Young lattice operators at all levels, together with the commutation relation encoding Lemma 8.2 and D₁∘U₀ = Id at level 0.

• ops (i : ℕ) : YoungLatticeOps i
• hcomm (i : ℕ) (w : PartitionSpace (i + 1)) : (self.ops (i + 1)).D ((self.ops (i + 1)).U w) = w + (self.ops i).U ((self.ops i).D w)

  Commutation relation at level i + 1 (Lemma 8.2): D_{i+2}(U_{i+1}(w)) = w + U_i(D_i(w)) for w ∈ PartitionSpace (i + 1).

• hbase : (self.ops 0).D ∘ₗ (self.ops 0).U = LinearMap.id

  Base case (Lemma 8.2 at level 0): D₁ ∘ U₀ = Id on PartitionSpace 0. At level 0 there is no previous level, so the U_prev ∘ D_prev term vanishes.

theorem YoungEigenvalues.eigenspace_dim_of_id (F : YoungLatticeFamily) (s : ℕ) : 1 ≤ s → s ≤ 1 → Module.finrank ℝ ↥(Module.End.eigenspace ((F.ops 0).D ∘ₗ (F.ops 0).U) ↑s) = kerDimDiff (1 - s)

Helper: from DU = Id, eigenspace at s (for 1 ≤ s ≤ 1, so s = 1) has dimension kerDimDiff(1 - s). Since DU = Id, eigenspace at 1 = full space of dimension p(0), and kerDimDiff(0) = p(0).

theorem YoungEigenvalues.DU_eigenspace_dim_induction (F : YoungLatticeFamily) (k s : ℕ) : 1 ≤ s → s ≤ k + 2 → Module.finrank ℝ ↥(Module.End.eigenspace ((F.ops (k + 1)).D ∘ₗ (F.ops (k + 1)).U) ↑s) = kerDimDiff (k + 2 - s)

theorem YoungEigenvalues.DU_eigenspace_dim_all_levels (F : YoungLatticeFamily) (k s : ℕ) : 1 ≤ s → s ≤ k + 1 → Module.finrank ℝ ↥(Module.End.eigenspace ((F.ops k).D ∘ₗ (F.ops k).U) ↑s) = kerDimDiff (k + 1 - s)

theorem YoungEigenvalues.young_lattice_eigenvalues_closed (F : YoungLatticeFamily) (j : ℕ) (hj : 1 ≤ j) : Module.finrank ℝ ↥((adjOp₂ (F.ops (j - 1)).U (F.ops (j - 1)).D).eigenspace 0) = p j - p (j - 1) ∧ (∀ (s : ℕ), 1 ≤ s → s ≤ j → Module.finrank ℝ ↥((adjOp₂ (F.ops (j - 1)).U (F.ops (j - 1)).D).eigenspace √↑s) = kerDimDiff (j - s)) ∧ (∀ (s : ℕ), 1 ≤ s → s ≤ j → Module.finrank ℝ ↥((adjOp₂ (F.ops (j - 1)).U (F.ops (j - 1)).D).eigenspace (-√↑s)) = kerDimDiff (j - s)) ∧ p j - p (j - 1) + 2 * (Finset.range j).sum kerDimDiff = p (j - 1) + p j

Theorem 8.8 (closed form).