The quantum Clebsch–Gordan decomposition

At a generic parameter q, the tensor product of two signed ladder modules decomposes as

L_m^ε ⊗ L_n^δ ≃ ⊕_(j = 0)^(min m n) L_(m + n - 2j)^(εδ),

where U_q(sl₂) acts on the tensor product through the coproduct ΔE = E ⊗ 1 + K ⊗ E, ΔF = F ⊗ K⁻¹ + 1 ⊗ F, ΔK = K ⊗ K.

The j-th summand is generated by the explicit highest vector w_j = ∑_(i = 0)^j α_i v_i ⊗ v_(j - i), whose coefficients satisfy α₀ = 1 and α_(i+1) = -δ q^(m - 2i) [n - j + i + 1]_q / [m - i]_q α_i. This recurrence is exactly the condition E w_j = 0. The vector w_j has weight εδ q^(m + n - 2j), so the universal property of the ladder modules (LadderModule.lift) turns it into an injective module map L_(m + n - 2j)^(εδ) → L_m^ε ⊗ L_n^δ sending v_k to F^k w_j / ([1]_q ⋯ [k]_q). The images of these maps lie in distinct Casimir blocks, hence are independent, and their dimensions add up to (m + 1)(n + 1).

Main definitions

• TauCeti.UqSl2.clebschGordanCoeff: the coefficients α_i.
• TauCeti.UqSl2.clebschGordanVector: the highest vector w_j in L_m^ε ⊗ L_n^δ.
• TauCeti.UqSl2.clebschGordanInclusion: the module map L_(m + n - 2j)^(εδ) → L_m^ε ⊗ L_n^δ sending v₀ to w_j.
• TauCeti.UqSl2.clebschGordanEquiv: the Clebsch–Gordan isomorphism.
• TauCeti.UqSl2.IsClebschGordanChannel, TauCeti.UqSl2.IsClebschGordanChannel.index: admissible highest weights k = m + n - 2j in L_m ⊗ L_n and their summand index (m + n - k) / 2.

Main results

• TauCeti.UqSl2.e_smul_clebschGordanVector: E w_j = 0.
• TauCeti.UqSl2.clebschGordanVector_mem_weightSpace: K w_j = εδ q^(m + n - 2j) w_j.
• TauCeti.UqSl2.clebschGordanVector_ne_zero: w_j ≠ 0 for j ≤ n.
• TauCeti.UqSl2.clebschGordanInclusion_zero_left_vec, TauCeti.UqSl2.clebschGordanInclusion_zero_right_vec: explicit images of v_k when m = 0 or n = 0.
• TauCeti.UqSl2.iSupIndep_range_clebschGordanInclusion: the summands are independent.
• TauCeti.UqSl2.clebschGordanEquiv_apply, TauCeti.UqSl2.clebschGordanEquiv_single: the isomorphism is the sum of the inclusions.
• TauCeti.UqSl2.isClebschGordanChannel_iff, TauCeti.UqSl2.sum_fin_channel_eq_sum_range: triangle-and-parity characterization and channel-to-weight sum reindexing.

References

• A. Virelizier, Quantum groups, Section 4.1, for the fusion rule of the finite-dimensional type-1 modules.
• C. Kassel, Quantum Groups, Graduate Texts in Mathematics 155, Chapter VII, for the Clebsch–Gordan formula for the tensor products of the modules V_(ε,n).

def TauCeti.UqSl2.clebschGordanCoeff (q : ℂ) (m n : ℕ) (δ : ℤˣ) (j : ℕ) : ℕ → ℂ

