Complete reducibility of finite-dimensional U_q(sl₂)-modules

At a generic parameter q (nonzero and not a root of unity), every finite-dimensional UqSl2 q-module is semisimple. No diagonalizability of K is assumed.

Along the way, taking generalized weight spaces is shown to be exact.

Implementation notes

The proof splits a finite-dimensional module into the generalized eigenspaces of the central Casimir element Ω. Every highest-weight vector in such a Casimir block has weight ε q^m for one fixed pair (m, ε), so E kills the generalized weight space W of weight ε q^m. By the highest-weight results F^(m+1) vanishes on W and K acts on W by the scalar ε q^m (TauCeti.UqSl2.mem_weightSpace_of_e_smul_eq_zero). Every vector of W is therefore the image of v₀ under a module map from the ladder module L_m^ε, and these images span a semisimple submodule U ⊇ W. Taking generalized weight spaces is exact, so the quotient by U has no generalized weight ε q^m; being a Casimir block with the same scalar, it is zero.

Main results

• TauCeti.UqSl2.e_smul_eq_zero_of_casimirBlock_eq_top: in a module equal to its Casimir block for the Casimir scalar of ε q^m, E kills the generalized weight space of weight ε q^m.
• TauCeti.UqSl2.isSemisimpleModule_of_finiteDimensional: at a generic parameter, every finite-dimensional UqSl2 q-module is semisimple.

References

• A. Virelizier, Quantum groups, Sections 2.3--2.4.
• C. Kassel, Quantum Groups, Graduate Texts in Mathematics 155, Chapter VII, for the semisimplicity of finite-dimensional modules at a generic parameter.

Complete reducibility

theorem TauCeti.UqSl2.e_smul_eq_zero_of_casimirBlock_eq_top {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [FiniteDimensional ℂ V] (hq : IsGenericQuantumParameter q) {m : ℕ} {ε : ℤˣ} (hc : casimirBlock q V (casimirScalar q (↑↑ε * q ^ m)) = ⊤) {w : V} (hw : w ∈ genWeightSpace q V (↑↑ε * q ^ m)) : e q • w = 0

In a module equal to its Casimir block for the Casimir scalar of ε q^m, every highest weight is ε q^m, so E kills the generalized weight space of weight ε q^m.

theorem TauCeti.UqSl2.isSemisimpleModule_of_finiteDimensional {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [FiniteDimensional ℂ V] (hq : IsGenericQuantumParameter q) : IsSemisimpleModule (UqSl2 q) V

Complete reducibility. At a generic parameter, every finite-dimensional UqSl2 q-module is semisimple.