Inverse Clebsch–Gordan maps and Casimir spectral projections

The normalized Clebsch–Gordan inclusions admit module-linear projections back to each signed ladder summand. Their composites are the spectral projections of the Casimir: the projection onto channel j is the Lagrange polynomial which is one at that channel's Casimir scalar and zero at the other channel scalars, evaluated on the Casimir action. Thus each channel is exactly a Casimir eigenspace, and these projections resolve the identity, commute with every module endomorphism, and are natural with respect to module maps on the two tensor factors via LadderModule.schurScalar. The projections extract components in the normalized highest-vector and lowering string bases, as needed when comparing iterated tensor decompositions.

The inclusions and their normalization are those of clebschGordanInclusion; no choice of basis or normalization is made in defining the inverse maps.

References

• C. Kassel, Quantum Groups, Graduate Texts in Mathematics 155, Chapter VII, for the signed Clebsch–Gordan decomposition.

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

The inverse Clebsch–Gordan map onto channel j, with the normalization of clebschGordanInclusion.

theorem TauCeti.UqSl2.clebschGordanProjection_apply {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) (j : Fin (min m n + 1)) (x : BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ)) : (clebschGordanProjection hq j) x = (clebschGordanEquiv hq).symm x j

The projections are the components of the inverse decomposition map.

@[simp]

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

The inverse map recovers the j-th component of a Clebsch–Gordan expansion.

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

Projection onto an included channel gives its corresponding single component.

@[simp]

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

A channel projection is a left inverse of its normalized inclusion.

@[simp]

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

Different channels are annihilated by the projection.

@[simp]

theorem TauCeti.UqSl2.clebschGordanProjection_comp_inclusion_self {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) (j : Fin (min m n + 1)) : clebschGordanProjection hq j ∘ₗ clebschGordanInclusion hq j = LinearMap.id

Composing a channel projection with its normalized inclusion gives the identity map.

@[simp]

theorem TauCeti.UqSl2.clebschGordanProjection_comp_inclusion_of_ne {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) {i j : Fin (min m n + 1)} (hij : i ≠ j) : clebschGordanProjection hq i ∘ₗ clebschGordanInclusion hq j = 0

Composing a channel projection with a distinct channel inclusion gives the zero map.

theorem TauCeti.UqSl2.sum_clebschGordanInclusion_projection {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) (x : BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ)) : ∑ j : Fin (min m n + 1), (clebschGordanInclusion hq j) ((clebschGordanProjection hq j) x) = x

The normalized channel projections reconstruct every tensor vector.

theorem TauCeti.UqSl2.sum_clebschGordanInclusion_comp_projection {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) : ∑ j : Fin (min m n + 1), clebschGordanInclusion hq j ∘ₗ clebschGordanProjection hq j = LinearMap.id

The channel endomorphisms resolve the identity as module maps.

theorem TauCeti.UqSl2.clebschGordanInclusion_comp_projection_eq_aeval {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) (j : Fin (min m n + 1)) : ↑ℂ (clebschGordanInclusion hq j ∘ₗ clebschGordanProjection hq j) = (Polynomial.aeval ((Algebra.lsmul ℂ ℂ (BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ))) (casimir q))) (Lagrange.basis Finset.univ (fun (i : Fin (min m n + 1)) => casimirScalar q (↑↑(ε * δ) * q ^ (m + n - 2 * ↑i))) j)

The channel projection followed by its inclusion is the explicit Casimir spectral projection: evaluate the corresponding Lagrange basis polynomial on the Casimir action.

theorem TauCeti.UqSl2.range_clebschGordanInclusion_eq_eigenspace {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) (j : Fin (min m n + 1)) : Submodule.restrictScalars ℂ (clebschGordanInclusion hq j).range = ((Algebra.lsmul ℂ ℂ (BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ))) (casimir q)).eigenspace (casimirScalar q (↑↑(ε * δ) * q ^ (m + n - 2 * ↑j)))

A channel is exactly the Casimir eigenspace with its highest-weight scalar.

theorem TauCeti.UqSl2.clebschGordanInclusion_projection_naturality {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) (j : Fin (min m n + 1)) (φ : Module.End (UqSl2 q) (BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ))) (x : BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ)) : (clebschGordanInclusion hq j) ((clebschGordanProjection hq j) (φ x)) = φ ((clebschGordanInclusion hq j) ((clebschGordanProjection hq j) x))

