The Biedenharn–Elliott pentagon identity for U_q(sl₂)

On a fourfold tensor product ((L_a^ε ⊗ L_b^δ) ⊗ L_c^ζ) ⊗ L_d^θ of signed ladder modules at a generic parameter q, Mac Lane's pentagon coherence identity (BialgebraModule.assoc_pentagon) equates the two-step and three-step composites of coproduct tensor associators landing in L_a^ε ⊗ (L_b^δ ⊗ (L_c^ζ ⊗ L_d^θ)).

Composing with the normalized fourfold inclusions (clebschGordanQuadLeftInclusion) and projections (clebschGordanQuadRightProjection) defines quadRecouplingHom. Evaluating it on v_l along both sides of assoc_pentagon yields the index-form identity (recouplingCoeff_pentagon) and the unconditional six-weight Biedenharn–Elliott pentagon identity (sixJ_pentagon) for the α₀ = 1 change-of-decomposition (F-matrix) entries sixJ of clebschGordanInclusion (rather than the rescaled, tetrahedrally symmetric Racah/Kirillov–Reshetikhin 6j symbol).

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 the quantum recoupling pentagon relation, up to basis rescaling).

noncomputable def TauCeti.UqSl2.clebschGordanQuadLeftInclusion {q : ℂ} [Fact (q ≠ 0)] {a b c d : ℕ} {ε δ ζ θ : ℤˣ} (hq : IsGenericQuantumParameter q) (i₁ : Fin (min a b + 1)) (i₂ : Fin (min (a + b - 2 * ↑i₁) c + 1)) (i₃ : Fin (min (a + b - 2 * ↑i₁ + c - 2 * ↑i₂) d + 1)) : LadderModule q (a + b - 2 * ↑i₁ + c - 2 * ↑i₂ + d - 2 * ↑i₃) (ε * δ * ζ * θ) →ₗ[UqSl2 q] BialgebraModule.Tensor ℂ (UqSl2 q) (BialgebraModule.Tensor ℂ (UqSl2 q) (BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q a ε) (LadderModule q b δ)) (LadderModule q c ζ)) (LadderModule q d θ)

Normalized inclusion of the (i₁, i₂, i₃) fully left-associated channel into ((L_a^ε ⊗ L_b^δ) ⊗ L_c^ζ) ⊗ L_d^θ.

theorem TauCeti.UqSl2.clebschGordanQuadLeftInclusion_def {q : ℂ} [Fact (q ≠ 0)] {a b c d : ℕ} {ε δ ζ θ : ℤˣ} (hq : IsGenericQuantumParameter q) (i₁ : Fin (min a b + 1)) (i₂ : Fin (min (a + b - 2 * ↑i₁) c + 1)) (i₃ : Fin (min (a + b - 2 * ↑i₁ + c - 2 * ↑i₂) d + 1)) : clebschGordanQuadLeftInclusion hq i₁ i₂ i₃ = BialgebraModule.tensorMap ℂ (UqSl2 q) (clebschGordanLeftInclusion hq i₁ i₂) LinearMap.id ∘ₗ clebschGordanInclusion hq i₃

Definitional composite formula for clebschGordanQuadLeftInclusion.

noncomputable def TauCeti.UqSl2.clebschGordanQuadRightProjection {q : ℂ} [Fact (q ≠ 0)] {a b c d : ℕ} {ε δ ζ θ : ℤˣ} (hq : IsGenericQuantumParameter q) (r₁ : Fin (min c d + 1)) (r₂ : Fin (min b (c + d - 2 * ↑r₁) + 1)) (r₃ : Fin (min a (b + (c + d - 2 * ↑r₁) - 2 * ↑r₂) + 1)) : BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q a ε) (BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q b δ) (BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q c ζ) (LadderModule q d θ))) →ₗ[UqSl2 q] LadderModule q (a + (b + (c + d - 2 * ↑r₁) - 2 * ↑r₂) - 2 * ↑r₃) (ε * (δ * (ζ * θ)))

Normalized projection of L_a^ε ⊗ (L_b^δ ⊗ (L_c^ζ ⊗ L_d^θ)) onto its (r₁, r₂, r₃) fully right-associated channel.

