Recoupling three signed ladder modules

There are two normalized decompositions of a triple tensor product L_m^ε ⊗ L_n^δ ⊗ L_p^ζ at a generic parameter q: first decompose the left pair (clebschGordanLeftEquiv), or first decompose the right pair (clebschGordanRightEquiv). clebschGordanRecouplingEquiv changes between their channel coordinates through the coproduct tensor associator BialgebraModule.assoc, without choosing any additional normalizations beyond clebschGordanInclusion.

Main definitions and results

• clebschGordanLeftInclusion, clebschGordanRightInclusion, clebschGordanLeftProjection, clebschGordanRightProjection: normalized triple-product channel inclusions and projections.
• recouplingHom, invRecouplingHom: channel-to-channel recoupling intertwiners through assoc and assoc.symm.
• recouplingCoeff, invRecouplingCoeff: Schur scalars of recouplingHom and invRecouplingHom, governing their action on every ladder vector v_l (recouplingHom_vec, invRecouplingHom_vec) and vanishing on mismatched channel weights.
• assoc_clebschGordanLeftInclusion_vec, assoc_symm_clebschGordanRightInclusion_vec: explicit triple-product expansions of assoc and assoc.symm on every channel ladder vector v_l.
• sum_invRecouplingCoeff_mul_recouplingCoeff, sum_recouplingCoeff_mul_invRecouplingCoeff: channel-summed orthogonality of recouplingCoeff and invRecouplingCoeff.

References

• C. Kassel, Quantum Groups, Graduate Texts in Mathematics 155, Chapters VII and XII, for Clebsch–Gordan decompositions and recoupling.

@[reducible, inline]

abbrev TauCeti.UqSl2.ClebschGordanLeft (q : ℂ) (m n p : ℕ) (ε δ ζ : ℤˣ) : Type

Channel coordinates obtained by coupling L_m^ε with L_n^δ first, and then with L_p^ζ. The first channel has highest weight m + n - 2i.

@[reducible, inline]

abbrev TauCeti.UqSl2.ClebschGordanRight (q : ℂ) (m n p : ℕ) (ε δ ζ : ℤˣ) : Type

Channel coordinates obtained by coupling L_n^δ with L_p^ζ first, and then with L_m^ε. The first channel has highest weight n + p - 2i.

noncomputable def TauCeti.UqSl2.clebschGordanLeftEquiv {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) : ClebschGordanLeft q m n p ε δ ζ ≃ₗ[UqSl2 q] BialgebraModule.Tensor ℂ (UqSl2 q) (BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ)) (LadderModule q p ζ)

The normalized decomposition of the left-associated triple tensor product.

noncomputable def TauCeti.UqSl2.clebschGordanRightEquiv {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) : ClebschGordanRight q m n p ε δ ζ ≃ₗ[UqSl2 q] BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q m ε) (BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q n δ) (LadderModule q p ζ))

The normalized decomposition of the right-associated triple tensor product.

@[simp]

