Verma modules of U_q(sl₂)

For complex numbers q and μ, the Verma module M(μ) of UqSl2 q is the quotient of UqSl2 q by the left ideal generated by E and K - μ. The class v₀ of 1 is a vector of weight μ killed by E, and M(μ) is the universal module generated by such a vector: for every vector v of weight μ killed by E in a UqSl2 q-module there is a unique module map M(μ) → V sending v₀ to v.

Writing v_j = F^j v₀, the action of the generators is

• F v_j = v_(j + 1),
• K v_j = q^(-2j) μ v_j and K⁻¹ v_j = q^(2j) μ⁻¹ v_j,
• E v₀ = 0 and E v_(j + 1) = [j + 1]_q (q^(-j) μ - q^j μ⁻¹) / (q - q⁻¹) v_j,

where [r]_q is the symmetric quantum integer. When q and μ are nonzero, the vectors v_j form a basis of M(μ).

The coefficient of E shows where M(μ) acquires singular vectors: at a generic parameter, E v_(j + 1) = 0 exactly when μ² = q^(2j), that is, when μ = ± q^j is the highest weight of one of the signed simple modules L_j^±. In that case v_(j + 1) is a vector of weight q^(-2(j + 1)) μ killed by E inside M(μ).

Main definitions

• TauCeti.UqSl2.vermaIdeal q μ: the left ideal generated by E and K - μ.
• TauCeti.UqSl2.VermaModule q μ: the Verma module M(μ).
• TauCeti.UqSl2.VermaModule.vec q μ j: the vector v_j = F^j v₀.
• TauCeti.UqSl2.VermaModule.lift: the module map determined by a vector of weight μ killed by E.
• TauCeti.UqSl2.VermaModule.basis: the basis (v_j)_(j ∈ ℕ), for nonzero q and μ.

Main results

• TauCeti.UqSl2.VermaModule.e_smul_vec_succ, f_smul_vec, k_smul_vec, kInv_smul_vec: the action of the generators.
• TauCeti.UqSl2.VermaModule.lift_vec_zero, TauCeti.UqSl2.VermaModule.hom_ext: the universal property.
• TauCeti.UqSl2.VermaModule.span_singleton_vec_zero: M(μ) is generated by v₀.
• TauCeti.UqSl2.VermaModule.span_vec_eq_top, linearIndependent_vec: the vectors v_j span M(μ), and are linearly independent for nonzero q and μ.
• TauCeti.UqSl2.VermaModule.e_smul_vec_succ_eq_zero_iff: the singular-vector criterion.

References

• C. Kassel, Quantum Groups, Graduate Texts in Mathematics 155, Section VI.3, for the Verma modules of U_q(sl₂) and the action of the generators on the lowering string.
• A. Virelizier, Quantum groups, Sections 2.3--2.4, for the rank-one convention used here.

def TauCeti.UqSl2.vermaIdeal (q μ : ℂ) : Submodule (UqSl2 q) (UqSl2 q)

The left ideal of UqSl2 q generated by E and K - μ.

theorem TauCeti.UqSl2.e_mem_vermaIdeal {q : ℂ} (μ : ℂ) : e q ∈ vermaIdeal q μ

The raising generator lies in the Verma ideal.

theorem TauCeti.UqSl2.k_sub_algebraMap_mem_vermaIdeal {q : ℂ} (μ : ℂ) : k q - (algebraMap ℂ (UqSl2 q)) μ ∈ vermaIdeal q μ

The weight relation K - μ lies in the Verma ideal.

def TauCeti.UqSl2.VermaModule (q μ : ℂ) : Type

The Verma module M(μ) of UqSl2 q: the quotient of UqSl2 q by the left ideal generated by E and K - μ.

@[instance_reducible]

instance TauCeti.UqSl2.VermaModule.instAddCommGroup (q μ : ℂ) : AddCommGroup (VermaModule q μ)

@[instance_reducible]

instance TauCeti.UqSl2.VermaModule.instModule (q μ : ℂ) : Module (UqSl2 q) (VermaModule q μ)

@[instance_reducible]