theorem TauCeti.UqSl2.clebschGordanQuadRightProjection_def {q : ℂ} [Fact (q ≠ 0)] {a b c d : ℕ} {ε δ ζ θ : ℤˣ} (hq : IsGenericQuantumParameter q) (r₁ : Fin (min c d + 1)) (r₂ : Fin (min b (c + d - 2 * ↑r₁) + 1)) (r₃ : Fin (min a (b + (c + d - 2 * ↑r₁) - 2 * ↑r₂) + 1)) : clebschGordanQuadRightProjection hq r₁ r₂ r₃ = clebschGordanRightProjection hq r₂ r₃ ∘ₗ BialgebraModule.tensorMap ℂ (UqSl2 q) LinearMap.id (BialgebraModule.tensorMap ℂ (UqSl2 q) LinearMap.id (clebschGordanProjection hq r₁))

Definitional composite formula for clebschGordanQuadRightProjection.

noncomputable def TauCeti.UqSl2.quadRecouplingHom {q : ℂ} [Fact (q ≠ 0)] {a b c d : ℕ} {ε δ ζ θ : ℤˣ} (hq : IsGenericQuantumParameter q) (i₁ : Fin (min a b + 1)) (i₂ : Fin (min (a + b - 2 * ↑i₁) c + 1)) (i₃ : Fin (min (a + b - 2 * ↑i₁ + c - 2 * ↑i₂) d + 1)) (r₁ : Fin (min c d + 1)) (r₂ : Fin (min b (c + d - 2 * ↑r₁) + 1)) (r₃ : Fin (min a (b + (c + d - 2 * ↑r₁) - 2 * ↑r₂) + 1)) : LadderModule q (a + b - 2 * ↑i₁ + c - 2 * ↑i₂ + d - 2 * ↑i₃) (ε * δ * ζ * θ) →ₗ[UqSl2 q] LadderModule q (a + (b + (c + d - 2 * ↑r₁) - 2 * ↑r₂) - 2 * ↑r₃) (ε * (δ * (ζ * θ)))

Fourfold recoupling intertwiner from left channel (i₁, i₂, i₃) to right channel (r₁, r₂, r₃) across (assoc (A ⊗ B) C D).trans (assoc A B (C ⊗ D)).

theorem TauCeti.UqSl2.quadRecouplingHom_def {q : ℂ} [Fact (q ≠ 0)] {a b c d : ℕ} {ε δ ζ θ : ℤˣ} (hq : IsGenericQuantumParameter q) (i₁ : Fin (min a b + 1)) (i₂ : Fin (min (a + b - 2 * ↑i₁) c + 1)) (i₃ : Fin (min (a + b - 2 * ↑i₁ + c - 2 * ↑i₂) d + 1)) (r₁ : Fin (min c d + 1)) (r₂ : Fin (min b (c + d - 2 * ↑r₁) + 1)) (r₃ : Fin (min a (b + (c + d - 2 * ↑r₁) - 2 * ↑r₂) + 1)) : quadRecouplingHom hq i₁ i₂ i₃ r₁ r₂ r₃ = clebschGordanQuadRightProjection hq r₁ r₂ r₃ ∘ₗ ↑(BialgebraModule.assoc ℂ (UqSl2 q) (BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q a ε) (LadderModule q b δ)) (LadderModule q c ζ) (LadderModule q d θ) ≪≫ₗ BialgebraModule.assoc ℂ (UqSl2 q) (LadderModule q a ε) (LadderModule q b δ) (BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q c ζ) (LadderModule q d θ))) ∘ₗ clebschGordanQuadLeftInclusion hq i₁ i₂ i₃

Definitional composite formula for quadRecouplingHom.

theorem TauCeti.UqSl2.clebschGordanQuadLeftInclusion_apply {q : ℂ} [Fact (q ≠ 0)] {a b c d : ℕ} {ε δ ζ θ : ℤˣ} (hq : IsGenericQuantumParameter q) (i₁ : Fin (min a b + 1)) (i₂ : Fin (min (a + b - 2 * ↑i₁) c + 1)) (i₃ : Fin (min (a + b - 2 * ↑i₁ + c - 2 * ↑i₂) d + 1)) (v : LadderModule q (a + b - 2 * ↑i₁ + c - 2 * ↑i₂ + d - 2 * ↑i₃) (ε * δ * ζ * θ)) : (clebschGordanQuadLeftInclusion hq i₁ i₂ i₃) v = (BialgebraModule.tensorMap ℂ (UqSl2 q) (BialgebraModule.tensorMap ℂ (UqSl2 q) (clebschGordanInclusion hq i₁) LinearMap.id) LinearMap.id) ((clebschGordanLeftInclusion hq i₂ i₃) v)

