Locally finite U_q(sl₂)-modules

A UqSl2 q-module is locally finite when each vector generates a finite-dimensional submodule; no finiteness of the whole module is assumed. At a generic parameter q (nonzero and not a root of unity), the locally finite modules are exactly the algebraic direct sums of signed ladder modules L_m^ε, with arbitrary, possibly infinite, index sets.

Each cyclic submodule of a locally finite module is finite-dimensional, hence semisimple by complete reducibility of finite-dimensional modules, and a module spanned by semisimple submodules is semisimple. A semisimple module is a direct sum of simple submodules; in a locally finite module these are cyclic, hence finite-dimensional, hence each isomorphic to one L_m^ε by the classification of finite-dimensional simple modules. Conversely, a direct sum of finite-dimensional modules is locally finite.

The decomposition can be made canonical. Since the L_m^ε are pairwise non-isomorphic finite-dimensional simple modules over ℂ, evaluation v ⊗ φ ↦ φ v identifies a locally finite module V with ⨁_(m,ε) L_m^ε ⊗ Hom_U(L_m^ε, V), compatibly with the action of UqSl2 q on the left tensor factors. The multiplicity of L_m^ε in V is thus the space Hom_U(L_m^ε, V), with no choice of decomposition.

Main results

• TauCeti.UqSl2.isSemisimpleModule_of_isLocallyFiniteModule: at a generic parameter, every locally finite UqSl2 q-module is semisimple.
• TauCeti.UqSl2.isLocallyFiniteModule_iff_exists_linearEquiv_dfinsupp_ladderModule: at a generic parameter, a UqSl2 q-module is locally finite exactly when it is isomorphic to a direct sum ⨁ᵢ L_(mᵢ)^(εᵢ) of signed ladder modules.
• TauCeti.UqSl2.ladderModuleTensorHomEquiv: at a generic parameter, the evaluation isomorphism ⨁_(m,ε) L_m^ε ⊗ Hom_U(L_m^ε, V) ≃ V for a locally finite module V, natural in V (TauCeti.UqSl2.ladderModuleTensorHomEquiv_map), so that End_U(V) acts on the multiplicity spaces alone (TauCeti.UqSl2.ladderModuleTensorHomEquiv_symm_apply_map).

References

• A. Virelizier, Quantum groups, Sections 2.3--2.4, for the rank-one conventions.

theorem TauCeti.UqSl2.isSemisimpleModule_of_isLocallyFiniteModule {q : ℂ} {V : Type u} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (hq : IsGenericQuantumParameter q) [IsLocallyFiniteModule ℂ (UqSl2 q) V] : IsSemisimpleModule (UqSl2 q) V

At a generic parameter, every locally finite UqSl2 q-module is semisimple.

theorem TauCeti.UqSl2.exists_e_pow_smul_eq_zero_of_isLocallyFiniteModule {q : ℂ} {V : Type u} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (hq : IsGenericQuantumParameter q) [IsLocallyFiniteModule ℂ (UqSl2 q) V] (v : V) : ∃ (n : ℕ), e q ^ n • v = 0

At a generic parameter, E acts locally nilpotently on a locally finite module.

theorem TauCeti.UqSl2.exists_f_pow_smul_eq_zero_of_isLocallyFiniteModule {q : ℂ} {V : Type u} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (hq : IsGenericQuantumParameter q) [IsLocallyFiniteModule ℂ (UqSl2 q) V] (v : V) : ∃ (n : ℕ), f q ^ n • v = 0

At a generic parameter, F acts locally nilpotently on a locally finite module.

theorem TauCeti.UqSl2.exists_linearEquiv_dfinsupp_ladderModule {q : ℂ} {V : Type u} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [Fact (q ≠ 0)] (hq : IsGenericQuantumParameter q) [IsLocallyFiniteModule ℂ (UqSl2 q) V] : ∃ (ι : Type u) (m : ι → ℕ) (ε : ι → ℤˣ), Nonempty (V ≃ₗ[UqSl2 q] Π₀ (i : ι), LadderModule q (m i) (ε i))

At a generic parameter, every locally finite UqSl2 q-module is isomorphic to a direct sum of signed ladder modules L_m^ε.

theorem TauCeti.UqSl2.exists_linearEquiv_pi_ladderModule {q : ℂ} {V : Type u} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [Fact (q ≠ 0)] (hq : IsGenericQuantumParameter q) [FiniteDimensional ℂ V] : ∃ (n : ℕ) (m : Fin n → ℕ) (ε : Fin n → ℤˣ), Nonempty (V ≃ₗ[UqSl2 q] (i : Fin n) → LadderModule q (m i) (ε i))

At a generic parameter, every finite-dimensional UqSl2 q-module is isomorphic to a finite product ∏ᵢ L_(mᵢ)^(εᵢ) of signed ladder modules.

