Quantum 6j change-of-decomposition matrices

At a generic parameter q, indexing the triple-product recoupling scalars recouplingCoeff and invRecouplingCoeff on L_m^ε ⊗ L_n^δ ⊗ L_p^ζ by intermediate highest weights u and v at fixed total highest weight k yields the six-weight change-of-decomposition (F-matrix) functions sixJ and invSixJ (extended by 0 outside admissible Clebsch–Gordan channels) and the two-sided inverse matrices sixJMatrix and invSixJMatrix.

Here sixJ is the recoupling entry in the unnormalized α₀ = 1 highest-weight convention of clebschGordanInclusion (so its value depends on that basis normalization and on the module signs ε, δ, ζ, as in sixJ_zero_right), rather than the Racah/Kirillov–Reshetikhin-normalized, tetrahedrally symmetric 6j symbol.

• TauCeti.UqSl2.LeftSixJChannel, RightSixJChannel: admissible triple-product channels.
• TauCeti.UqSl2.sixJ, invSixJ, sixJMatrix, invSixJMatrix: α₀ = 1 change-of-decomposition (F-matrix) scalars and matrices.
• TauCeti.UqSl2.invSixJMatrix_mul_sixJMatrix, sixJMatrix_mul_invSixJMatrix: matrix inverses.
• TauCeti.UqSl2.sixJ_add_add, TauCeti.UqSl2.sixJ_zero_left, TauCeti.UqSl2.sixJ_zero_right: explicit boundary values.

References

• C. Kassel, Quantum Groups, Graduate Texts in Mathematics 155, Chapters VII and XII.
• A. N. Kirillov and N. Yu. Reshetikhin, Representations of the algebra U_q(sl(2)), q-orthogonal polynomials and invariants of links, World Scientific, 1989, pp. 285--339 (for quantum recoupling and 6j theory, up to basis rescaling).

Admissible triple-product channels

@[reducible, inline]

abbrev TauCeti.UqSl2.LeftSixJChannel (m n p k : ℕ) : Type

Admissible left intermediate highest weights u in (L_m ⊗ L_n) ⊗ L_p coupling to k.

@[reducible, inline]

abbrev TauCeti.UqSl2.RightSixJChannel (m n p k : ℕ) : Type

Admissible right intermediate highest weights v in L_m ⊗ (L_n ⊗ L_p) coupling to k.

@[instance_reducible]

instance TauCeti.UqSl2.instFintypeLeftSixJChannel (m n p k : ℕ) : Fintype (LeftSixJChannel m n p k)

@[instance_reducible]

instance TauCeti.UqSl2.instFintypeRightSixJChannel (m n p k : ℕ) : Fintype (RightSixJChannel m n p k)

Six-weight change-of-decomposition scalars and matrices

noncomputable def TauCeti.UqSl2.sixJ {q : ℂ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) (m n p k u v : ℕ) : ℂ

Six-weight change-of-decomposition (F-matrix) entry for L_m^ε ⊗ L_n^δ ⊗ L_p^ζ at total highest weight k in the α₀ = 1 normalization of clebschGordanInclusion, from left intermediate channel u to right intermediate channel v (extended by 0 outside admissible channels). Unlike the Racah/Kirillov–Reshetikhin symbol, it is not rescaled to tetrahedral symmetry and depends on ε, δ, ζ.

noncomputable def TauCeti.UqSl2.invSixJ {q : ℂ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) (m n p k v u : ℕ) : ℂ

Inverse six-weight change-of-decomposition (F-matrix) entry for L_m^ε ⊗ L_n^δ ⊗ L_p^ζ at total highest weight k in the α₀ = 1 normalization of clebschGordanInclusion, from right channel v to left channel u (extended by 0 outside admissible channels).

