The compact real form of `U_q(sl₂)` #

For a real parameter q, the quantized enveloping algebra UqSl2 q carries the star structure of its compact real form: the conjugate-linear antimultiplicative involution with

K* = K, E* = K F, F* = E K⁻¹ (and hence (K⁻¹)* = K⁻¹).

These assignments respect the defining relations because the relations have real coefficients: K F K = q² K K F and E = q⁻² K E K⁻¹ are the conjugated forms of the K E and K F relations, and K F E K⁻¹ = F E turns the starred commutator back into E F - F E.

For a real nonzero q, the star structure is compatible with the Hopf structure: the coproduct is a star homomorphism, Δ(x*) = Δ(x)*, so UqSl2 q is a Hopf star algebra. The general theory of Hopf star algebras then gives ε(x*) = conj (ε x) and S(S(x*)*) = x; consequently the inverse of the antipode is x ↦ S(x*)*. This is the structure with respect to which invariant inner products on its modules are defined, and through which its finite-dimensional modules are compared with the unitary corepresentations of the compact quantum group SU_q(2).

Main definitions #

TauCeti.UqSl2.instStarRing: for a real parameter q, the star structure with K* = K, E* = K F and F* = E K⁻¹; it is conjugate-linear (TauCeti.UqSl2.instStarModule).
TauCeti.UqSl2.instStarCoalgebra: for a real nonzero parameter q, the coproduct is a star homomorphism, making UqSl2 q a Hopf star algebra.

Main results #

TauCeti.UqSl2.star_e, star_f, star_k, star_kInv: the star of the generators.
TauCeti.UqSl2.star_antipode_star: the inverse of the antipode is x ↦ S(x*)*.

Implementation notes #

A conjugate-linear antimultiplicative map out of UqSl2 q is obtained from the universal property of the presentation as a complex algebra map into a private copy of the opposite algebra on which complex scalars act through complex conjugation, built with Algebra.compHom.

References #

A. Klimyk and K. Schmüdgen, Quantum Groups and Their Representations, Springer, 1997, Chapter 3, for the real forms of U_q(sl₂) and their Hopf star structures, there stated for a different coproduct convention.
A. Virelizier, Quantum groups, Sections 2.3--2.4, for the rank-one Hopf convention.

The conjugate opposite algebra #

The star structure #

source

@[instance_reducible]

noncomputable instance TauCeti.UqSl2.instStarRing (q : ℂ) [Fact (IsSelfAdjoint q)] :

StarRing (UqSl2 q)

For a real parameter q, the star structure of the compact real form of UqSl2 q: the conjugate-linear antimultiplicative involution with K* = K, E* = K F and F* = E K⁻¹.

source