The coefficients α_i of the Clebsch–Gordan vector ∑_i α_i v_i ⊗ v_(j - i) in L_m^ε ⊗ L_n^δ, defined for all q, m, n, j and i by α₀ = 1 and α_(i+1) = -δ q^(m - 2i) [n - j + i + 1]_q / [m - i]_q α_i (with Lean's convention x / 0 = 0). They do not depend on ε. At a generic parameter and for j ≤ m, the denominators [m - i]_q with i < j are nonzero and the resulting vector is a highest vector (see TauCeti.UqSl2.e_smul_clebschGordanVector).

@[simp]

theorem TauCeti.UqSl2.clebschGordanCoeff_zero {q : ℂ} (m n : ℕ) (δ : ℤˣ) (j : ℕ) : clebschGordanCoeff q m n δ j 0 = 1

The leading Clebsch–Gordan coefficient is normalized to α₀ = 1.

theorem TauCeti.UqSl2.clebschGordanCoeff_succ {q : ℂ} (m n : ℕ) (δ : ℤˣ) (j i : ℕ) : clebschGordanCoeff q m n δ j (i + 1) = -↑↑δ * q ^ (↑m - 2 * ↑i) * quantumInteger q (↑n - ↑j + ↑i + 1) / quantumInteger q (↑m - ↑i) * clebschGordanCoeff q m n δ j i

The defining recurrence of the Clebsch–Gordan coefficients.

theorem TauCeti.UqSl2.clebschGordanCoeff_mul_sign {q : ℂ} (m n : ℕ) (δ ζ : ℤˣ) (j i : ℕ) : clebschGordanCoeff q m n (δ * ζ) j i = ↑↑ζ ^ i * clebschGordanCoeff q m n δ j i

Multiplying the right sign δ by ζ scales the i-th Clebsch–Gordan coefficient by ζ^i.

theorem TauCeti.UqSl2.quantumInteger_mul_clebschGordanCoeff_succ {q : ℂ} (hq : IsGenericQuantumParameter q) {m n : ℕ} {δ : ℤˣ} {j i : ℕ} (hi : i < m) : quantumInteger q (↑m - ↑i) * clebschGordanCoeff q m n δ j (i + 1) = -↑↑δ * q ^ (↑m - 2 * ↑i) * quantumInteger q (↑n - ↑j + ↑i + 1) * clebschGordanCoeff q m n δ j i

At a generic parameter and for i < m, the Clebsch–Gordan recurrence with its denominator cleared: [m - i]_q α_(i+1) = -δ q^(m - 2i) [n - j + i + 1]_q α_i.

noncomputable def TauCeti.UqSl2.clebschGordanVector (q : ℂ) [Fact (q ≠ 0)] (m : ℕ) (ε : ℤˣ) (n : ℕ) (δ : ℤˣ) (j : ℕ) : BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ)

The Clebsch–Gordan vector w_j = ∑_(i = 0)^j α_i v_i ⊗ v_(j - i) in L_m^ε ⊗ L_n^δ, with the coefficients α_i = clebschGordanCoeff q m n δ j i, defined for every j. It always has weight εδ q^(m + n - 2j), and it is nonzero for j ≤ n. At a generic parameter and for j ≤ m it is moreover killed by E, so for j ≤ min m n it is a nonzero highest vector.

theorem TauCeti.UqSl2.clebschGordanVector_def {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (j : ℕ) : clebschGordanVector q m ε n δ j = ∑ i ∈ Finset.range (j + 1), clebschGordanCoeff q m n δ j i • BialgebraModule.tmul ℂ (UqSl2 q) (LadderModule.vec q m ε ↑i) (LadderModule.vec q n δ (↑j - ↑i))

The defining formula w_j = ∑_(i = 0)^j α_i v_i ⊗ v_(j - i) of the Clebsch–Gordan vector.

@[simp]

theorem TauCeti.UqSl2.clebschGordanVector_zero {q : ℂ} [Fact (q ≠ 0)] (m : ℕ) (ε : ℤˣ) (n : ℕ) (δ : ℤˣ) : clebschGordanVector q m ε n δ 0 = BialgebraModule.tmul ℂ (UqSl2 q) (LadderModule.vec q m ε 0) (LadderModule.vec q n δ 0)

The leading Clebsch–Gordan highest vector w₀ is the pure tensor v₀ ⊗ v₀.

theorem TauCeti.UqSl2.assoc_clebschGordanVector_tmul {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} {P : Type u_1} [AddCommMonoid P] [Module ℂ P] [Module (UqSl2 q) P] [IsScalarTower ℂ (UqSl2 q) P] (j : ℕ) (x : P) : (BialgebraModule.assoc ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ) P) (BialgebraModule.tmul ℂ (UqSl2 q) (clebschGordanVector q m ε n δ j) x) = ∑ i ∈ Finset.range (j + 1), clebschGordanCoeff q m n δ j i • BialgebraModule.tmul ℂ (UqSl2 q) (LadderModule.vec q m ε ↑i) (BialgebraModule.tmul ℂ (UqSl2 q) (LadderModule.vec q n δ (↑j - ↑i)) x)

Reassociating w_j ⊗ x expands it into pure triple tensors v_i ⊗ (v_(j - i) ⊗ x).