clebschGordanQuadLeftInclusion factors through clebschGordanLeftInclusion on (i₂, i₃).

theorem TauCeti.UqSl2.clebschGordanQuadRightProjection_apply {q : ℂ} [Fact (q ≠ 0)] {a b c d : ℕ} {ε δ ζ θ : ℤˣ} (hq : IsGenericQuantumParameter q) (r₁ : Fin (min c d + 1)) (r₂ : Fin (min b (c + d - 2 * ↑r₁) + 1)) (r₃ : Fin (min a (b + (c + d - 2 * ↑r₁) - 2 * ↑r₂) + 1)) (z : BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q a ε) (BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q b δ) (BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q c ζ) (LadderModule q d θ)))) : (clebschGordanQuadRightProjection hq r₁ r₂ r₃) z = (clebschGordanProjection hq r₃) ((BialgebraModule.tensorMap ℂ (UqSl2 q) LinearMap.id (clebschGordanRightProjection hq r₁ r₂)) z)

clebschGordanQuadRightProjection factors through clebschGordanRightProjection.

theorem TauCeti.UqSl2.quadRecouplingHom_vec_eq_sum_recouplingCoeff_mul_smul {q : ℂ} [Fact (q ≠ 0)] {a b c d : ℕ} {ε δ ζ θ : ℤˣ} (hq : IsGenericQuantumParameter q) (i₁ : Fin (min a b + 1)) (i₂ : Fin (min (a + b - 2 * ↑i₁) c + 1)) (i₃ : Fin (min (a + b - 2 * ↑i₁ + c - 2 * ↑i₂) d + 1)) (r₁ : Fin (min c d + 1)) (r₂ : Fin (min b (c + d - 2 * ↑r₁) + 1)) (r₃ : Fin (min a (b + (c + d - 2 * ↑r₁) - 2 * ↑r₂) + 1)) (l : ℤ) : (quadRecouplingHom hq i₁ i₂ i₃ r₁ r₂ r₃) (LadderModule.vec q (a + b - 2 * ↑i₁ + c - 2 * ↑i₂ + d - 2 * ↑i₃) (ε * δ * ζ * θ) l) = (∑ p₂ : Fin (min (a + b - 2 * ↑i₁) (c + d - 2 * ↑r₁) + 1), recouplingCoeff hq ε δ (ζ * θ) i₁ p₂ r₂ r₃ * recouplingCoeff hq (ε * δ) ζ θ i₂ i₃ r₁ p₂) • LadderModule.vec q (a + (b + (c + d - 2 * ↑r₁) - 2 * ↑r₂) - 2 * ↑r₃) (ε * (δ * (ζ * θ))) l

Evaluation of quadRecouplingHom on every ladder vector v_l along the two-step associator path ((A ⊗ B) ⊗ C) ⊗ D → (A ⊗ B) ⊗ (C ⊗ D) → A ⊗ (B ⊗ (C ⊗ D)).

theorem TauCeti.UqSl2.quadRecouplingHom_vec_eq_sum_sum_recouplingCoeff_mul_smul {q : ℂ} [Fact (q ≠ 0)] {a b c d : ℕ} {ε δ ζ θ : ℤˣ} (hq : IsGenericQuantumParameter q) (i₁ : Fin (min a b + 1)) (i₂ : Fin (min (a + b - 2 * ↑i₁) c + 1)) (i₃ : Fin (min (a + b - 2 * ↑i₁ + c - 2 * ↑i₂) d + 1)) (r₁ : Fin (min c d + 1)) (r₂ : Fin (min b (c + d - 2 * ↑r₁) + 1)) (r₃ : Fin (min a (b + (c + d - 2 * ↑r₁) - 2 * ↑r₂) + 1)) (l : ℤ) : (quadRecouplingHom hq i₁ i₂ i₃ r₁ r₂ r₃) (LadderModule.vec q (a + b - 2 * ↑i₁ + c - 2 * ↑i₂ + d - 2 * ↑i₃) (ε * δ * ζ * θ) l) = (∑ q₁ : Fin (min b c + 1), ∑ q₂ : Fin (min a (b + c - 2 * ↑q₁) + 1), if hw : a + b - 2 * ↑i₁ + c - 2 * ↑i₂ = a + (b + c - 2 * ↑q₁) - 2 * ↑q₂ then ∑ p₁ : Fin (min (b + c - 2 * ↑q₁) d + 1), ∑ p₂ : Fin (min a (b + c - 2 * ↑q₁ + d - 2 * ↑p₁) + 1), if ↑p₂ = ↑r₃ then recouplingCoeff hq δ ζ θ q₁ p₁ r₁ r₂ * recouplingCoeff hq ε (δ * ζ) θ q₂ (Fin.cast ⋯ i₃) p₁ p₂ * recouplingCoeff hq ε δ ζ i₁ i₂ q₁ q₂ else 0 else 0) • LadderModule.vec q (a + (b + (c + d - 2 * ↑r₁) - 2 * ↑r₂) - 2 * ↑r₃) (ε * (δ * (ζ * θ))) l

