Submodules and simple quotients of the Verma modules of U_q(sl₂)

At a generic parameter q (nonzero and not a root of unity) and for a nonzero weight μ, this file determines all submodules of the Verma module M(μ).

The vectors v_j = F^j v₀ form a basis of M(μ) on which K acts diagonally with the pairwise distinct weights q^(-2j) μ, so a submodule contains every v_j occurring in one of its elements. Since F v_j = v_(j + 1), the indices of the v_j lying in a nonzero submodule N form a final segment {j | n ≤ j}, and N is generated by v_n. Since E v_n is a multiple of v_(n - 1), which does not lie in N, the vector v_n is killed by E. Conversely, a vector v_n killed by E induces an injective module map M(q^(-2n) μ) → M(μ) sending v₀ to v_n, whose image, the submodule generated by v_n, is spanned by the v_j with n ≤ j.

Combined with the singular-vector criterion VermaModule.e_smul_vec_succ_eq_zero_iff, this gives:

• if μ is not a signed highest weight ± q^m, then M(μ) is simple;
• if μ = ε q^m for a sign ε, then the submodules of M(μ) are 0, M(μ) and the submodule N generated by v_(m + 1), which is isomorphic to M(q^(-2(m + 1)) μ). The submodule N is maximal, and the simple quotient M(ε q^m) ⧸ N is isomorphic to the signed ladder module L_m^ε.

Main definitions

• TauCeti.UqSl2.VermaModule.singularMap: the module map M(q^(-2n) μ) → M(μ) sending v₀ to a vector v_n killed by E.
• TauCeti.UqSl2.VermaModule.ladderModuleEquivQuotient: at a generic parameter, the isomorphism L_m^ε ≃ M(ε q^m) ⧸ N sending v₀ to the class of v₀.

Main results

• TauCeti.UqSl2.VermaModule.singularMap_injective, range_singularMap: the map induced by v_n is injective, with image the submodule generated by v_n.
• TauCeti.UqSl2.VermaModule.vec_mem_of_basis_repr_ne_zero: at a generic parameter, a submodule of M(μ) contains every v_j occurring in one of its elements.
• TauCeti.UqSl2.VermaModule.eq_bot_or_exists_eq_span_singleton_vec: at a generic parameter, every nonzero submodule of M(μ) is generated by a vector v_n killed by E.
• TauCeti.UqSl2.VermaModule.isSimpleModule_iff: at a generic parameter, M(μ) is simple exactly when μ² ≠ q^(2m) for every m.
• TauCeti.UqSl2.VermaModule.eq_bot_or_eq_span_singleton_vec_succ_or_eq_top and TauCeti.UqSl2.VermaModule.isCoatom_span_singleton_vec_succ: the submodules of M(ε q^m), and maximality of the one generated by v_(m + 1).

References

• C. Kassel, Quantum Groups, Graduate Texts in Mathematics 155, Section VI.3, for the Verma modules of U_q(sl₂), their simplicity criterion and their finite-dimensional quotients.
• A. Virelizier, Quantum groups, Sections 2.3--2.4, for the rank-one convention used here.

Maps between Verma modules

noncomputable def TauCeti.UqSl2.VermaModule.singularMap {q μ : ℂ} {n : ℕ} (he : e q • vec q μ n = 0) : VermaModule q ((q⁻¹ ^ 2) ^ n * μ) →ₗ[UqSl2 q] VermaModule q μ

For a vector v_n of M(μ) killed by E, the module map M(q^(-2n) μ) → M(μ) sending v₀ to v_n.

@[simp]

theorem TauCeti.UqSl2.VermaModule.singularMap_vec {q μ : ℂ} {n : ℕ} (he : e q • vec q μ n = 0) (i : ℕ) : (singularMap he) (vec q ((q⁻¹ ^ 2) ^ n * μ) i) = vec q μ (i + n)

The map induced by v_n sends v_i to v_(i + n).

theorem TauCeti.UqSl2.VermaModule.range_singularMap {q μ : ℂ} {n : ℕ} (he : e q • vec q μ n = 0) : (singularMap he).range = UqSl2 q ∙ vec q μ n

The image of the map induced by v_n is the submodule generated by v_n.

theorem TauCeti.UqSl2.VermaModule.singularMap_injective {q μ : ℂ} {n : ℕ} (he : e q • vec q μ n = 0) (hq : q ≠ 0) (hμ : μ ≠ 0) : Function.Injective ⇑(singularMap he)

For nonzero q and μ, the map induced by v_n is injective.

theorem TauCeti.UqSl2.VermaModule.vec_mem_span_singleton_vec_iff {q μ : ℂ} {n : ℕ} (he : e q • vec q μ n = 0) (hq : q ≠ 0) (hμ : μ ≠ 0) {j : ℕ} : vec q μ j ∈ UqSl2 q ∙ vec q μ n ↔ n ≤ j

For nonzero q and μ, the submodule generated by a vector v_n killed by E contains exactly the v_j with n ≤ j.

The submodules of a Verma module

