Weights and highest vectors for U_q(sl₂)

The weight spaces of a native UqSl2 q-module are the eigenspaces of the action of K, and its generalized weight spaces are the maximal generalized eigenspaces of K. The generators E and F shift both kinds of weight by q² and q⁻², respectively. A finite-dimensional module is the direct sum of its generalized weight spaces, whether or not K is diagonalizable. At a generic parameter, raising or lowering any vector of a finite-dimensional module therefore eventually kills it: otherwise the finite spectrum of K would contain an infinite geometric progression. Consequently every nonzero finite-dimensional module has a highest-weight vector. More precisely, every nonzero generalized weight vector is moved by some element of UqSl2 q to a nonzero highest-weight vector, and by another to a nonzero lowest-weight vector. This is the starting point for classifying finite-dimensional simple modules, and the generalized weight decomposition is the setting of the finite-dimensional complete-reducibility argument. Taking generalized weight spaces of finite-dimensional modules is exact: a surjective module map carries generalized weight spaces onto those of its target.

The action conventions are those of A. Virelizier, Quantum groups, Sections 2.3--2.4.

def TauCeti.UqSl2.weightSpace (q : ℂ) (V : Type u_2) [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (μ : ℂ) : Submodule ℂ V

The μ-weight space of a module is the native eigenspace of the action of K.

theorem TauCeti.UqSl2.weightSpace_def {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (μ : ℂ) : weightSpace q V μ = ((Algebra.lsmul ℂ ℂ V) (k q)).eigenspace μ

The weight space agrees with the native eigenspace of the action of K.

@[simp]

theorem TauCeti.UqSl2.mem_weightSpace_iff {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {μ : ℂ} {v : V} : v ∈ weightSpace q V μ ↔ k q • v = μ • v

Membership in a weight space means that K acts by its weight.

@[simp]

theorem TauCeti.UqSl2.weightSpace_zero {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] : weightSpace q V 0 = ⊥

The zero-weight space vanishes because K is invertible.

theorem TauCeti.UqSl2.weight_ne_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 μ) (hv0 : v ≠ 0) : μ ≠ 0

Every nonzero weight vector has nonzero weight.

theorem TauCeti.UqSl2.kInv_smul_of_mem_weightSpace {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {μ : ℂ} {v : V} (hv : v ∈ weightSpace q V μ) : kInv q • v = μ⁻¹ • v

On a vector of weight μ, the generator K⁻¹ acts by μ⁻¹.

theorem TauCeti.UqSl2.e_smul_mem_weightSpace {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {μ : ℂ} {v : V} (hv : v ∈ weightSpace q V μ) : e q • v ∈ weightSpace q V (q ^ 2 * μ)

Raising a weight vector multiplies its weight by q².

theorem TauCeti.UqSl2.f_smul_mem_weightSpace {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {μ : ℂ} {v : V} (hv : v ∈ weightSpace q V μ) : f q • v ∈ weightSpace q V (q⁻¹ ^ 2 * μ)

Lowering a weight vector multiplies its weight by q⁻².

theorem TauCeti.UqSl2.e_pow_smul_mem_weightSpace {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {μ : ℂ} {v : V} (hv : v ∈ weightSpace q V μ) (n : ℕ) : e q ^ n • v ∈ weightSpace q V ((q ^ 2) ^ n * μ)

The weight after n raising operations.

theorem TauCeti.UqSl2.f_pow_smul_mem_weightSpace {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {μ : ℂ} {v : V} (hv : v ∈ weightSpace q V μ) (n : ℕ) : f q ^ n • v ∈ weightSpace q V ((q⁻¹ ^ 2) ^ n * μ)

The weight after n lowering operations.

theorem TauCeti.UqSl2.kUnit_zpow_smul_of_mem_weightSpace {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {μ : ℂ} {v : V} (hv : v ∈ weightSpace q V μ) (b : ℤ) : ↑(kUnit q ^ b) • v = μ ^ b • v

On a vector of weight μ, the integer power K ^ b acts by μ ^ b.

theorem TauCeti.UqSl2.map_weightSpace_le {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {W : Type u_2} [AddCommGroup W] [Module ℂ W] [Module (UqSl2 q) W] [IsScalarTower ℂ (UqSl2 q) W] (φ : V →ₗ[UqSl2 q] W) (μ : ℂ) : Submodule.map (↑ℂ φ) (weightSpace q V μ) ≤ weightSpace q W μ

A module map carries each weight space into the weight space of the same weight.

theorem TauCeti.UqSl2.finite_setOf_weightSpace_ne_bot (q : ℂ) (V : Type u_1) [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [FiniteDimensional ℂ V] : {μ : ℂ | weightSpace q V μ ≠ ⊥}.Finite

A finite-dimensional module has only finitely many weights.

Generalized weight spaces

def TauCeti.UqSl2.genWeightSpace (q : ℂ) (V : Type u_2) [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (μ : ℂ) : Submodule ℂ V

The generalized μ-weight space of a module is the native maximal generalized eigenspace of the action of K: the vectors killed by some power of K - μ.

theorem TauCeti.UqSl2.genWeightSpace_def {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (μ : ℂ) : genWeightSpace q V μ = ((Algebra.lsmul ℂ ℂ V) (k q)).maxGenEigenspace μ

The generalized weight space agrees with the native maximal generalized eigenspace of the action of K.

@[simp]

theorem TauCeti.UqSl2.mem_genWeightSpace_iff {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {μ : ℂ} {v : V} : v ∈ genWeightSpace q V μ ↔ ∃ (n : ℕ), (k q - (algebraMap ℂ (UqSl2 q)) μ) ^ n • v = 0

Membership in a generalized weight space means that some power of K - μ kills the vector.

theorem TauCeti.UqSl2.weightSpace_le_genWeightSpace {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (μ : ℂ) : weightSpace q V μ ≤ genWeightSpace q V μ

Every weight space lies in the generalized weight space of the same weight.

@[simp]

theorem TauCeti.UqSl2.genWeightSpace_zero {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] : genWeightSpace q V 0 = ⊥

The generalized zero-weight space vanishes because K is invertible.

theorem TauCeti.UqSl2.smul_mem_genWeightSpace_of_k_mul {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {a : UqSl2 q} {c μ : ℂ} (ha : k q * a = c • (a * k q)) {v : V} (hv : v ∈ genWeightSpace q V μ) : a • v ∈ genWeightSpace q V (c * μ)

An element a that q-commutes with K in the form K a = c (a K) maps the generalized μ-weight space into the generalized c μ-weight space.

theorem TauCeti.UqSl2.e_smul_mem_genWeightSpace {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {μ : ℂ} {v : V} (hv : v ∈ genWeightSpace q V μ) : e q • v ∈ genWeightSpace q V (q ^ 2 * μ)

Raising a generalized weight vector multiplies its generalized weight by q².

theorem TauCeti.UqSl2.f_smul_mem_genWeightSpace {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {μ : ℂ} {v : V} (hv : v ∈ genWeightSpace q V μ) : f q • v ∈ genWeightSpace q V (q⁻¹ ^ 2 * μ)

Lowering a generalized weight vector multiplies its generalized weight by q⁻².

theorem TauCeti.UqSl2.e_pow_smul_mem_genWeightSpace {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {μ : ℂ} {v : V} (hv : v ∈ genWeightSpace q V μ) (n : ℕ) : e q ^ n • v ∈ genWeightSpace q V ((q ^ 2) ^ n * μ)

The generalized weight after n raising operations.

theorem TauCeti.UqSl2.f_pow_smul_mem_genWeightSpace {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {μ : ℂ} {v : V} (hv : v ∈ genWeightSpace q V μ) (n : ℕ) : f q ^ n • v ∈ genWeightSpace q V ((q⁻¹ ^ 2) ^ n * μ)

The generalized weight after n lowering operations.

theorem TauCeti.UqSl2.iSupIndep_genWeightSpace {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] : iSupIndep (genWeightSpace q V)

Generalized weight spaces for distinct weights are independent.

theorem TauCeti.UqSl2.k_smul_mem_genWeightSpace {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {μ : ℂ} {v : V} (hv : v ∈ genWeightSpace q V μ) : k q • v ∈ genWeightSpace q V μ

K preserves every generalized weight space.

theorem TauCeti.UqSl2.kInv_smul_mem_genWeightSpace {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {μ : ℂ} {v : V} (hv : v ∈ genWeightSpace q V μ) : kInv q • v ∈ genWeightSpace q V μ

K⁻¹ preserves every generalized weight space.

theorem TauCeti.UqSl2.eq_zero_of_mem_weightSpace_of_mem_genWeightSpace {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {α ν : ℂ} (h : α ≠ ν) {v : V} (hα : v ∈ weightSpace q V α) (hν : v ∈ genWeightSpace q V ν) : v = 0

A vector of weight α in the generalized weight space of a different weight vanishes.

theorem TauCeti.UqSl2.k_smul_eq_of_k_sq_smul_eq {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {ν ρ : ℂ} (h : -ρ ≠ ν) {v : V} (hv : v ∈ genWeightSpace q V ν) (hk : k q ^ 2 • v = ρ ^ 2 • v) : k q • v = ρ • v

If K² v = ρ² v for a generalized weight vector v of weight ν ≠ -ρ, then K v = ρ v.

theorem TauCeti.UqSl2.exists_pow_smul_mem_weightSpace {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {μ : ℂ} {w : V} (hw : w ∈ genWeightSpace q V μ) (hw0 : w ≠ 0) : ∃ (r : ℕ), (k q - (algebraMap ℂ (UqSl2 q)) μ) ^ r • w ≠ 0 ∧ (k q - (algebraMap ℂ (UqSl2 q)) μ) ^ r • w ∈ weightSpace q V μ

Some power of K - μ sends a nonzero generalized weight vector of weight μ to a nonzero weight vector of weight μ.

theorem TauCeti.UqSl2.iSup_genWeightSpace_eq_top {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [FiniteDimensional ℂ V] : ⨆ (μ : ℂ), genWeightSpace q V μ = ⊤

A finite-dimensional module is the sum of its generalized weight spaces.

theorem TauCeti.UqSl2.map_genWeightSpace_eq_of_surjective {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [FiniteDimensional ℂ V] {V' : Type u_2} [AddCommGroup V'] [Module ℂ V'] [Module (UqSl2 q) V'] [IsScalarTower ℂ (UqSl2 q) V'] {φ : V →ₗ[UqSl2 q] V'} (hφ : Function.Surjective ⇑φ) (μ : ℂ) : Submodule.map (↑ℂ φ) (genWeightSpace q V μ) = genWeightSpace q V' μ

A surjective module map carries the generalized weight spaces of a finite-dimensional module onto the generalized weight spaces of its target. In particular, taking generalized weight spaces is exact on quotient modules.

theorem TauCeti.UqSl2.exists_eq_zero_of_forall_mem_genWeightSpace {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [FiniteDimensional ℂ V] {p : ℂ} (hp : IsGenericQuantumParameter p) {μ : ℂ} {w : ℕ → V} (hw : ∀ (n : ℕ), w n ∈ genWeightSpace q V ((p ^ 2) ^ n * μ)) : ∃ (n : ℕ), w n = 0

At a generic parameter p, a sequence of vectors whose n-th term has generalized weight (p²)ⁿ μ eventually vanishes: otherwise the finite spectrum of K would contain an infinite geometric progression.

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

At a generic parameter, the raising string through any vector of a finite-dimensional module terminates: E acts locally nilpotently.

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

At a generic parameter, the lowering string through any vector of a finite-dimensional module terminates: F acts locally nilpotently.

theorem TauCeti.UqSl2.exists_e_pow_smul_ne_zero_and_e_smul_eq_zero {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [FiniteDimensional ℂ V] (hq : IsGenericQuantumParameter q) {v : V} (hv0 : v ≠ 0) : ∃ (n : ℕ), e q ^ n • v ≠ 0 ∧ e q • e q ^ n • v = 0

At a generic parameter, the raising string through a nonzero vector of a finite-dimensional module ends in a nonzero vector Eⁿ v killed by E. When v has weight μ, this is a highest-weight vector of weight (q²)ⁿ μ.

theorem TauCeti.UqSl2.exists_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) [Nontrivial V] : ∃ (μ : ℂ) (v : V), μ ≠ 0 ∧ v ≠ 0 ∧ k q • v = μ • v ∧ e q • v = 0

Every nonzero finite-dimensional module at a generic parameter has a highest-weight vector. No diagonalizability of K is assumed.

theorem TauCeti.UqSl2.exists_highest_weight_vector_of_genWeightSpace_ne_bot {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [FiniteDimensional ℂ V] (hq : IsGenericQuantumParameter q) {ν : ℂ} (hν : genWeightSpace q V ν ≠ ⊥) : ∃ (n : ℕ), ∃ v ∈ weightSpace q V ((q ^ 2) ^ n * ν), v ≠ 0 ∧ e q • v = 0

At a generic parameter, every nonzero generalized weight space of weight ν yields a nonzero vector of weight (q²)ⁿ ν, for some n, killed by E.

theorem TauCeti.UqSl2.exists_smul_highest_weight_vector_of_mem_genWeightSpace {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [FiniteDimensional ℂ V] (hq : IsGenericQuantumParameter q) {μ : ℂ} {w : V} (hw : w ∈ genWeightSpace q V μ) (hw0 : w ≠ 0) : ∃ (a : UqSl2 q) (n : ℕ), a • w ≠ 0 ∧ a • w ∈ weightSpace q V ((q ^ 2) ^ n * μ) ∧ e q • a • w = 0

At a generic parameter, every nonzero generalized weight vector w of weight μ in a finite-dimensional module can be moved by an element of UqSl2 q to a nonzero highest-weight vector, of weight q^(2n) μ for some n.

theorem TauCeti.UqSl2.exists_smul_lowest_weight_vector_of_mem_genWeightSpace {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [FiniteDimensional ℂ V] (hq : IsGenericQuantumParameter q) {μ : ℂ} {w : V} (hw : w ∈ genWeightSpace q V μ) (hw0 : w ≠ 0) : ∃ (a : UqSl2 q) (n : ℕ), a • w ≠ 0 ∧ a • w ∈ weightSpace q V ((q⁻¹ ^ 2) ^ n * μ) ∧ f q • a • w = 0

At a generic parameter, every nonzero generalized weight vector w of weight μ in a finite-dimensional module can be moved by an element of UqSl2 q to a nonzero lowest-weight vector, of weight q^(-2n) μ for some n.