theorem TauCeti.UqSl2.clebschGordanLeftEquiv_single {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (i : Fin (min m n + 1)) (j : Fin (min (m + n - 2 * ↑i) p + 1)) (x : LadderModule q (m + n - 2 * ↑i + p - 2 * ↑j) (ε * δ * ζ)) : (clebschGordanLeftEquiv hq) (Pi.single i (Pi.single j x)) = (BialgebraModule.tensorMap ℂ (UqSl2 q) (clebschGordanInclusion hq i) LinearMap.id) ((clebschGordanInclusion hq j) x)

On one left channel the decomposition is the composite of its two normalized Clebsch–Gordan inclusions, tensoring the first inclusion with the identity.

@[simp]

theorem TauCeti.UqSl2.clebschGordanRightEquiv_single {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (i : Fin (min n p + 1)) (j : Fin (min m (n + p - 2 * ↑i) + 1)) (x : LadderModule q (m + (n + p - 2 * ↑i) - 2 * ↑j) (ε * (δ * ζ))) : (clebschGordanRightEquiv hq) (Pi.single i (Pi.single j x)) = (BialgebraModule.tensorMap ℂ (UqSl2 q) LinearMap.id (clebschGordanInclusion hq i)) ((clebschGordanInclusion hq j) x)

On one right channel the decomposition is the composite of its two normalized Clebsch–Gordan inclusions, tensoring the identity on L_m^ε with the right-pair inclusion.

@[simp]

theorem TauCeti.UqSl2.clebschGordanRightEquiv_symm_apply {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (x : BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q m ε) (BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q n δ) (LadderModule q p ζ))) (i : Fin (min n p + 1)) (j : Fin (min m (n + p - 2 * ↑i) + 1)) : (clebschGordanRightEquiv hq).symm x i j = (clebschGordanProjection hq j) ((BialgebraModule.tensorMap ℂ (UqSl2 q) LinearMap.id (clebschGordanProjection hq i)) x)

Right-associated channel extraction is the composite of the two binary projections.

@[simp]

theorem TauCeti.UqSl2.clebschGordanLeftEquiv_symm_apply {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (x : BialgebraModule.Tensor ℂ (UqSl2 q) (BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ)) (LadderModule q p ζ)) (i : Fin (min m n + 1)) (j : Fin (min (m + n - 2 * ↑i) p + 1)) : (clebschGordanLeftEquiv hq).symm x i j = (clebschGordanProjection hq j) ((BialgebraModule.tensorMap ℂ (UqSl2 q) (clebschGordanProjection hq i) LinearMap.id) x)

Left-associated channel extraction is the composite of the two binary projections.

noncomputable def TauCeti.UqSl2.clebschGordanRecouplingEquiv {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) : ClebschGordanLeft q m n p ε δ ζ ≃ₗ[UqSl2 q] ClebschGordanRight q m n p ε δ ζ

Change from left-pair-first to right-pair-first Clebsch–Gordan coordinates, through the actual coproduct tensor associator. All three signs and highest weights are arbitrary.

@[simp]

theorem TauCeti.UqSl2.clebschGordanRightEquiv_recoupling {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (x : ClebschGordanLeft q m n p ε δ ζ) : (clebschGordanRightEquiv hq) ((clebschGordanRecouplingEquiv hq) x) = (BialgebraModule.assoc ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ) (LadderModule q p ζ)) ((clebschGordanLeftEquiv hq) x)

Recoupling followed by the right decomposition is the reassociated left decomposition.

@[simp]

theorem TauCeti.UqSl2.clebschGordanLeftEquiv_recoupling_symm {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (x : ClebschGordanRight q m n p ε δ ζ) : (clebschGordanLeftEquiv hq) ((clebschGordanRecouplingEquiv hq).symm x) = (BialgebraModule.assoc ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ) (LadderModule q p ζ)).symm ((clebschGordanRightEquiv hq) x)

Inverse recoupling followed by the left decomposition undoes reassociation of the right decomposition.

theorem TauCeti.UqSl2.clebschGordanRecouplingEquiv_single_apply {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (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)) (x : LadderModule q (m + n - 2 * ↑i + p - 2 * ↑j) (ε * δ * ζ)) : (clebschGordanRecouplingEquiv hq) (Pi.single i (Pi.single j x)) r s = (clebschGordanProjection hq s) ((BialgebraModule.tensorMap ℂ (UqSl2 q) LinearMap.id (clebschGordanProjection hq r)) ((BialgebraModule.assoc ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ) (LadderModule q p ζ)) ((BialgebraModule.tensorMap ℂ (UqSl2 q) (clebschGordanInclusion hq i) LinearMap.id) ((clebschGordanInclusion hq j) x))))

A recoupling coordinate is obtained by including its left channel, reassociating, and then projecting onto the right channel. This fixes the normalization of every entry.

theorem TauCeti.UqSl2.clebschGordanRecouplingEquiv_symm_single_apply {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (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)) (x : LadderModule q (m + (n + p - 2 * ↑r) - 2 * ↑s) (ε * (δ * ζ))) : (clebschGordanRecouplingEquiv hq).symm (Pi.single r (Pi.single s x)) i j = (clebschGordanProjection hq j) ((BialgebraModule.tensorMap ℂ (UqSl2 q) (clebschGordanProjection hq i) LinearMap.id) ((BialgebraModule.assoc ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ) (LadderModule q p ζ)).symm ((BialgebraModule.tensorMap ℂ (UqSl2 q) LinearMap.id (clebschGordanInclusion hq r)) ((clebschGordanInclusion hq s) x))))

An inverse recoupling coordinate is obtained by including its right channel, undoing reassociation, and then projecting onto the left channel.

Triple-product channel inclusions, projections, and recoupling intertwiners

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

Inclusion of the (i, j) left-associated channel into (L_m^ε ⊗ L_n^δ) ⊗ L_p^ζ.

