Classification of the finite-dimensional simple U_q(sl₂)-modules

At a generic parameter q (nonzero and not a root of unity), every nonzero finite-dimensional module has a highest-weight vector whose lowering string forces its weight to be ε q^m, because the spectrum of K is finite; no diagonalizability of K is assumed. The universal property of LadderModule.lift makes the resulting map from L_m^ε an isomorphism when the target is simple. Together with the pairwise non-isomorphism of the ladder modules, this shows that at a generic parameter every finite-dimensional simple UqSl2 q-module is isomorphic to exactly one L_m^ε.

Main results

• TauCeti.UqSl2.exists_linearEquiv_ladderModule: at a generic parameter, every finite-dimensional simple UqSl2 q-module is isomorphic to a signed ladder module.
• TauCeti.UqSl2.existsUnique_linearEquiv_ladderModule: at a generic parameter, every finite-dimensional simple UqSl2 q-module is isomorphic to L_m^ε for exactly one pair (m, ε).

References

• A. Virelizier, Quantum groups, Section 2.4.
• C. Kassel, Quantum Groups, Graduate Texts in Mathematics 155, Section VI.3.

theorem TauCeti.UqSl2.exists_linearEquiv_ladderModule {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [Fact (q ≠ 0)] [FiniteDimensional ℂ V] [IsSimpleModule (UqSl2 q) V] (hq : IsGenericQuantumParameter q) : ∃ (m : ℕ) (ε : ℤˣ), Nonempty (LadderModule q m ε ≃ₗ[UqSl2 q] V)

At a generic parameter, every finite-dimensional simple UqSl2 q-module is isomorphic to a signed ladder module L_m^ε.

theorem TauCeti.UqSl2.existsUnique_linearEquiv_ladderModule {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [Fact (q ≠ 0)] [FiniteDimensional ℂ V] [IsSimpleModule (UqSl2 q) V] (hq : IsGenericQuantumParameter q) : ∃! p : ℕ × ℤˣ, Nonempty (LadderModule q p.1 p.2 ≃ₗ[UqSl2 q] V)

Classification of finite-dimensional simple U_q(sl₂)-modules. At a generic parameter, every finite-dimensional simple UqSl2 q-module is isomorphic to L_m^ε for exactly one natural number m and sign ε.