theorem TauCeti.UqSl2.VermaModule.vec_mem_of_basis_repr_ne_zero {q μ : ℂ} (hq : IsGenericQuantumParameter q) (hμ : μ ≠ 0) {N : Submodule (UqSl2 q) (VermaModule q μ)} {x : VermaModule q μ} (hx : x ∈ N) {j : ℕ} (hj : ((basis ⋯ hμ).repr x) j ≠ 0) : vec q μ j ∈ N

At a generic parameter and for nonzero μ, a submodule of M(μ) contains every vector v_j occurring with a nonzero coefficient in one of its elements.

theorem TauCeti.UqSl2.VermaModule.vec_mem_of_vec_succ_mem {q μ : ℂ} {N : Submodule (UqSl2 q) (VermaModule q μ)} {j : ℕ} (hN : vec q μ (j + 1) ∈ N) (he : e q • vec q μ (j + 1) ≠ 0) : vec q μ j ∈ N

A submodule of M(μ) containing v_(j + 1) contains v_j, unless E kills v_(j + 1).

theorem TauCeti.UqSl2.VermaModule.eq_bot_or_exists_eq_span_singleton_vec {q μ : ℂ} (hq : IsGenericQuantumParameter q) (hμ : μ ≠ 0) (N : Submodule (UqSl2 q) (VermaModule q μ)) : N = ⊥ ∨ ∃ (n : ℕ), e q • vec q μ n = 0 ∧ N = UqSl2 q ∙ vec q μ n

The submodules of a Verma module. At a generic parameter and for nonzero μ, every nonzero submodule of M(μ) is generated by a vector v_n killed by E.

theorem TauCeti.UqSl2.VermaModule.isSimpleModule_iff {q μ : ℂ} (hq : IsGenericQuantumParameter q) (hμ : μ ≠ 0) : IsSimpleModule (UqSl2 q) (VermaModule q μ) ↔ ∀ (m : ℕ), μ ^ 2 ≠ q ^ (2 * m)

Simplicity of Verma modules. At a generic parameter and for nonzero μ, the Verma module M(μ) is simple exactly when μ² ≠ q^(2m) for every m, that is, when μ is not a signed highest weight ± q^m.

Verma modules with a signed highest weight

theorem TauCeti.UqSl2.VermaModule.e_smul_vec_succ_eq_zero {q : ℂ} {m : ℕ} {ε : ℤˣ} : e q • vec q (↑↑ε * q ^ m) (m + 1) = 0

The vector v_(m + 1) of M(ε q^m) is killed by E.

theorem TauCeti.UqSl2.VermaModule.eq_bot_or_eq_span_singleton_vec_succ_or_eq_top {q : ℂ} {m : ℕ} {ε : ℤˣ} (hq : IsGenericQuantumParameter q) (N : Submodule (UqSl2 q) (VermaModule q (↑↑ε * q ^ m))) : N = ⊥ ∨ N = UqSl2 q ∙ vec q (↑↑ε * q ^ m) (m + 1) ∨ N = ⊤

The submodules of M(ε q^m). At a generic parameter, the only submodules of M(ε q^m) are 0, the submodule generated by v_(m + 1), and M(ε q^m) itself.

theorem TauCeti.UqSl2.VermaModule.isCoatom_span_singleton_vec_succ {q : ℂ} {m : ℕ} {ε : ℤˣ} (hq : IsGenericQuantumParameter q) : IsCoatom (UqSl2 q ∙ vec q (↑↑ε * q ^ m) (m + 1))

At a generic parameter, the submodule of M(ε q^m) generated by v_(m + 1) is a maximal submodule.

The simple quotient

noncomputable def TauCeti.UqSl2.VermaModule.ladderModuleEquivQuotient {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] (hq : IsGenericQuantumParameter q) : LadderModule q m ε ≃ₗ[UqSl2 q] VermaModule q (↑↑ε * q ^ m) ⧸ UqSl2 q ∙ vec q (↑↑ε * q ^ m) (m + 1)

The simple quotient of M(ε q^m). At a generic parameter, the quotient of M(ε q^m) by the submodule generated by v_(m + 1) is isomorphic to the signed ladder module L_m^ε, by the module map sending v₀ to the class of v₀.

@[simp]

theorem TauCeti.UqSl2.VermaModule.ladderModuleEquivQuotient_vec_zero {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] (hq : IsGenericQuantumParameter q) : (ladderModuleEquivQuotient hq) (LadderModule.vec q m ε 0) = Submodule.Quotient.mk (vec q (↑↑ε * q ^ m) 0)

The isomorphism L_m^ε ≃ M(ε q^m) ⧸ N sends v₀ to the class of v₀.

@[simp]

theorem TauCeti.UqSl2.VermaModule.ladderModuleEquivQuotient_symm_mk_vec_zero {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] (hq : IsGenericQuantumParameter q) : (ladderModuleEquivQuotient hq).symm (Submodule.Quotient.mk (vec q (↑↑ε * q ^ m) 0)) = LadderModule.vec q m ε 0

The inverse isomorphism M(ε q^m) ⧸ N ≃ L_m^ε sends the class of v₀ to v₀.