Documentation

TauCeti.QuantumGroups.UqSl2.HighestWeight

Finite highest-weight strings for U_q(sl₂) #

At a generic parameter, a nonzero highest-weight vector in a finite-dimensional module has a finite nonzero lowering string. Commuting E past the first vanishing power of F forces its weight to be ε q^m for a sign ε. This is the numerical step in the classification of finite-dimensional simple modules by the signed ladder modules. Conversely, the lowering string of a highest-weight vector of weight ε q^m in a finite-dimensional module stops after m + 1 steps, so such a vector generates a copy of the signed ladder module L_m^ε.

The vanishing holds more generally for a generalized weight vector w of weight ε q^m killed by E: the commutator formula E F^(r+1) = F^(r+1) E + [r+1]_q F^r (q^(-r) K - q^r K⁻¹) / (q - q⁻¹) shows that F^r w ≠ 0 for w ≠ 0 and r ≤ m, and that F^(m+1) w = 0. Moreover K acts on such a w by the scalar ε q^m, so w is an honest weight vector. No diagonalizability of K is assumed; these are the weight-space inputs to complete reducibility.

Main results #

The calculation follows A. Virelizier, Quantum groups, Section 2.4.

source
theorem TauCeti.UqSl2.exists_eq_sign_mul_pow_of_highest_weight_vector {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [FiniteDimensional ℂ V] (hq : IsGenericQuantumParameter q) {μ : ℂ} {v : V} (hv : v ∈ weightSpace q V μ) (hv0 : v ≠ 0) (hev : e q • v = 0) :
∃ (m : ℕ) (ε : ℤˣ), μ = ↑↑ε * q ^ m ∧ f q ^ (m + 1) • v = 0 ∧ f q ^ m • v ≠ 0

A finite nonzero lowering string from a highest-weight vector has signed integral highest weight. The returned m is the last nonvanishing index of the string.

The top generalized weight space #

source
theorem TauCeti.UqSl2.eq_zero_of_f_pow_smul_eq_zero {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {m : ℕ} {ε : ℤˣ} (hq : IsGenericQuantumParameter q) {r : ℕ} (hr : r ≤ m) {w : V} (hw : w ∈ genWeightSpace q V (↑↑ε * q ^ m)) (he : e q • w = 0) (hf : f q ^ r • w = 0) :
w = 0

A generalized weight vector of weight ε q^m killed by E and by F^r for some r ≤ m is zero: F^r is injective on such vectors.

source
theorem TauCeti.UqSl2.f_pow_smul_eq_zero_of_e_smul_eq_zero {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {m : ℕ} {ε : ℤˣ} (hq : IsGenericQuantumParameter q) [FiniteDimensional ℂ V] {w : V} (hw : w ∈ genWeightSpace q V (↑↑ε * q ^ m)) (he : e q • w = 0) :
f q ^ (m + 1) • w = 0

At a generic parameter, in a finite-dimensional module, a generalized weight vector of weight ε q^m killed by E is killed by F^(m+1).

source
theorem TauCeti.UqSl2.f_pow_succ_smul_eq_zero_of_highest_weight_vector {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {m : ℕ} {ε : ℤˣ} (hq : IsGenericQuantumParameter q) [FiniteDimensional ℂ V] {v : V} (hv : v ∈ weightSpace q V (↑↑ε * q ^ m)) (hev : e q • v = 0) :
f q ^ (m + 1) • v = 0

In a finite-dimensional module at a generic parameter, the lowering string of a highest-weight vector of weight ε q^m vanishes after m + 1 steps.

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

At a generic parameter, in a finite-dimensional module, a generalized weight vector of weight ε q^m killed by E is an honest weight vector: K acts on it by the scalar ε q^m.