instance TauCeti.UqSl2.VermaModule.instModuleComplex (q μ : ℂ) : Module ℂ (VermaModule q μ)

instance TauCeti.UqSl2.VermaModule.instIsScalarTowerComplex (q μ : ℂ) : IsScalarTower ℂ (UqSl2 q) (VermaModule q μ)

def TauCeti.UqSl2.VermaModule.mk (q μ : ℂ) : UqSl2 q →ₗ[UqSl2 q] VermaModule q μ

The quotient map UqSl2 q → M(μ).

theorem TauCeti.UqSl2.VermaModule.mk_surjective {q μ : ℂ} : Function.Surjective ⇑(mk q μ)

Every vector of M(μ) is the class of an element of UqSl2 q.

@[simp]

theorem TauCeti.UqSl2.VermaModule.mk_eq_zero_iff {q μ : ℂ} {a : UqSl2 q} : (mk q μ) a = 0 ↔ a ∈ vermaIdeal q μ

The class of an element of UqSl2 q vanishes exactly when it lies in the Verma ideal.

def TauCeti.UqSl2.VermaModule.vec (q μ : ℂ) (j : ℕ) : VermaModule q μ

The vector v_j = F^j v₀ of M(μ), where v₀ is the class of 1.

theorem TauCeti.UqSl2.VermaModule.mk_eq_smul_vec_zero {q μ : ℂ} (a : UqSl2 q) : (mk q μ) a = a • vec q μ 0

The class of a is a v₀.

theorem TauCeti.UqSl2.VermaModule.vec_eq_f_pow_smul {q μ : ℂ} (j : ℕ) : vec q μ j = f q ^ j • vec q μ 0

The vector v_j is F^j v₀.

theorem TauCeti.UqSl2.VermaModule.span_singleton_vec_zero (q μ : ℂ) : UqSl2 q ∙ vec q μ 0 = ⊤

The Verma module M(μ) is generated by its highest vector v₀.

theorem TauCeti.UqSl2.VermaModule.f_pow_smul_vec {q μ : ℂ} (n j : ℕ) : f q ^ n • vec q μ j = vec q μ (n + j)

The action of the powers of F: F^n v_j = v_(n + j).

@[simp]

theorem TauCeti.UqSl2.VermaModule.f_smul_vec {q μ : ℂ} (j : ℕ) : f q • vec q μ j = vec q μ (j + 1)

The action of F: F v_j = v_(j + 1).

@[simp]

theorem TauCeti.UqSl2.VermaModule.e_smul_vec_zero {q μ : ℂ} : e q • vec q μ 0 = 0

The highest vector is killed by E.

theorem TauCeti.UqSl2.VermaModule.k_smul_vec_zero {q μ : ℂ} : k q • vec q μ 0 = μ • vec q μ 0

The highest vector has weight μ.

theorem TauCeti.UqSl2.VermaModule.kInv_smul_vec_zero {q μ : ℂ} : kInv q • vec q μ 0 = μ⁻¹ • vec q μ 0

The action of K⁻¹ on the highest vector.

@[simp]

theorem TauCeti.UqSl2.VermaModule.k_smul_vec {q μ : ℂ} (j : ℕ) : k q • vec q μ j = ((q⁻¹ ^ 2) ^ j * μ) • vec q μ j

The action of K: K v_j = q^(-2j) μ v_j.

@[simp]

theorem TauCeti.UqSl2.VermaModule.kInv_smul_vec {q μ : ℂ} (j : ℕ) : kInv q • vec q μ j = ((q ^ 2) ^ j * μ⁻¹) • vec q μ j

The action of K⁻¹: K⁻¹ v_j = q^(2j) μ⁻¹ v_j.

theorem TauCeti.UqSl2.VermaModule.vec_mem_weightSpace {q μ : ℂ} (j : ℕ) : vec q μ j ∈ weightSpace q (VermaModule q μ) ((q⁻¹ ^ 2) ^ j * μ)

The vector v_j has weight q^(-2j) μ.

@[simp]