theorem TauCeti.UqSl2.assoc_symm_tmul_clebschGordanVector {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} {M : Type u_1} [AddCommMonoid M] [Module ℂ M] [Module (UqSl2 q) M] [IsScalarTower ℂ (UqSl2 q) M] (x : M) (j : ℕ) : (BialgebraModule.assoc ℂ (UqSl2 q) M (LadderModule q m ε) (LadderModule q n δ)).symm (BialgebraModule.tmul ℂ (UqSl2 q) x (clebschGordanVector q m ε n δ j)) = ∑ i ∈ Finset.range (j + 1), clebschGordanCoeff q m n δ j i • BialgebraModule.tmul ℂ (UqSl2 q) (BialgebraModule.tmul ℂ (UqSl2 q) x (LadderModule.vec q m ε ↑i)) (LadderModule.vec q n δ (↑j - ↑i))

Inverse-reassociating x ⊗ w_j expands it into pure triple tensors (x ⊗ v_i) ⊗ v_(j - i).

theorem TauCeti.UqSl2.clebschGordanVector_mem_weightSpace {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (j : ℕ) : clebschGordanVector q m ε n δ j ∈ weightSpace q (BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ)) (↑↑(ε * δ) * q ^ (↑m + ↑n - 2 * ↑j))

The Clebsch–Gordan vector w_j has weight εδ q^(m + n - 2j).

theorem TauCeti.UqSl2.e_smul_clebschGordanVector {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) {j : ℕ} (hj : j ≤ m) : e q • clebschGordanVector q m ε n δ j = 0

For j ≤ m, the Clebsch–Gordan vector w_j is a highest-weight vector: E w_j = 0.

theorem TauCeti.UqSl2.clebschGordanVector_ne_zero {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} {j : ℕ} (hj : j ≤ n) : clebschGordanVector q m ε n δ j ≠ 0

For j ≤ n, the Clebsch–Gordan vector w_j is nonzero: its coefficient on v₀ ⊗ v_j is α₀ = 1.

theorem TauCeti.UqSl2.f_pow_smul_clebschGordanVector {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) {j : ℕ} (hjm : j ≤ m) (hjn : j ≤ n) : f q ^ (m + n - 2 * j + 1) • clebschGordanVector q m ε n δ j = 0

For j ≤ min m n, the lowering string of w_j vanishes after m + n - 2j + 1 steps.

noncomputable def TauCeti.UqSl2.clebschGordanInclusion {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) (j : Fin (min m n + 1)) : LadderModule q (m + n - 2 * ↑j) (ε * δ) →ₗ[UqSl2 q] BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ)

For j ≤ min m n, the Clebsch–Gordan inclusion L_(m + n - 2j)^(εδ) → L_m^ε ⊗ L_n^δ: the module map sending v₀ to the highest vector w_j, and v_k to F^k w_j / ([1]_q ⋯ [k]_q).

@[simp]

theorem TauCeti.UqSl2.clebschGordanInclusion_vec_zero {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) (j : Fin (min m n + 1)) : (clebschGordanInclusion hq j) (LadderModule.vec q (m + n - 2 * ↑j) (ε * δ) 0) = clebschGordanVector q m ε n δ ↑j

The Clebsch–Gordan inclusion sends v₀ to the highest vector w_j.

theorem TauCeti.UqSl2.clebschGordanInclusion_vec {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) (j : Fin (min m n + 1)) (k : ℕ) : (clebschGordanInclusion hq j) (LadderModule.vec q (m + n - 2 * ↑j) (ε * δ) ↑k) = (quantumFactorial q k)⁻¹ • f q ^ k • clebschGordanVector q m ε n δ ↑j

The Clebsch–Gordan inclusion sends v_k to the normalized lowering string F^k w_j / ([1]_q ⋯ [k]_q).

theorem TauCeti.UqSl2.clebschGordanInclusion_zero_left_vec {q : ℂ} [Fact (q ≠ 0)] {n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) (k : ℕ) : (clebschGordanInclusion hq 0) (LadderModule.vec q (0 + n - 2 * ↑0) (ε * δ) ↑k) = BialgebraModule.tmul ℂ (UqSl2 q) (LadderModule.vec q 0 ε 0) (LadderModule.vec q n δ ↑k)

Tensoring with L_0^ε on the left embeds v_k as v₀ ⊗ v_k.

