The triangular decomposition of `U_q(sl₂)` #

For a nonzero parameter q, write U⁻, U⁰ and U⁺ for the subalgebras of UqSl2 q generated by F, by K and K⁻¹, and by E. This file proves:

the subalgebra inclusions: evaluation at F and at E is injective on the polynomial ring ℂ[X], so F and E are transcendental over ℂ, and evaluation at the unit K is injective on the Laurent polynomial ring ℂ[T, T⁻¹];
the triangular decomposition: multiplication p ⊗ r ⊗ s ↦ p(F) * r(K) * s(E) is a linear isomorphism ℂ[X] ⊗ ℂ[T, T⁻¹] ⊗ ℂ[X] ≃ UqSl2 q, i.e. U⁻ ⊗ U⁰ ⊗ U⁺ ≃ U_q(sl₂).

Both statements are repackagings of the PBW basis F ^ a * K ^ b * E ^ c: the tensor product of the monomial bases of the three factors is sent to it. The decomposition is the form in which the PBW theorem enters highest-weight theory: an element is determined by its components in U⁻ ⊗ U⁰ ⊗ U⁺, which is how central elements are reduced to their U⁰ part.

Main definitions #

TauCeti.UqSl2.triangularEquiv: the multiplication isomorphism ℂ[X] ⊗[ℂ] (ℂ[T;T⁻¹] ⊗[ℂ] ℂ[X]) ≃ₗ[ℂ] UqSl2 q.

Main results #

TauCeti.UqSl2.triangularEquiv_tmul: its value p(F) * r(K) * s(E) on a pure tensor.
TauCeti.UqSl2.triangularEquiv_symm_pbwBasis: its inverse sends the PBW basis vector F ^ a * K ^ b * E ^ c to the monomial tensor X ^ a ⊗ T b ⊗ X ^ c.
TauCeti.UqSl2.transcendental_f and TauCeti.UqSl2.transcendental_e: F and E generate polynomial subalgebras.
TauCeti.UqSl2.laurentEval_kUnit_injective: K generates a Laurent polynomial subalgebra.

References #

J. C. Jantzen, Lectures on Quantum Groups, Graduate Studies in Mathematics 6, Chapter 1, for the rank-one triangular decomposition.
C. Kassel, Quantum Groups, Graduate Texts in Mathematics 155, Section VI.1, for the PBW basis it is derived from.

The subalgebra inclusions #

source

theorem TauCeti.UqSl2.transcendental_f (q : ℂ) [Fact (q ≠ 0)] :

Transcendental ℂ (f q)

The lowering generator F is transcendental over ℂ: evaluation at F is injective, so it identifies ℂ[X] with the subalgebra U⁻ generated by F.

source

theorem TauCeti.UqSl2.transcendental_e (q : ℂ) [Fact (q ≠ 0)] :

Transcendental ℂ (e q)

The raising generator E is transcendental over ℂ: evaluation at E is injective, so it identifies ℂ[X] with the subalgebra U⁺ generated by E.

source

theorem TauCeti.UqSl2.laurentEval_kUnit_injective (q : ℂ) [Fact (q ≠ 0)] :

Function.Injective ⇑(laurentEval (kUnit q))

Evaluation at the unit K is injective, so it identifies the Laurent polynomial ring ℂ[T, T⁻¹] with the subalgebra U⁰ generated by K and K⁻¹.