theorem TauCeti.UqSl2.VermaModule.e_smul_vec_succ {q μ : ℂ} (j : ℕ) : e q • vec q μ (j + 1) = (quantumInteger q (↑j + 1) * (q⁻¹ ^ j * μ - q ^ j * μ⁻¹) / (q - q⁻¹)) • vec q μ j

The action of E: E v_(j + 1) = [j + 1]_q (q^(-j) μ - q^j μ⁻¹) / (q - q⁻¹) v_j.

Spanning

theorem TauCeti.UqSl2.VermaModule.span_vec_eq_top {q μ : ℂ} : Submodule.span ℂ (Set.range (vec q μ)) = ⊤

The vectors v_j span M(μ).

The universal property

def TauCeti.UqSl2.VermaModule.lift {q μ : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {v : V} (hv : v ∈ weightSpace q V μ) (he : e q • v = 0) : VermaModule q μ →ₗ[UqSl2 q] V

The UqSl2 q-module map M(μ) → V determined by a vector v of weight μ killed by E. It sends v₀ to v.

@[simp]

theorem TauCeti.UqSl2.VermaModule.lift_mk {q μ : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {v : V} (hv : v ∈ weightSpace q V μ) (he : e q • v = 0) (a : UqSl2 q) : (lift hv he) ((mk q μ) a) = a • v

The map induced by v sends the class of a to a v.

theorem TauCeti.UqSl2.VermaModule.lift_vec {q μ : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {v : V} (hv : v ∈ weightSpace q V μ) (he : e q • v = 0) (j : ℕ) : (lift hv he) (vec q μ j) = f q ^ j • v

The map induced by v sends v_j to F^j v.

@[simp]

theorem TauCeti.UqSl2.VermaModule.lift_vec_zero {q μ : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {v : V} (hv : v ∈ weightSpace q V μ) (he : e q • v = 0) : (lift hv he) (vec q μ 0) = v

The map induced by v sends the highest vector v₀ to v.

theorem TauCeti.UqSl2.VermaModule.hom_ext {q μ : ℂ} {V : Type u_1} [AddCommGroup V] [Module (UqSl2 q) V] {φ ψ : VermaModule q μ →ₗ[UqSl2 q] V} (h : φ (vec q μ 0) = ψ (vec q μ 0)) : φ = ψ

A UqSl2 q-module map out of M(μ) is determined by its value at the highest vector v₀.

Linear independence

For nonzero q and μ, the vectors v_j are linearly independent, so together with spanning they form a basis of M(μ).

theorem TauCeti.UqSl2.VermaModule.linearIndependent_vec {q μ : ℂ} (hq : q ≠ 0) (hμ : μ ≠ 0) : LinearIndependent ℂ (vec q μ)

For nonzero q and μ, the vectors v_j are linearly independent.

The basis

noncomputable def TauCeti.UqSl2.VermaModule.basis {q μ : ℂ} (hq : q ≠ 0) (hμ : μ ≠ 0) : Module.Basis ℕ ℂ (VermaModule q μ)

For nonzero q and μ, the basis (v_j)_(j ∈ ℕ) of M(μ), where v_j = F^j v₀.

@[simp]

theorem TauCeti.UqSl2.VermaModule.coe_basis {q μ : ℂ} (hq : q ≠ 0) (hμ : μ ≠ 0) : ⇑(basis hq hμ) = vec q μ

The basis vectors of M(μ) are the vectors v_j.

theorem TauCeti.UqSl2.VermaModule.vec_ne_zero {q μ : ℂ} (hq : q ≠ 0) (hμ : μ ≠ 0) (j : ℕ) : vec q μ j ≠ 0

For nonzero q and μ, every vector v_j is nonzero.

Singular vectors

theorem TauCeti.UqSl2.VermaModule.e_smul_vec_succ_eq_zero_iff {q μ : ℂ} (hq : IsGenericQuantumParameter q) (hμ : μ ≠ 0) (j : ℕ) : e q • vec q μ (j + 1) = 0 ↔ μ ^ 2 = q ^ (2 * j)

The singular-vector criterion: at a generic parameter and for nonzero μ, the vector v_(j + 1) is killed by E exactly when μ² = q^(2j).