theorem TauCeti.UqSl2.clebschGordanInclusion_zero_right_vec {q : ℂ} [Fact (q ≠ 0)] {m : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) (k : ℕ) : (clebschGordanInclusion hq 0) (LadderModule.vec q (m + 0 - 2 * ↑0) (ε * δ) ↑k) = ↑↑δ ^ k • BialgebraModule.tmul ℂ (UqSl2 q) (LadderModule.vec q m ε ↑k) (LadderModule.vec q 0 δ 0)

Tensoring with L_0^δ on the right embeds v_k as δ^k (v_k ⊗ v₀).

theorem TauCeti.UqSl2.clebschGordanInclusion_injective {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) (j : Fin (min m n + 1)) : Function.Injective ⇑(clebschGordanInclusion hq j)

The Clebsch–Gordan inclusions are injective.

theorem TauCeti.UqSl2.casimir_smul_clebschGordanInclusion {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) (j : Fin (min m n + 1)) (x : LadderModule q (m + n - 2 * ↑j) (ε * δ)) : casimir q • (clebschGordanInclusion hq j) x = casimirScalar q (↑↑(ε * δ) * q ^ (m + n - 2 * ↑j)) • (clebschGordanInclusion hq j) x

The Casimir acts on the included channel by its signed highest-weight scalar.

theorem TauCeti.UqSl2.clebschGordan_casimirScalar_injective {q : ℂ} {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) : Function.Injective fun (j : Fin (min m n + 1)) => casimirScalar q (↑↑(ε * δ) * q ^ (m + n - 2 * ↑j))

The Casimir scalars of the Clebsch–Gordan channels are distinct.

theorem TauCeti.UqSl2.range_clebschGordanInclusion_le_casimirBlock {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) (j : Fin (min m n + 1)) : (clebschGordanInclusion hq j).range ≤ casimirBlock q (BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ)) (casimirScalar q (↑↑(ε * δ) * q ^ (m + n - 2 * ↑j)))

The image of the j-th Clebsch–Gordan inclusion lies in the Casimir block of its highest weight εδ q^(m + n - 2j).

theorem TauCeti.UqSl2.iSupIndep_range_clebschGordanInclusion {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) : iSupIndep fun (j : Fin (min m n + 1)) => (clebschGordanInclusion hq j).range

The images of the Clebsch–Gordan inclusions are independent.

noncomputable def TauCeti.UqSl2.clebschGordanEquiv {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) : ((j : Fin (min m n + 1)) → LadderModule q (m + n - 2 * ↑j) (ε * δ)) ≃ₗ[UqSl2 q] BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ)

The quantum Clebsch–Gordan decomposition: at a generic parameter, L_m^ε ⊗ L_n^δ ≃ ⊕_(j = 0)^(min m n) L_(m + n - 2j)^(εδ) as UqSl2 q-modules, with the j-th summand embedded by clebschGordanInclusion.

theorem TauCeti.UqSl2.clebschGordanEquiv_apply {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) (x : (j : Fin (min m n + 1)) → LadderModule q (m + n - 2 * ↑j) (ε * δ)) : (clebschGordanEquiv hq) x = ∑ j : Fin (min m n + 1), (clebschGordanInclusion hq j) (x j)

The Clebsch–Gordan isomorphism is the sum of the Clebsch–Gordan inclusions.

@[simp]

theorem TauCeti.UqSl2.clebschGordanEquiv_single {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) (j : Fin (min m n + 1)) (x : LadderModule q (m + n - 2 * ↑j) (ε * δ)) : (clebschGordanEquiv hq) (Pi.single j x) = (clebschGordanInclusion hq j) x

The Clebsch–Gordan isomorphism restricts to the j-th inclusion on the j-th summand.

@[simp]

theorem TauCeti.UqSl2.clebschGordanEquiv_comp_single {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) (j : Fin (min m n + 1)) : ↑(clebschGordanEquiv hq) ∘ₗ LinearMap.single (UqSl2 q) (fun (j : Fin (min m n + 1)) => LadderModule q (m + n - 2 * ↑j) (ε * δ)) j = clebschGordanInclusion hq j

Composing the Clebsch–Gordan isomorphism with a coordinate inclusion gives the corresponding normalized Clebsch–Gordan inclusion.

Admissible Clebsch–Gordan channels

def TauCeti.UqSl2.IsClebschGordanChannel (m n k : ℕ) : Prop

IsClebschGordanChannel m n k holds when L_k occurs in the binary Clebsch–Gordan decomposition of L_m ⊗ L_n, i.e., k = m + n - 2j for some j ≤ min m n.