theorem TauCeti.UqSl2.clebschGordanLeftInclusion_def {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (i : Fin (min m n + 1)) (j : Fin (min (m + n - 2 * ↑i) p + 1)) : clebschGordanLeftInclusion hq i j = BialgebraModule.tensorMap ℂ (UqSl2 q) (clebschGordanInclusion hq i) LinearMap.id ∘ₗ clebschGordanInclusion hq j

Definitional composite formula for clebschGordanLeftInclusion.

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

Inclusion of the (r, s) right-associated channel into L_m^ε ⊗ (L_n^δ ⊗ L_p^ζ).

theorem TauCeti.UqSl2.clebschGordanRightInclusion_def {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (r : Fin (min n p + 1)) (s : Fin (min m (n + p - 2 * ↑r) + 1)) : clebschGordanRightInclusion hq r s = BialgebraModule.tensorMap ℂ (UqSl2 q) LinearMap.id (clebschGordanInclusion hq r) ∘ₗ clebschGordanInclusion hq s

Definitional composite formula for clebschGordanRightInclusion.

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

Projection of (L_m^ε ⊗ L_n^δ) ⊗ L_p^ζ onto its (i, j) left-associated channel.

theorem TauCeti.UqSl2.clebschGordanLeftProjection_def {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (i : Fin (min m n + 1)) (j : Fin (min (m + n - 2 * ↑i) p + 1)) : clebschGordanLeftProjection hq i j = clebschGordanProjection hq j ∘ₗ BialgebraModule.tensorMap ℂ (UqSl2 q) (clebschGordanProjection hq i) LinearMap.id

Definitional composite formula for clebschGordanLeftProjection.

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

Projection of L_m^ε ⊗ (L_n^δ ⊗ L_p^ζ) onto its (r, s) right-associated channel.

theorem TauCeti.UqSl2.clebschGordanRightProjection_def {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (r : Fin (min n p + 1)) (s : Fin (min m (n + p - 2 * ↑r) + 1)) : clebschGordanRightProjection hq r s = clebschGordanProjection hq s ∘ₗ BialgebraModule.tensorMap ℂ (UqSl2 q) LinearMap.id (clebschGordanProjection hq r)

Definitional composite formula for clebschGordanRightProjection.

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

clebschGordanLeftInclusion agrees with clebschGordanLeftEquiv on a single channel.

theorem TauCeti.UqSl2.clebschGordanRightInclusion_eq_single {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (r : Fin (min n p + 1)) (s : Fin (min m (n + p - 2 * ↑r) + 1)) (x : LadderModule q (m + (n + p - 2 * ↑r) - 2 * ↑s) (ε * (δ * ζ))) : (clebschGordanRightInclusion hq r s) x = (clebschGordanRightEquiv hq) (Pi.single r (Pi.single s x))

clebschGordanRightInclusion agrees with clebschGordanRightEquiv on a single channel.

theorem TauCeti.UqSl2.clebschGordanLeftProjection_eq_symm {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (i : Fin (min m n + 1)) (j : Fin (min (m + n - 2 * ↑i) p + 1)) (x : BialgebraModule.Tensor ℂ (UqSl2 q) (BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ)) (LadderModule q p ζ)) : (clebschGordanLeftProjection hq i j) x = (clebschGordanLeftEquiv hq).symm x i j

clebschGordanLeftProjection extracts (i, j) of (clebschGordanLeftEquiv).symm.

theorem TauCeti.UqSl2.clebschGordanRightProjection_eq_symm {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (r : Fin (min n p + 1)) (s : Fin (min m (n + p - 2 * ↑r) + 1)) (x : BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q m ε) (BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q n δ) (LadderModule q p ζ))) : (clebschGordanRightProjection hq r s) x = (clebschGordanRightEquiv hq).symm x r s

clebschGordanRightProjection extracts (r, s) of (clebschGordanRightEquiv).symm.

@[simp]

theorem TauCeti.UqSl2.clebschGordanLeftInclusion_vec_zero {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (i : Fin (min m n + 1)) (j : Fin (min (m + n - 2 * ↑i) p + 1)) : (clebschGordanLeftInclusion hq i j) (LadderModule.vec q (m + n - 2 * ↑i + p - 2 * ↑j) (ε * δ * ζ) 0) = (BialgebraModule.tensorMap ℂ (UqSl2 q) (clebschGordanInclusion hq i) LinearMap.id) (clebschGordanVector q (m + n - 2 * ↑i) (ε * δ) p ζ ↑j)

clebschGordanLeftInclusion sends v₀ to the left-coupled α₀ = 1 highest-weight vector.

@[simp]

theorem TauCeti.UqSl2.clebschGordanRightInclusion_vec_zero {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (r : Fin (min n p + 1)) (s : Fin (min m (n + p - 2 * ↑r) + 1)) : (clebschGordanRightInclusion hq r s) (LadderModule.vec q (m + (n + p - 2 * ↑r) - 2 * ↑s) (ε * (δ * ζ)) 0) = (BialgebraModule.tensorMap ℂ (UqSl2 q) LinearMap.id (clebschGordanInclusion hq r)) (clebschGordanVector q m ε (n + p - 2 * ↑r) (δ * ζ) ↑s)

clebschGordanRightInclusion sends v₀ to the right-coupled α₀ = 1 highest-weight vector.

theorem TauCeti.UqSl2.clebschGordanLeftInclusion_zero_vec_zero {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (i : Fin (min m n + 1)) : (clebschGordanLeftInclusion hq i 0) (LadderModule.vec q (m + n - 2 * ↑i + p - 2 * ↑0) (ε * δ * ζ) 0) = BialgebraModule.tmul ℂ (UqSl2 q) (clebschGordanVector q m ε n δ ↑i) (LadderModule.vec q p ζ 0)

On an outer j = 0 channel, clebschGordanLeftInclusion sends v₀ to w_i ⊗ v₀.

theorem TauCeti.UqSl2.clebschGordanRightInclusion_zero_vec_zero {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (r : Fin (min n p + 1)) : (clebschGordanRightInclusion hq r 0) (LadderModule.vec q (m + (n + p - 2 * ↑r) - 2 * ↑0) (ε * (δ * ζ)) 0) = BialgebraModule.tmul ℂ (UqSl2 q) (LadderModule.vec q m ε 0) (clebschGordanVector q n δ p ζ ↑r)

On an outer s = 0 channel, clebschGordanRightInclusion sends v₀ to v₀ ⊗ w_r.

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

clebschGordanLeftInclusion sends v_l to the normalized F-ladder string of v₀.

theorem TauCeti.UqSl2.clebschGordanRightInclusion_vec {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (r : Fin (min n p + 1)) (s : Fin (min m (n + p - 2 * ↑r) + 1)) (l : ℕ) : (clebschGordanRightInclusion hq r s) (LadderModule.vec q (m + (n + p - 2 * ↑r) - 2 * ↑s) (ε * (δ * ζ)) ↑l) = (quantumFactorial q l)⁻¹ • f q ^ l • (clebschGordanRightInclusion hq r s) (LadderModule.vec q (m + (n + p - 2 * ↑r) - 2 * ↑s) (ε * (δ * ζ)) 0)

clebschGordanRightInclusion sends v_l to the normalized F-ladder string of v₀.

@[simp]

theorem TauCeti.UqSl2.clebschGordanLeftProjection_inclusion_self {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (i : Fin (min m n + 1)) (j : Fin (min (m + n - 2 * ↑i) p + 1)) (x : LadderModule q (m + n - 2 * ↑i + p - 2 * ↑j) (ε * δ * ζ)) : (clebschGordanLeftProjection hq i j) ((clebschGordanLeftInclusion hq i j) x) = x

Left channel projection is a left inverse to left channel inclusion.

@[simp]

theorem TauCeti.UqSl2.clebschGordanRightProjection_inclusion_self {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (r : Fin (min n p + 1)) (s : Fin (min m (n + p - 2 * ↑r) + 1)) (x : LadderModule q (m + (n + p - 2 * ↑r) - 2 * ↑s) (ε * (δ * ζ))) : (clebschGordanRightProjection hq r s) ((clebschGordanRightInclusion hq r s) x) = x

Right channel projection is a left inverse to right channel inclusion.

@[simp]

theorem TauCeti.UqSl2.clebschGordanLeftProjection_inclusion_of_ne {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) {i₁ i₂ : Fin (min m n + 1)} {j₁ : Fin (min (m + n - 2 * ↑i₁) p + 1)} {j₂ : Fin (min (m + n - 2 * ↑i₂) p + 1)} (h : ↑i₁ ≠ ↑i₂ ∨ ↑j₁ ≠ ↑j₂) (x : LadderModule q (m + n - 2 * ↑i₂ + p - 2 * ↑j₂) (ε * δ * ζ)) : (clebschGordanLeftProjection hq i₁ j₁) ((clebschGordanLeftInclusion hq i₂ j₂) x) = 0

Distinct left-associated channels are annihilated by clebschGordanLeftProjection.

@[simp]

theorem TauCeti.UqSl2.clebschGordanRightProjection_inclusion_of_ne {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) {r₁ r₂ : Fin (min n p + 1)} {s₁ : Fin (min m (n + p - 2 * ↑r₁) + 1)} {s₂ : Fin (min m (n + p - 2 * ↑r₂) + 1)} (h : ↑r₁ ≠ ↑r₂ ∨ ↑s₁ ≠ ↑s₂) (x : LadderModule q (m + (n + p - 2 * ↑r₂) - 2 * ↑s₂) (ε * (δ * ζ))) : (clebschGordanRightProjection hq r₁ s₁) ((clebschGordanRightInclusion hq r₂ s₂) x) = 0

Distinct right-associated channels are annihilated by clebschGordanRightProjection.

@[simp]

theorem TauCeti.UqSl2.clebschGordanLeftProjection_comp_inclusion_self {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (i : Fin (min m n + 1)) (j : Fin (min (m + n - 2 * ↑i) p + 1)) : clebschGordanLeftProjection hq i j ∘ₗ clebschGordanLeftInclusion hq i j = LinearMap.id

Composing a left channel projection with its left channel inclusion gives LinearMap.id.

@[simp]

theorem TauCeti.UqSl2.clebschGordanRightProjection_comp_inclusion_self {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (r : Fin (min n p + 1)) (s : Fin (min m (n + p - 2 * ↑r) + 1)) : clebschGordanRightProjection hq r s ∘ₗ clebschGordanRightInclusion hq r s = LinearMap.id

Composing a right channel projection with its right channel inclusion gives LinearMap.id.

@[simp]

theorem TauCeti.UqSl2.clebschGordanLeftProjection_comp_inclusion_of_ne {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) {i₁ i₂ : Fin (min m n + 1)} {j₁ : Fin (min (m + n - 2 * ↑i₁) p + 1)} {j₂ : Fin (min (m + n - 2 * ↑i₂) p + 1)} (h : ↑i₁ ≠ ↑i₂ ∨ ↑j₁ ≠ ↑j₂) : clebschGordanLeftProjection hq i₁ j₁ ∘ₗ clebschGordanLeftInclusion hq i₂ j₂ = 0

Composing a left channel projection with a distinct left channel inclusion gives 0.

@[simp]

theorem TauCeti.UqSl2.clebschGordanRightProjection_comp_inclusion_of_ne {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) {r₁ r₂ : Fin (min n p + 1)} {s₁ : Fin (min m (n + p - 2 * ↑r₁) + 1)} {s₂ : Fin (min m (n + p - 2 * ↑r₂) + 1)} (h : ↑r₁ ≠ ↑r₂ ∨ ↑s₁ ≠ ↑s₂) : clebschGordanRightProjection hq r₁ s₁ ∘ₗ clebschGordanRightInclusion hq r₂ s₂ = 0

Composing a right channel projection with a distinct right channel inclusion gives 0.

noncomputable def TauCeti.UqSl2.recouplingHom {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (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)) : LadderModule q (m + n - 2 * ↑i + p - 2 * ↑j) (ε * δ * ζ) →ₗ[UqSl2 q] LadderModule q (m + (n + p - 2 * ↑r) - 2 * ↑s) (ε * (δ * ζ))

Channel-to-channel recoupling intertwiner (i, j) → (r, s) through BialgebraModule.assoc.

theorem TauCeti.UqSl2.recouplingHom_def {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (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)) : recouplingHom hq i j r s = clebschGordanRightProjection hq r s ∘ₗ ↑(BialgebraModule.assoc ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ) (LadderModule q p ζ)) ∘ₗ clebschGordanLeftInclusion hq i j

Definitional composite formula for recouplingHom.

noncomputable def TauCeti.UqSl2.invRecouplingHom {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (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)) : LadderModule q (m + (n + p - 2 * ↑r) - 2 * ↑s) (ε * (δ * ζ)) →ₗ[UqSl2 q] LadderModule q (m + n - 2 * ↑i + p - 2 * ↑j) (ε * δ * ζ)

Inverse recoupling intertwiner (r, s) → (i, j) through (BialgebraModule.assoc).symm.

theorem TauCeti.UqSl2.invRecouplingHom_def {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (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)) : invRecouplingHom hq r s i j = clebschGordanLeftProjection hq i j ∘ₗ ↑(BialgebraModule.assoc ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ) (LadderModule q p ζ)).symm ∘ₗ clebschGordanRightInclusion hq r s

Definitional composite formula for invRecouplingHom.

theorem TauCeti.UqSl2.recouplingHom_apply {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (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)) (x : LadderModule q (m + n - 2 * ↑i + p - 2 * ↑j) (ε * δ * ζ)) : (recouplingHom hq i j r s) x = (clebschGordanRecouplingEquiv hq) (Pi.single i (Pi.single j x)) r s

recouplingHom agrees with coordinate (r, s) of clebschGordanRecouplingEquiv.

theorem TauCeti.UqSl2.invRecouplingHom_apply {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (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)) (x : LadderModule q (m + (n + p - 2 * ↑r) - 2 * ↑s) (ε * (δ * ζ))) : (invRecouplingHom hq r s i j) x = (clebschGordanRecouplingEquiv hq).symm (Pi.single r (Pi.single s x)) i j

invRecouplingHom agrees with coordinate (i, j) of (clebschGordanRecouplingEquiv).symm.

Recoupling scalars, basis expansions, and channel orthogonality

noncomputable def TauCeti.UqSl2.recouplingCoeff {q : ℂ} {m n p : ℕ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) (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)) : ℂ

Scalar recoupling coefficient from left channel (i, j) to right channel (r, s).

theorem TauCeti.UqSl2.recouplingCoeff_def {q : ℂ} {m n p : ℕ} [Fact (q ≠ 0)] (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) (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 = LadderModule.schurScalar (recouplingHom hq i j r s)

Definitional Schur-scalar formula for recouplingCoeff.

noncomputable def TauCeti.UqSl2.invRecouplingCoeff {q : ℂ} {m n p : ℕ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) (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)) : ℂ

Inverse scalar recoupling coefficient from right channel (r, s) to left channel (i, j).

theorem TauCeti.UqSl2.invRecouplingCoeff_def {q : ℂ} {m n p : ℕ} [Fact (q ≠ 0)] (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) (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 = LadderModule.schurScalar (invRecouplingHom hq r s i j)

Definitional Schur-scalar formula for invRecouplingCoeff.

theorem TauCeti.UqSl2.recouplingCoeff_congr {q : ℂ} {m n p : ℕ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) {i₁ i₂ : Fin (min m n + 1)} {j₁ : Fin (min (m + n - 2 * ↑i₁) p + 1)} {j₂ : Fin (min (m + n - 2 * ↑i₂) p + 1)} {r₁ r₂ : Fin (min n p + 1)} {s₁ : Fin (min m (n + p - 2 * ↑r₁) + 1)} {s₂ : Fin (min m (n + p - 2 * ↑r₂) + 1)} (hi : ↑i₁ = ↑i₂) (hj : ↑j₁ = ↑j₂) (hr : ↑r₁ = ↑r₂) (hs : ↑s₁ = ↑s₂) : recouplingCoeff hq ε δ ζ i₁ j₁ r₁ s₁ = recouplingCoeff hq ε δ ζ i₂ j₂ r₂ s₂

Congruence of recouplingCoeff along equality of underlying natural-number indices.

theorem TauCeti.UqSl2.invRecouplingCoeff_congr {q : ℂ} {m n p : ℕ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) {r₁ r₂ : Fin (min n p + 1)} {s₁ : Fin (min m (n + p - 2 * ↑r₁) + 1)} {s₂ : Fin (min m (n + p - 2 * ↑r₂) + 1)} {i₁ i₂ : Fin (min m n + 1)} {j₁ : Fin (min (m + n - 2 * ↑i₁) p + 1)} {j₂ : Fin (min (m + n - 2 * ↑i₂) p + 1)} (hr : ↑r₁ = ↑r₂) (hs : ↑s₁ = ↑s₂) (hi : ↑i₁ = ↑i₂) (hj : ↑j₁ = ↑j₂) : invRecouplingCoeff hq ε δ ζ r₁ s₁ i₁ j₁ = invRecouplingCoeff hq ε δ ζ r₂ s₂ i₂ j₂

Congruence of invRecouplingCoeff along equality of underlying natural-number indices.

theorem TauCeti.UqSl2.recouplingCoeff_eq_zero_of_ne {q : ℂ} {m n p : ℕ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) {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)} (hne : m + n - 2 * ↑i + p - 2 * ↑j ≠ m + (n + p - 2 * ↑r) - 2 * ↑s) : recouplingCoeff hq ε δ ζ i j r s = 0

recouplingCoeff vanishes when the left and right channels have distinct total weights.

theorem TauCeti.UqSl2.invRecouplingCoeff_eq_zero_of_ne {q : ℂ} {m n p : ℕ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) {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)} (hne : m + (n + p - 2 * ↑r) - 2 * ↑s ≠ m + n - 2 * ↑i + p - 2 * ↑j) : invRecouplingCoeff hq ε δ ζ r s i j = 0

invRecouplingCoeff vanishes when the right and left channels have distinct total weights.

theorem TauCeti.UqSl2.recouplingCoeff_eq_zero_of_not_channel_right {q : ℂ} {m n p : ℕ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) {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)} {k : ℕ} (hk : m + n - 2 * ↑i + p - 2 * ↑j = k) (hnot : ¬IsClebschGordanChannel m (n + p - 2 * ↑r) k) : recouplingCoeff hq ε δ ζ i j r s = 0

recouplingCoeff vanishes when the right outer coupling to k is inadmissible.

theorem TauCeti.UqSl2.recouplingCoeff_eq_zero_of_ne_index_right {q : ℂ} {m n p : ℕ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) {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)} {k : ℕ} (hk : m + n - 2 * ↑i + p - 2 * ↑j = k) (hmv : IsClebschGordanChannel m (n + p - 2 * ↑r) k) (hs : s ≠ hmv.index) : recouplingCoeff hq ε δ ζ i j r s = 0

recouplingCoeff vanishes off the unique right outer index hmv.index for total weight k.

theorem TauCeti.UqSl2.recouplingCoeff_eq_zero_of_not_channel_left {q : ℂ} {m n p : ℕ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) {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)} {k : ℕ} (hk : m + (n + p - 2 * ↑r) - 2 * ↑s = k) (hnot : ¬IsClebschGordanChannel (m + n - 2 * ↑i) p k) : recouplingCoeff hq ε δ ζ i j r s = 0

recouplingCoeff vanishes when the left outer coupling to k is inadmissible.

theorem TauCeti.UqSl2.recouplingCoeff_eq_zero_of_ne_index_left {q : ℂ} {m n p : ℕ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) {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)} {k : ℕ} (hk : m + (n + p - 2 * ↑r) - 2 * ↑s = k) (hup : IsClebschGordanChannel (m + n - 2 * ↑i) p k) (hj : j ≠ hup.index) : recouplingCoeff hq ε δ ζ i j r s = 0

recouplingCoeff vanishes off the unique left outer index hup.index for total weight k.

theorem TauCeti.UqSl2.invRecouplingCoeff_eq_zero_of_not_channel_left {q : ℂ} {m n p : ℕ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) {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)} {k : ℕ} (hk : m + (n + p - 2 * ↑r) - 2 * ↑s = k) (hnot : ¬IsClebschGordanChannel (m + n - 2 * ↑i) p k) : invRecouplingCoeff hq ε δ ζ r s i j = 0

invRecouplingCoeff vanishes when the left outer coupling to k is inadmissible.

theorem TauCeti.UqSl2.invRecouplingCoeff_eq_zero_of_ne_index_left {q : ℂ} {m n p : ℕ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) {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)} {k : ℕ} (hk : m + (n + p - 2 * ↑r) - 2 * ↑s = k) (hup : IsClebschGordanChannel (m + n - 2 * ↑i) p k) (hj : j ≠ hup.index) : invRecouplingCoeff hq ε δ ζ r s i j = 0

invRecouplingCoeff vanishes off the unique left outer index hup.index for weight k.

@[simp]

theorem TauCeti.UqSl2.recouplingHom_vec {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (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)) (l : ℤ) : (recouplingHom hq i j r s) (LadderModule.vec q (m + n - 2 * ↑i + p - 2 * ↑j) (ε * δ * ζ) l) = recouplingCoeff hq ε δ ζ i j r s • LadderModule.vec q (m + (n + p - 2 * ↑r) - 2 * ↑s) (ε * (δ * ζ)) l

recouplingHom acts on every ladder vector v_l by multiplication by recouplingCoeff.

@[simp]

theorem TauCeti.UqSl2.invRecouplingHom_vec {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (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)) (l : ℤ) : (invRecouplingHom hq r s i j) (LadderModule.vec q (m + (n + p - 2 * ↑r) - 2 * ↑s) (ε * (δ * ζ)) l) = invRecouplingCoeff hq ε δ ζ r s i j • LadderModule.vec q (m + n - 2 * ↑i + p - 2 * ↑j) (ε * δ * ζ) l

invRecouplingHom acts on every ladder vector v_l by invRecouplingCoeff.

@[simp]

theorem TauCeti.UqSl2.clebschGordanRecouplingEquiv_single_vec {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (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)) (l : ℤ) : (clebschGordanRecouplingEquiv hq) (Pi.single i (Pi.single j (LadderModule.vec q (m + n - 2 * ↑i + p - 2 * ↑j) (ε * δ * ζ) l))) r s = recouplingCoeff hq ε δ ζ i j r s • LadderModule.vec q (m + (n + p - 2 * ↑r) - 2 * ↑s) (ε * (δ * ζ)) l

Action of clebschGordanRecouplingEquiv on every ladder vector v_l of a left channel.

@[simp]

theorem TauCeti.UqSl2.clebschGordanRecouplingEquiv_symm_single_vec {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (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)) (l : ℤ) : (clebschGordanRecouplingEquiv hq).symm (Pi.single r (Pi.single s (LadderModule.vec q (m + (n + p - 2 * ↑r) - 2 * ↑s) (ε * (δ * ζ)) l))) i j = invRecouplingCoeff hq ε δ ζ r s i j • LadderModule.vec q (m + n - 2 * ↑i + p - 2 * ↑j) (ε * δ * ζ) l

Action of (clebschGordanRecouplingEquiv).symm on every v_l of a right channel.

theorem TauCeti.UqSl2.assoc_comp_clebschGordanLeftInclusion {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (i : Fin (min m n + 1)) (j : Fin (min (m + n - 2 * ↑i) p + 1)) : ↑(BialgebraModule.assoc ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ) (LadderModule q p ζ)) ∘ₗ clebschGordanLeftInclusion hq i j = ∑ r : Fin (min n p + 1), ∑ s : Fin (min m (n + p - 2 * ↑r) + 1), clebschGordanRightInclusion hq r s ∘ₗ recouplingHom hq i j r s

Operator-level expansion of assoc composed with clebschGordanLeftInclusion.

theorem TauCeti.UqSl2.assoc_symm_comp_clebschGordanRightInclusion {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (r : Fin (min n p + 1)) (s : Fin (min m (n + p - 2 * ↑r) + 1)) : ↑(BialgebraModule.assoc ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ) (LadderModule q p ζ)).symm ∘ₗ clebschGordanRightInclusion hq r s = ∑ i : Fin (min m n + 1), ∑ j : Fin (min (m + n - 2 * ↑i) p + 1), clebschGordanLeftInclusion hq i j ∘ₗ invRecouplingHom hq r s i j

Operator-level inverse expansion of assoc.symm composed with clebschGordanRightInclusion.

theorem TauCeti.UqSl2.assoc_clebschGordanLeftInclusion_vec {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (i : Fin (min m n + 1)) (j : Fin (min (m + n - 2 * ↑i) p + 1)) (l : ℤ) : (BialgebraModule.assoc ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ) (LadderModule q p ζ)) ((clebschGordanLeftInclusion hq i j) (LadderModule.vec q (m + n - 2 * ↑i + p - 2 * ↑j) (ε * δ * ζ) l)) = ∑ r : Fin (min n p + 1), ∑ s : Fin (min m (n + p - 2 * ↑r) + 1), recouplingCoeff hq ε δ ζ i j r s • (clebschGordanRightInclusion hq r s) (LadderModule.vec q (m + (n + p - 2 * ↑r) - 2 * ↑s) (ε * (δ * ζ)) l)

Triple-product recoupling expansion. Under BialgebraModule.assoc, every v_l of left channel (i, j) expands in the right-channel v_l with coefficients recouplingCoeff.

theorem TauCeti.UqSl2.assoc_symm_clebschGordanRightInclusion_vec {q : ℂ} [Fact (q ≠ 0)] {m n p : ℕ} {ε δ ζ : ℤˣ} (hq : IsGenericQuantumParameter q) (r : Fin (min n p + 1)) (s : Fin (min m (n + p - 2 * ↑r) + 1)) (l : ℤ) : (BialgebraModule.assoc ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ) (LadderModule q p ζ)).symm ((clebschGordanRightInclusion hq r s) (LadderModule.vec q (m + (n + p - 2 * ↑r) - 2 * ↑s) (ε * (δ * ζ)) l)) = ∑ i : Fin (min m n + 1), ∑ j : Fin (min (m + n - 2 * ↑i) p + 1), invRecouplingCoeff hq ε δ ζ r s i j • (clebschGordanLeftInclusion hq i j) (LadderModule.vec q (m + n - 2 * ↑i + p - 2 * ↑j) (ε * δ * ζ) l)

Inverse triple-product recoupling expansion. Under (BialgebraModule.assoc).symm, every v_l of right channel (r, s) expands in the left-channel v_l via invRecouplingCoeff.

theorem TauCeti.UqSl2.sum_invRecouplingCoeff_mul_recouplingCoeff {q : ℂ} {m n p : ℕ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) (i₁ i₂ : Fin (min m n + 1)) (j₁ : Fin (min (m + n - 2 * ↑i₁) p + 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), invRecouplingCoeff hq ε δ ζ r s i₁ j₁ * recouplingCoeff hq ε δ ζ i₂ j₂ r s = if ↑i₁ = ↑i₂ ∧ ↑j₁ = ↑j₂ then 1 else 0

Channel-summed left orthogonality of invRecouplingCoeff and recouplingCoeff.

theorem TauCeti.UqSl2.sum_recouplingCoeff_mul_invRecouplingCoeff {q : ℂ} {m n p : ℕ} (hq : IsGenericQuantumParameter q) (ε δ ζ : ℤˣ) (r₁ r₂ : Fin (min n p + 1)) (s₁ : Fin (min m (n + p - 2 * ↑r₁) + 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), recouplingCoeff hq ε δ ζ i j r₁ s₁ * invRecouplingCoeff hq ε δ ζ r₂ s₂ i j = if ↑r₁ = ↑r₂ ∧ ↑s₁ = ↑s₂ then 1 else 0

Channel-summed right orthogonality of recouplingCoeff and invRecouplingCoeff.