theorem TauCeti.UqSl2.sixJ_eq_recouplingCoeff {q : ℂ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) {m n p k u v : ℕ} {i : Fin (min m n + 1)} {j : Fin (min (m + n - 2 * ↑i) p + 1)} {r : Fin (min n p + 1)} {s : Fin (min m (n + p - 2 * ↑r) + 1)} (hu : m + n - 2 * ↑i = u) (hk : m + n - 2 * ↑i + p - 2 * ↑j = k) (hv : n + p - 2 * ↑r = v) (hk' : m + (n + p - 2 * ↑r) - 2 * ↑s = k) : sixJ hq ε δ ζ m n p k u v = recouplingCoeff hq ε δ ζ i j r s

On any left channel (i, j) and right channel (r, s) with intermediate weights u, v and common total weight k, sixJ equals recouplingCoeff hq ε δ ζ i j r s.

theorem TauCeti.UqSl2.invSixJ_eq_invRecouplingCoeff {q : ℂ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) {m n p k v u : ℕ} {r : Fin (min n p + 1)} {s : Fin (min m (n + p - 2 * ↑r) + 1)} {i : Fin (min m n + 1)} {j : Fin (min (m + n - 2 * ↑i) p + 1)} (hv : n + p - 2 * ↑r = v) (hk : m + (n + p - 2 * ↑r) - 2 * ↑s = k) (hu : m + n - 2 * ↑i = u) (hk' : m + n - 2 * ↑i + p - 2 * ↑j = k) : invSixJ hq ε δ ζ m n p k v u = invRecouplingCoeff hq ε δ ζ r s i j

On any right channel (r, s) and left channel (i, j) with intermediate weights v, u and common total weight k, invSixJ equals invRecouplingCoeff hq ε δ ζ r s i j.

@[simp]

theorem TauCeti.UqSl2.sixJ_eq_zero_of_not {q : ℂ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) {m n p k u v : ℕ} (h : ¬((IsClebschGordanChannel m n u ∧ IsClebschGordanChannel u p k) ∧ IsClebschGordanChannel n p v ∧ IsClebschGordanChannel m v k)) : sixJ hq ε δ ζ m n p k u v = 0

sixJ vanishes when any of its four binary channel conditions fails.

@[simp]

theorem TauCeti.UqSl2.invSixJ_eq_zero_of_not {q : ℂ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) {m n p k v u : ℕ} (h : ¬((IsClebschGordanChannel n p v ∧ IsClebschGordanChannel m v k) ∧ IsClebschGordanChannel m n u ∧ IsClebschGordanChannel u p k)) : invSixJ hq ε δ ζ m n p k v u = 0

invSixJ vanishes when any of its four binary channel conditions fails.

theorem TauCeti.UqSl2.recouplingCoeff_eq_ite {q : ℂ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) {m n p : ℕ} (i : Fin (min m n + 1)) (j : Fin (min (m + n - 2 * ↑i) p + 1)) (r : Fin (min n p + 1)) (s : Fin (min m (n + p - 2 * ↑r) + 1)) : recouplingCoeff hq ε δ ζ i j r s = if m + n - 2 * ↑i + p - 2 * ↑j = m + (n + p - 2 * ↑r) - 2 * ↑s then sixJ hq ε δ ζ m n p (m + n - 2 * ↑i + p - 2 * ↑j) (m + n - 2 * ↑i) (n + p - 2 * ↑r) else 0

recouplingCoeff equals sixJ when the total highest weights agree, and 0 otherwise.

theorem TauCeti.UqSl2.invRecouplingCoeff_eq_ite {q : ℂ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) {m n p : ℕ} (r : Fin (min n p + 1)) (s : Fin (min m (n + p - 2 * ↑r) + 1)) (i : Fin (min m n + 1)) (j : Fin (min (m + n - 2 * ↑i) p + 1)) : invRecouplingCoeff hq ε δ ζ r s i j = if m + (n + p - 2 * ↑r) - 2 * ↑s = m + n - 2 * ↑i + p - 2 * ↑j then invSixJ hq ε δ ζ m n p (m + (n + p - 2 * ↑r) - 2 * ↑s) (n + p - 2 * ↑r) (m + n - 2 * ↑i) else 0

invRecouplingCoeff equals invSixJ when the total weights agree, and 0 otherwise.

noncomputable def TauCeti.UqSl2.sixJMatrix {q : ℂ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) (m n p k : ℕ) : Matrix (RightSixJChannel m n p k) (LeftSixJChannel m n p k) ℂ

Change-of-decomposition (F-matrix) at total highest weight k from LeftSixJChannel to RightSixJChannel in the α₀ = 1 normalization of clebschGordanInclusion.

noncomputable def TauCeti.UqSl2.invSixJMatrix {q : ℂ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) (m n p k : ℕ) : Matrix (LeftSixJChannel m n p k) (RightSixJChannel m n p k) ℂ

Inverse change-of-decomposition matrix at total weight k from RightSixJChannel to LeftSixJChannel in the α₀ = 1 normalization of clebschGordanInclusion.

@[simp]

theorem TauCeti.UqSl2.sixJMatrix_apply {q : ℂ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) (m n p k : ℕ) (v : RightSixJChannel m n p k) (u : LeftSixJChannel m n p k) : sixJMatrix hq ε δ ζ m n p k v u = sixJ hq ε δ ζ m n p k ↑u ↑v

Entry formula for sixJMatrix.

@[simp]

theorem TauCeti.UqSl2.invSixJMatrix_apply {q : ℂ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) (m n p k : ℕ) (u : LeftSixJChannel m n p k) (v : RightSixJChannel m n p k) : invSixJMatrix hq ε δ ζ m n p k u v = invSixJ hq ε δ ζ m n p k ↑v ↑u

Entry formula for invSixJMatrix.

Orthogonality and matrix invertibility

theorem TauCeti.UqSl2.sum_invSixJ_mul_sixJ {q : ℂ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) {m n p k u₁ u₂ : ℕ} (hu₁ : IsClebschGordanChannel m n u₁ ∧ IsClebschGordanChannel u₁ p k) (hu₂ : IsClebschGordanChannel m n u₂ ∧ IsClebschGordanChannel u₂ p k) : ∑ v ∈ Finset.range (n + p + 1), invSixJ hq ε δ ζ m n p k v u₁ * sixJ hq ε δ ζ m n p k u₂ v = if u₁ = u₂ then 1 else 0

Orthogonality of invSixJ and sixJ summed over v ∈ Finset.range (n + p + 1).

theorem TauCeti.UqSl2.sum_sixJ_mul_invSixJ {q : ℂ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) {m n p k v₁ v₂ : ℕ} (hv₁ : IsClebschGordanChannel n p v₁ ∧ IsClebschGordanChannel m v₁ k) (hv₂ : IsClebschGordanChannel n p v₂ ∧ IsClebschGordanChannel m v₂ k) : ∑ u ∈ Finset.range (m + n + 1), sixJ hq ε δ ζ m n p k u v₁ * invSixJ hq ε δ ζ m n p k v₂ u = if v₁ = v₂ then 1 else 0

Orthogonality of sixJ and invSixJ summed over u ∈ Finset.range (m + n + 1).

@[simp]

theorem TauCeti.UqSl2.invSixJMatrix_mul_sixJMatrix {q : ℂ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) (m n p k : ℕ) : invSixJMatrix hq ε δ ζ m n p k * sixJMatrix hq ε δ ζ m n p k = 1

invSixJMatrix is a left inverse to sixJMatrix.

@[simp]

theorem TauCeti.UqSl2.sixJMatrix_mul_invSixJMatrix {q : ℂ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) (m n p k : ℕ) : sixJMatrix hq ε δ ζ m n p k * invSixJMatrix hq ε δ ζ m n p k = 1

invSixJMatrix is a right inverse to sixJMatrix.

Explicit boundary evaluations

@[simp]

theorem TauCeti.UqSl2.sixJ_add_add {q : ℂ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) (m n p : ℕ) : sixJ hq ε δ ζ m n p (m + n + p) (m + n) (n + p) = 1

On the leading stretched channel k = m + n + p (u = m + n, v = n + p), sixJ is 1.

@[simp]

theorem TauCeti.UqSl2.sixJ_zero_left {q : ℂ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) {n p k : ℕ} (hk : IsClebschGordanChannel n p k) : sixJ hq ε δ ζ 0 n p k n k = 1

When the first factor is L_0^ε, sixJ on any admissible channel k of L_n^δ ⊗ L_p^ζ equals 1.

@[simp]

theorem TauCeti.UqSl2.sixJ_zero_right {q : ℂ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) {m n k : ℕ} (hk : IsClebschGordanChannel m n k) : sixJ hq ε δ ζ m n 0 k k n = ↑↑ζ ^ ((m + n - k) / 2)

When the third factor is L_0^ζ, sixJ on an admissible channel k of L_m^ε ⊗ L_n^δ equals ζ^((m + n - k) / 2), reflecting the K⁻¹ factor in ΔF = F ⊗ K⁻¹ + 1 ⊗ F.