Channel projection commutes with every module endomorphism of the tensor product.

theorem TauCeti.UqSl2.tensorMap_apply_eq_schurScalar_smul {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) (f : Module.End (UqSl2 q) (LadderModule q m ε)) (g : Module.End (UqSl2 q) (LadderModule q n δ)) (x : BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ)) : (BialgebraModule.tensorMap ℂ (UqSl2 q) f g) x = (LadderModule.schurScalar f * LadderModule.schurScalar g) • x

At a generic parameter, the tensor product of endomorphisms of two signed ladder modules acts by the product of their Schur scalars.

theorem TauCeti.UqSl2.tensorMap_clebschGordanInclusion_vec {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) {m' n' : ℕ} {ε' δ' : ℤˣ} (f : LadderModule q m ε →ₗ[UqSl2 q] LadderModule q m' ε') (g : LadderModule q n δ →ₗ[UqSl2 q] LadderModule q n' δ') {j : Fin (min m n + 1)} {j' : Fin (min m' n' + 1)} (hj : ↑j = ↑j') (l : ℤ) : (BialgebraModule.tensorMap ℂ (UqSl2 q) f g) ((clebschGordanInclusion hq j) (LadderModule.vec q (m + n - 2 * ↑j) (ε * δ) l)) = (LadderModule.schurScalar f * LadderModule.schurScalar g) • (clebschGordanInclusion hq j') (LadderModule.vec q (m' + n' - 2 * ↑j') (ε' * δ') l)

Naturality of the Clebsch–Gordan inclusions on the ladder vectors v_l across arbitrary UqSl2 q-intertwiners f : L_m^ε → L_{m'}^{ε'} and g : L_n^δ → L_{n'}^{δ'} at matching channel indices (j : ℕ) = (j' : ℕ).

theorem TauCeti.UqSl2.clebschGordanInclusion_projection_tensorMap {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) {m' n' : ℕ} {ε' δ' : ℤˣ} (f : LadderModule q m ε →ₗ[UqSl2 q] LadderModule q m' ε') (g : LadderModule q n δ →ₗ[UqSl2 q] LadderModule q n' δ') {j : Fin (min m n + 1)} {j' : Fin (min m' n' + 1)} (hj : ↑j = ↑j') (x : BialgebraModule.Tensor ℂ (UqSl2 q) (LadderModule q m ε) (LadderModule q n δ)) : (clebschGordanInclusion hq j') ((clebschGordanProjection hq j') ((BialgebraModule.tensorMap ℂ (UqSl2 q) f g) x)) = (BialgebraModule.tensorMap ℂ (UqSl2 q) f g) ((clebschGordanInclusion hq j) ((clebschGordanProjection hq j) x))

Naturality of the channel spectral projections clebschGordanInclusion ∘ clebschGordanProjection across arbitrary UqSl2 q-intertwiners f : L_m^ε → L_{m'}^{ε'} and g : L_n^δ → L_{n'}^{δ'} at matching channel indices (j : ℕ) = (j' : ℕ).

theorem TauCeti.UqSl2.clebschGordanProjection_tensorMap_inclusion_vec {q : ℂ} [Fact (q ≠ 0)] {m n : ℕ} {ε δ : ℤˣ} (hq : IsGenericQuantumParameter q) {m' n' : ℕ} {ε' δ' : ℤˣ} (f : LadderModule q m ε →ₗ[UqSl2 q] LadderModule q m' ε') (g : LadderModule q n δ →ₗ[UqSl2 q] LadderModule q n' δ') (j : Fin (min m n + 1)) (j' : Fin (min m' n' + 1)) (l : ℤ) : (clebschGordanProjection hq j') ((BialgebraModule.tensorMap ℂ (UqSl2 q) f g) ((clebschGordanInclusion hq j) (LadderModule.vec q (m + n - 2 * ↑j) (ε * δ) l))) = (if ↑j = ↑j' then LadderModule.schurScalar f * LadderModule.schurScalar g else 0) • LadderModule.vec q (m' + n' - 2 * ↑j') (ε' * δ') l

Naturality of Clebsch–Gordan inclusions and projections across arbitrary factor intertwiners f : L_m^ε → L_{m'}^{ε'} and g : L_n^δ → L_{n'}^{δ'} on the ladder vectors v_l.