The Clebsch-Gordan rule for sl₂ #
Over a field of characteristic zero the tensor product of two standard irreducible
sl (Fin 2) K-modules decomposes as
V(m) ⊗ V(n) ≅ V(m + n) ⊕ V(m + n - 2) ⊕ ⋯ ⊕ V(m + n - 2 min(m, n)),
each summand occurring once. This file proves it, in the form used elsewhere for sl₂
decompositions (TauCeti.Sl2Std.exists_isInternal_lieModuleEquiv): a family of Lie submodules
indexed by Fin (min m n + 1) which is an internal direct sum
(TauCeti.Sl2Std.isInternal_cgSummand) and whose k-th member is a copy of V(m + n - 2k)
(TauCeti.Sl2Std.nonempty_lieModuleEquiv_cgSummand).
The construction #
The summands are not obtained abstractly: the highest weight vector of each is written down. With
vᵢ and uⱼ the coordinate vectors of V(m) and V(n),
w_k = ∑_{j ≤ k} (-1)ʲ C(k, j) • (v_{k-j} ⊗ u_j) (TauCeti.Sl2Std.cgVector).
The Cartan element acts on v_a ⊗ u_b by (m - 2a) + (n - 2b), which is m + n - 2k all along
the antidiagonal a + b = k, so w_k is a weight vector of weight m + n - 2k. Raising sends the
antidiagonal a + b = k to the antidiagonal a + b = k - 1, and the coefficient of
v_{k-1-i} ⊗ u_i in e · w_k works out to
(-1)ⁱ (C(k, i)(k - i) - C(k, i+1)(i+1)),
which vanishes by Nat.choose_succ_right_eq. So w_k is a primitive vector;
TauCeti.isIrreducible_lieSpan_singleton proves the Lie submodule it generates is irreducible, and
TauCeti.Sl2Std.nonempty_lieModuleEquiv_lieSpan_singleton applies the classification to identify it
with V(m + n - 2k).
The summands are independent because the Casimir operator separates them: it acts on the k-th by
the scalar p(p + 2)/2 with p = m + n - 2k, and those scalars are pairwise distinct, so the
summands lie in distinct eigenspaces of a single endomorphism. Their dimensions then add up to
(m + 1)(n + 1) = dim (V(m) ⊗ V(n)), which upgrades independence to a decomposition of the whole
tensor product.
Main definitions #
TauCeti.Sl2Std.cgVector: the Clebsch-Gordan highest weight vectorsw_k.TauCeti.Sl2Std.cgSummand: the Lie submodule ofV(m) ⊗ V(n)generated byw_k.
Main results #
TauCeti.Sl2Std.hasPrimitiveVectorWith_cgVector:w_kis a primitive vector of weightm + n - 2k.TauCeti.Sl2Std.nonempty_lieModuleEquiv_cgSummand: thek-th summand is a copy ofV(m + n - 2k).TauCeti.Sl2Std.isInternal_cgSummand: the Clebsch-Gordan rule, the summands are an internal direct sum decomposition ofV(m) ⊗ V(n).
References #
This is the Clebsch-Gordan item of Layer 0 of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md.
The Clebsch-Gordan highest weight vectors #
The k-th Clebsch-Gordan highest weight vector of V(m) ⊗ V(n),
w_k = ∑_{j ≤ k} (-1)ʲ C(k, j) • (v_{k-j} ⊗ u_j). It is a primitive vector of weight
m + n - 2k whenever k ≤ min m n (TauCeti.Sl2Std.hasPrimitiveVectorWith_cgVector).
Unlike TauCeti.Sl2Std.cgSummand, this definition is @[expose]d: the explicit sum is the
content of the vector, so consumers should be able to compute with it directly rather than through
a restatement of the definition.
Equations
- TauCeti.Sl2Std.cgVector K m n k = ∑ j ∈ Finset.range (k + 1), ((-1) ^ j * ↑(k.choose j)) • TauCeti.Sl2Std.basisVector K m (k - j) ⊗ₜ[K] TauCeti.Sl2Std.basisVector K n j
Instances For
The Cartan element acts on the k-th Clebsch-Gordan vector by m + n - 2k: every pure tensor
in the defining sum lies on the antidiagonal a + b = k, where the two Cartan eigenvalues add up
to that scalar.
The raising element kills the k-th Clebsch-Gordan vector. Raising moves the antidiagonal
a + b = k to a + b = k - 1, and the two contributions to the coefficient of
v_{k-1-i} ⊗ u_i cancel by Nat.choose_succ_right_eq.
The k-th Clebsch-Gordan vector is nonzero: the coordinate of v_k ⊗ u_0 in it is 1, no
other term of the defining sum contributing to that coordinate.
The Clebsch-Gordan vectors are primitive vectors. For k ≤ min m n the vector w_k is a
nonzero weight vector of weight m + n - 2k killed by the raising element, so the general theory
applies to it.
The generated summands #
The k-th Clebsch-Gordan summand of V(m) ⊗ V(n): the Lie submodule generated by the
primitive vector TauCeti.Sl2Std.cgVector. Over a field of characteristic zero it is a copy of
V(m + n - 2k) (TauCeti.Sl2Std.nonempty_lieModuleEquiv_cgSummand).
Equations
- TauCeti.Sl2Std.cgSummand K m n k = LieSubmodule.lieSpan K ↥(LieAlgebra.SpecialLinear.sl (Fin 2) K) {TauCeti.Sl2Std.cgVector K m n ↑k}
Instances For
A Clebsch-Gordan summand lies in a Lie submodule exactly when its primitive vector does.
The decomposition #
The Clebsch-Gordan rule. The submodules TauCeti.Sl2Std.cgSummand, one for each
k ≤ min m n, are an internal direct sum decomposition of V(m) ⊗ V(n); together with
TauCeti.Sl2Std.nonempty_lieModuleEquiv_cgSummand this is
V(m) ⊗ V(n) ≅ ⨁_{k ≤ min m n} V(m + n - 2k).