Evaluation of quadRecouplingHom on every ladder vector v_l along the three-step associator path ((A ⊗ B) ⊗ C) ⊗ D → (A ⊗ (B ⊗ C)) ⊗ D → A ⊗ ((B ⊗ C) ⊗ D) → A ⊗ (B ⊗ (C ⊗ D)) via BialgebraModule.assoc_pentagon_apply.

Channel-index and six-weight Biedenharn–Elliott pentagon identities

theorem TauCeti.UqSl2.recouplingCoeff_pentagon {q : ℂ} (hq : IsGenericQuantumParameter q) (ε δ ζ θ : ℤˣ) {a b c d : ℕ} (i₁ : Fin (min a b + 1)) (i₂ : Fin (min (a + b - 2 * ↑i₁) c + 1)) (i₃ : Fin (min (a + b - 2 * ↑i₁ + c - 2 * ↑i₂) d + 1)) (r₁ : Fin (min c d + 1)) (r₂ : Fin (min b (c + d - 2 * ↑r₁) + 1)) (r₃ : Fin (min a (b + (c + d - 2 * ↑r₁) - 2 * ↑r₂) + 1)) : ∑ p₂ : Fin (min (a + b - 2 * ↑i₁) (c + d - 2 * ↑r₁) + 1), recouplingCoeff hq ε δ (ζ * θ) i₁ p₂ r₂ r₃ * recouplingCoeff hq (ε * δ) ζ θ i₂ i₃ r₁ p₂ = ∑ q₁ : Fin (min b c + 1), ∑ q₂ : Fin (min a (b + c - 2 * ↑q₁) + 1), if hw : a + b - 2 * ↑i₁ + c - 2 * ↑i₂ = a + (b + c - 2 * ↑q₁) - 2 * ↑q₂ then ∑ p₁ : Fin (min (b + c - 2 * ↑q₁) d + 1), ∑ p₂ : Fin (min a (b + c - 2 * ↑q₁ + d - 2 * ↑p₁) + 1), if ↑p₂ = ↑r₃ then recouplingCoeff hq δ ζ θ q₁ p₁ r₁ r₂ * recouplingCoeff hq ε (δ * ζ) θ q₂ (Fin.cast ⋯ i₃) p₁ p₂ * recouplingCoeff hq ε δ ζ i₁ i₂ q₁ q₂ else 0 else 0

Index-form pentagon identity for recouplingCoeff across all fourfold left-associated channels (i₁, i₂, i₃) and right-associated channels (r₁, r₂, r₃).

theorem TauCeti.UqSl2.sixJ_pentagon {q : ℂ} (hq : IsGenericQuantumParameter q) (ε δ ζ θ : ℤˣ) (a b c d e u w x y : ℕ) : sixJ hq ε δ (ζ * θ) a b y e u x * sixJ hq (ε * δ) ζ θ u c d e w y = ∑ z ∈ Finset.range (b + c + 1), sixJ hq δ ζ θ b c d x z y * sixJ hq ε (δ * ζ) θ a z d e w x * sixJ hq ε δ ζ a b c w u z

The Biedenharn–Elliott pentagon identity for the α₀ = 1 change-of-decomposition (F-matrix) entries sixJ of clebschGordanInclusion across all signed ladder modules L_a^ε ⊗ L_b^δ ⊗ L_c^ζ ⊗ L_d^θ at generic q.