theorem TauCeti.UqSl2.isLocallyFiniteModule_iff_exists_linearEquiv_dfinsupp_ladderModule {q : ℂ} {V : Type u} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [Fact (q ≠ 0)] (hq : IsGenericQuantumParameter q) : IsLocallyFiniteModule ℂ (UqSl2 q) V ↔ ∃ (ι : Type u) (m : ι → ℕ) (ε : ι → ℤˣ), Nonempty (V ≃ₗ[UqSl2 q] Π₀ (i : ι), LadderModule q (m i) (ε i))

At a generic parameter, a UqSl2 q-module is locally finite exactly when it is isomorphic to a direct sum of signed ladder modules L_m^ε.

noncomputable def TauCeti.UqSl2.ladderModuleTensorHomEquiv {q : ℂ} {V : Type u} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [Fact (q ≠ 0)] (hq : IsGenericQuantumParameter q) [IsLocallyFiniteModule ℂ (UqSl2 q) V] : (Π₀ (p : ℕ × ℤˣ), TensorProduct ℂ (LadderModule q p.1 p.2) (LadderModule q p.1 p.2 →ₗ[UqSl2 q] V)) ≃ₗ[UqSl2 q] V

The evaluation isomorphism. At a generic parameter, a locally finite UqSl2 q-module V is the direct sum over (m, ε) of L_m^ε ⊗ Hom_U(L_m^ε, V), by v ⊗ φ ↦ φ v. Here UqSl2 q acts on the left tensor factors, and the multiplicity spaces Hom_U(L_m^ε, V) may be infinite-dimensional.

@[simp]

theorem TauCeti.UqSl2.ladderModuleTensorHomEquiv_single_tmul {q : ℂ} {V : Type u} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [Fact (q ≠ 0)] (hq : IsGenericQuantumParameter q) [IsLocallyFiniteModule ℂ (UqSl2 q) V] (p : ℕ × ℤˣ) (v : LadderModule q p.1 p.2) (φ : LadderModule q p.1 p.2 →ₗ[UqSl2 q] V) : (ladderModuleTensorHomEquiv hq) (DFinsupp.single p (v ⊗ₜ[ℂ] φ)) = φ v

The evaluation isomorphism sends v ⊗ φ in the (m, ε) summand to φ v.

theorem TauCeti.UqSl2.ladderModuleTensorHomEquiv_map {q : ℂ} {V : Type u} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [Fact (q ≠ 0)] {W : Type u_1} [AddCommGroup W] [Module ℂ W] [Module (UqSl2 q) W] [IsScalarTower ℂ (UqSl2 q) W] (hq : IsGenericQuantumParameter q) [IsLocallyFiniteModule ℂ (UqSl2 q) V] [IsLocallyFiniteModule ℂ (UqSl2 q) W] (g : V →ₗ[UqSl2 q] W) (x : Π₀ (p : ℕ × ℤˣ), TensorProduct ℂ (LadderModule q p.1 p.2) (LadderModule q p.1 p.2 →ₗ[UqSl2 q] V)) : (ladderModuleTensorHomEquiv hq) ((DFinsupp.mapRange.linearMap fun (p : ℕ × ℤˣ) => TensorProduct.AlgebraTensorModule.map LinearMap.id (LinearMap.compRight ℂ g)) x) = g ((ladderModuleTensorHomEquiv hq) x)

The evaluation isomorphism is natural. A UqSl2 q-linear map g : V → W of locally finite modules acts on each multiplicity space Hom_U(L_m^ε, V) by postcomposition, and trivially on the L_m^ε.

@[simp]

theorem TauCeti.UqSl2.ladderModuleTensorHomEquiv_symm_apply_map {q : ℂ} {V : Type u} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [Fact (q ≠ 0)] {W : Type u_1} [AddCommGroup W] [Module ℂ W] [Module (UqSl2 q) W] [IsScalarTower ℂ (UqSl2 q) W] (hq : IsGenericQuantumParameter q) [IsLocallyFiniteModule ℂ (UqSl2 q) V] [IsLocallyFiniteModule ℂ (UqSl2 q) W] (g : V →ₗ[UqSl2 q] W) (v : V) : (ladderModuleTensorHomEquiv hq).symm (g v) = (DFinsupp.mapRange.linearMap fun (p : ℕ × ℤˣ) => TensorProduct.AlgebraTensorModule.map LinearMap.id (LinearMap.compRight ℂ g)) ((ladderModuleTensorHomEquiv hq).symm v)

The commutant acts on the multiplicity spaces. Through the inverse evaluation isomorphisms, a UqSl2 q-linear map g : V → W of locally finite modules is 1 ⊗ (g ∘ ·) on every summand; for W = V this is the action of End_U(V) on the Hom_U(L_m^ε, V).