theorem TauCeti.UqSl2.isClebschGordanChannel_def {m n k : ℕ} : IsClebschGordanChannel m n k ↔ ∃ (j : Fin (min m n + 1)), m + n - 2 * ↑j = k

Definitional characterization of IsClebschGordanChannel.

@[instance_reducible]

instance TauCeti.UqSl2.instDecidablePredNatIsClebschGordanChannel (m n : ℕ) : DecidablePred (IsClebschGordanChannel m n)

theorem TauCeti.UqSl2.IsClebschGordanChannel.le_add {m n k : ℕ} (h : IsClebschGordanChannel m n k) : k ≤ m + n

Every Clebsch–Gordan channel of L_m ⊗ L_n has highest weight at most m + n.

theorem TauCeti.UqSl2.isClebschGordanChannel_iff {m n k : ℕ} : IsClebschGordanChannel m n k ↔ k ≤ m + n ∧ m ≤ n + k ∧ n ≤ m + k ∧ Even (m + n - k)

Triangle and parity characterization of admissible binary Clebsch–Gordan channels.

def TauCeti.UqSl2.IsClebschGordanChannel.index {m n k : ℕ} (h : IsClebschGordanChannel m n k) : Fin (min m n + 1)

The unique summand index j : Fin (min m n + 1) witnessing k = m + n - 2j, computed explicitly as (m + n - k) / 2.

theorem TauCeti.UqSl2.IsClebschGordanChannel.val_index {m n k : ℕ} (h : IsClebschGordanChannel m n k) : ↑h.index = (m + n - k) / 2

The underlying natural number of h.index is (m + n - k) / 2.

@[simp]

theorem TauCeti.UqSl2.IsClebschGordanChannel.sub_two_mul_index {m n k : ℕ} (h : IsClebschGordanChannel m n k) : m + n - 2 * ↑h.index = k

The constructive index of an admissible channel recovers its highest weight k.

theorem TauCeti.UqSl2.IsClebschGordanChannel.index_eq_of_eq {m n k : ℕ} (h : IsClebschGordanChannel m n k) {j : Fin (min m n + 1)} (hj : m + n - 2 * ↑j = k) : h.index = j

Uniqueness of the Clebsch–Gordan summand index for a given channel weight k.

@[simp]

theorem TauCeti.UqSl2.IsClebschGordanChannel.index_eq_iff {m n k : ℕ} (h : IsClebschGordanChannel m n k) (j : Fin (min m n + 1)) : h.index = j ↔ m + n - 2 * ↑j = k

h.index = j holds exactly when m + n - 2j = k.

theorem TauCeti.UqSl2.isClebschGordanChannel_sub_two_mul {m n : ℕ} (j : Fin (min m n + 1)) : IsClebschGordanChannel m n (m + n - 2 * ↑j)

Every summand index j : Fin (min m n + 1) gives an admissible Clebsch–Gordan channel.

@[simp]

theorem TauCeti.UqSl2.IsClebschGordanChannel.index_sub_two_mul {m n : ℕ} (j : Fin (min m n + 1)) : ⋯.index = j

The constructive index of m + n - 2j is j.

theorem TauCeti.UqSl2.isClebschGordanChannel_add (m n : ℕ) : IsClebschGordanChannel m n (m + n)

The leading channel m + n (j = 0) is always admissible.

@[simp]

theorem TauCeti.UqSl2.isClebschGordanChannel_zero_left {n k : ℕ} : IsClebschGordanChannel 0 n k ↔ k = n

Tensoring with L_0 on the left has n as its unique admissible channel.

@[simp]

theorem TauCeti.UqSl2.isClebschGordanChannel_zero_right {m k : ℕ} : IsClebschGordanChannel m 0 k ↔ k = m

Tensoring with L_0 on the right has m as its unique admissible channel.

theorem TauCeti.UqSl2.sum_fin_channel_eq_sum_range {M : Type u_1} [AddCommMonoid M] (m n : ℕ) (g : ℕ → M) (hg : ∀ (w : ℕ), ¬IsClebschGordanChannel m n w → g w = 0) : ∑ i : Fin (min m n + 1), g (m + n - 2 * ↑i) = ∑ w ∈ Finset.range (m + n + 1), g w

Reindexing a sum over channel indices i : Fin (min m n + 1) as a sum over weights w ∈ Finset.range (m + n + 1) when g vanishes outside admissible channels.