Type-1 U_q(sl₂)-modules

A UqSl2 q-module is a weight module with weights in S when K acts diagonalizably with all eigenvalues in S, i.e. the module is the sum, hence the algebraic direct sum, of its weight spaces of weight in S. No finiteness of the module is assumed. It is of type 1 when the weights are integral powers q ^ n, n : ℤ, and of signed type 1 when they are signed powers ± q ^ n.

At a generic parameter q (nonzero and not a root of unity) the following are equivalent for a module V:

• V is of type 1 and E, F act locally nilpotently;
• V is of type 1 and locally finite;
• V is a direct sum of positive signed ladder modules L_m^+.

Dropping the sign condition, a module is of signed type 1 with E, F locally nilpotent exactly when it is locally finite. The one-dimensional module L_0^-, on which K acts by -1 and E, F act by zero, is locally finite but not of type 1, so the unsigned integral-weight condition is genuinely stronger than local finiteness.

The implication from local nilpotence to local finiteness holds for any weight module: by the PBW basis, the cyclic submodule generated by v is spanned by the vectors F^a K^b E^c v. Only finitely many E^c v are nonzero, only finitely many F^a E^c v are nonzero, and the K-orbit of a vector of a weight module spans a finite-dimensional space.

Main definitions

• TauCeti.UqSl2.IsWeightModule q V S: V is spanned by its weight spaces of weight in S.
• TauCeti.UqSl2.IsTypeOne q V: V is a weight module with weights q ^ n, n : ℤ.
• TauCeti.UqSl2.IsSignedTypeOne q V: V is a weight module with weights ± q ^ n.

Main results

• TauCeti.UqSl2.isWeightModule_iff_isInternal: a weight module is the internal direct sum of its weight spaces.
• TauCeti.UqSl2.IsWeightModule.exists_basis_mem_weightSpace: a finite-dimensional weight module has a basis of weight vectors.
• TauCeti.UqSl2.isTypeOne_iff_isInternal: at a generic parameter, V is of type 1 exactly when it is the internal direct sum of the weight spaces of weight q ^ n, n : ℤ.
• TauCeti.UqSl2.isLocallyFiniteModule_of_isWeightModule: a weight module on which E and F act locally nilpotently is locally finite.
• isTypeOne_and_isLocallyFiniteModule_iff_exists_linearEquiv_dfinsupp_ladderModule and isTypeOne_and_forall_exists_pow_smul_eq_zero_iff_exists_linearEquiv_dfinsupp_ladderModule (in TauCeti.UqSl2): the classification of type-1 modules with locally nilpotent E, F as direct sums of L_m^+.
• TauCeti.UqSl2.isSignedTypeOne_and_forall_exists_pow_smul_eq_zero_iff_isLocallyFiniteModule: the signed version characterizes local finiteness.
• TauCeti.UqSl2.LadderModule.not_isTypeOne: L_m^- is not of type 1.

References

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

Weight modules

def TauCeti.UqSl2.IsWeightModule (q : ℂ) (V : Type u_1) [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (S : Set ℂ) : Prop

A UqSl2 q-module is a weight module with weights in S when it is spanned by its weight spaces of weight in S: K acts diagonalizably and all its eigenvalues lie in S.

theorem TauCeti.UqSl2.isWeightModule_iff {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {S : Set ℂ} : IsWeightModule q V S ↔ ⨆ μ ∈ S, weightSpace q V μ = ⊤

A module is a weight module with weights in S exactly when its weight spaces of weight in S span it.

theorem TauCeti.UqSl2.IsWeightModule.iSup_eq_top {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {S : Set ℂ} (h : IsWeightModule q V S) : ⨆ μ ∈ S, weightSpace q V μ = ⊤

The weight spaces of weight in S of a weight module with weights in S span it.

theorem TauCeti.UqSl2.IsWeightModule.mono {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {S T : Set ℂ} (h : IsWeightModule q V S) (hST : S ⊆ T) : IsWeightModule q V T

A weight module with weights in S has weights in every larger set.

theorem TauCeti.UqSl2.IsWeightModule.mem_of_mem_weightSpace {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {S : Set ℂ} (h : IsWeightModule q V S) {μ : ℂ} {v : V} (hv : v ∈ weightSpace q V μ) (hv0 : v ≠ 0) : μ ∈ S

Every eigenvalue of K on a weight module with weights in S lies in S.

theorem TauCeti.UqSl2.isWeightModule_iff_isInternal {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {S : Set ℂ} : IsWeightModule q V S ↔ DirectSum.IsInternal fun (μ : ↑S) => weightSpace q V ↑μ

A module is a weight module with weights in S exactly when it is the internal direct sum of its weight spaces of weight in S.

theorem TauCeti.UqSl2.IsWeightModule.exists_basis_mem_weightSpace {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {S : Set ℂ} [FiniteDimensional ℂ V] (h : IsWeightModule q V S) : ∃ (b : Module.Basis (Fin (Module.finrank ℂ V)) ℂ V) (wt : Fin (Module.finrank ℂ V) → ℂ), ∀ (i : Fin (Module.finrank ℂ V)), b i ∈ weightSpace q V (wt i)

A finite-dimensional weight module has a basis of weight vectors.

theorem TauCeti.UqSl2.IsWeightModule.of_iSup_range_eq_top {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {S : Set ℂ} {ι : Type u_2} {N : ι → Type u_3} [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module ℂ (N i)] [(i : ι) → Module (UqSl2 q) (N i)] [∀ (i : ι), IsScalarTower ℂ (UqSl2 q) (N i)] (φ : (i : ι) → N i →ₗ[UqSl2 q] V) (hφ : ⨆ (i : ι), (φ i).range = ⊤) (h : ∀ (i : ι), IsWeightModule q (N i) S) : IsWeightModule q V S

A module is a weight module with weights in S when it is spanned by the images of module maps from weight modules with weights in S.

theorem TauCeti.UqSl2.IsWeightModule.of_surjective {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {S : Set ℂ} {W : Type u_2} [AddCommGroup W] [Module ℂ W] [Module (UqSl2 q) W] [IsScalarTower ℂ (UqSl2 q) W] (h : IsWeightModule q W S) (φ : W →ₗ[UqSl2 q] V) (hφ : Function.Surjective ⇑φ) : IsWeightModule q V S

The image of a weight module under a surjective module map is a weight module with the same weights.

theorem TauCeti.UqSl2.IsWeightModule.dfinsupp {q : ℂ} {S : Set ℂ} {ι : Type u_2} {N : ι → Type u_3} [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module ℂ (N i)] [(i : ι) → Module (UqSl2 q) (N i)] [∀ (i : ι), IsScalarTower ℂ (UqSl2 q) (N i)] (h : ∀ (i : ι), IsWeightModule q (N i) S) : IsWeightModule q (Π₀ (i : ι), N i) S

A direct sum of weight modules with weights in S is a weight module with weights in S.

Type-1 and signed type-1 modules

@[reducible, inline]

abbrev TauCeti.UqSl2.IsTypeOne (q : ℂ) (V : Type u_1) [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] : Prop

A UqSl2 q-module is of type 1 when K acts diagonalizably with all eigenvalues integral powers q ^ n of q.

@[reducible, inline]

abbrev TauCeti.UqSl2.IsSignedTypeOne (q : ℂ) (V : Type u_1) [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] : Prop

A UqSl2 q-module is of signed type 1 when K acts diagonalizably with all eigenvalues signed integral powers ± q ^ n of q.

theorem TauCeti.UqSl2.isTypeOne_iff {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] : IsTypeOne q V ↔ ⨆ (n : ℤ), weightSpace q V (q ^ n) = ⊤

A module is of type 1 exactly when its weight spaces of weight q ^ n, n : ℤ, span it.

theorem TauCeti.UqSl2.isSignedTypeOne_iff {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] : IsSignedTypeOne q V ↔ ⨆ (ε : ℤˣ), ⨆ (n : ℤ), weightSpace q V (↑↑ε * q ^ n) = ⊤

A module is of signed type 1 exactly when its weight spaces of weight ε q ^ n, for signs ε and n : ℤ, span it.

theorem TauCeti.UqSl2.isTypeOne_iff_isInternal {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (hq : IsGenericQuantumParameter q) : IsTypeOne q V ↔ DirectSum.IsInternal fun (n : ℤ) => weightSpace q V (q ^ n)

At a generic parameter, a module is of type 1 exactly when it is the internal direct sum of its weight spaces of weight q ^ n, n : ℤ.

theorem TauCeti.UqSl2.IsTypeOne.isSignedTypeOne {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (h : IsTypeOne q V) : IsSignedTypeOne q V

A module of type 1 is of signed type 1.

Signed ladder modules

theorem TauCeti.UqSl2.LadderModule.isWeightModule {q : ℂ} {S : Set ℂ} [Fact (q ≠ 0)] {m : ℕ} {ε : ℤˣ} (hS : ∀ (j : Fin (m + 1)), ↑↑ε * q ^ (↑m - 2 * ↑↑j) ∈ S) : IsWeightModule q (LadderModule q m ε) S

The signed ladder module L_m^ε is a weight module with weights in any set containing its weights ε q ^ (m - 2j), 0 ≤ j ≤ m.

theorem TauCeti.UqSl2.LadderModule.isTypeOne {q : ℂ} [Fact (q ≠ 0)] {m : ℕ} : IsTypeOne q (LadderModule q m 1)

The positive signed ladder module L_m^+ is of type 1.

theorem TauCeti.UqSl2.LadderModule.isSignedTypeOne {q : ℂ} [Fact (q ≠ 0)] {m : ℕ} {ε : ℤˣ} : IsSignedTypeOne q (LadderModule q m ε)

Every signed ladder module L_m^ε is of signed type 1.

theorem TauCeti.UqSl2.IsTypeOne.eq_one_of_injective {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [Fact (q ≠ 0)] (hq : IsGenericQuantumParameter q) (h : IsTypeOne q V) {m : ℕ} {ε : ℤˣ} (φ : LadderModule q m ε →ₗ[UqSl2 q] V) (hφ : Function.Injective ⇑φ) : ε = 1

At a generic parameter, a signed ladder module L_m^ε embeds into a module of type 1 only for the positive sign ε = 1.

theorem TauCeti.UqSl2.LadderModule.not_isTypeOne {q : ℂ} [Fact (q ≠ 0)] (hq : IsGenericQuantumParameter q) {m : ℕ} : ¬IsTypeOne q (LadderModule q m (-1))

At a generic parameter, the negative signed ladder module L_m^- is not of type 1. For m = 0 this is the one-dimensional module on which K acts by -1 and E, F act by zero; being finite-dimensional, it is locally finite.

Local finiteness of weight modules

theorem TauCeti.UqSl2.isLocallyFiniteModule_of_isWeightModule {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {S : Set ℂ} [Fact (q ≠ 0)] (h : IsWeightModule q V S) (hE : ∀ (v : V), ∃ (n : ℕ), e q ^ n • v = 0) (hF : ∀ (v : V), ∃ (n : ℕ), f q ^ n • v = 0) : IsLocallyFiniteModule ℂ (UqSl2 q) V

A weight module on which E and F act locally nilpotently is locally finite.

Classification

theorem TauCeti.UqSl2.isTypeOne_of_linearEquiv_dfinsupp_ladderModule {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [Fact (q ≠ 0)] {ι : Type u_2} {m : ι → ℕ} (e : V ≃ₗ[UqSl2 q] Π₀ (i : ι), LadderModule q (m i) 1) : IsTypeOne q V

A direct sum of positive signed ladder modules L_m^+ is of type 1.

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

At a generic parameter, a locally finite module of type 1 is isomorphic to a direct sum of positive signed ladder modules L_m^+.

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

Type-1 locally finite modules. At a generic parameter, a module is of type 1 and locally finite exactly when it is isomorphic to a direct sum of positive signed ladder modules L_m^+.

theorem TauCeti.UqSl2.isTypeOne_and_forall_exists_pow_smul_eq_zero_iff_exists_linearEquiv_dfinsupp_ladderModule {q : ℂ} [Fact (q ≠ 0)] {V : Type u} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (hq : IsGenericQuantumParameter q) : (IsTypeOne q V ∧ (∀ (v : V), ∃ (n : ℕ), e q ^ n • v = 0) ∧ ∀ (v : V), ∃ (n : ℕ), f q ^ n • v = 0) ↔ ∃ (ι : Type u) (m : ι → ℕ), Nonempty (V ≃ₗ[UqSl2 q] Π₀ (i : ι), LadderModule q (m i) 1)

Type-1 modules with locally nilpotent E and F. At a generic parameter, a module is of type 1 with E and F acting locally nilpotently exactly when it is isomorphic to a direct sum of positive signed ladder modules L_m^+.

theorem TauCeti.UqSl2.isSignedTypeOne_and_forall_exists_pow_smul_eq_zero_iff_isLocallyFiniteModule {q : ℂ} [Fact (q ≠ 0)] {V : Type u} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (hq : IsGenericQuantumParameter q) : (IsSignedTypeOne q V ∧ (∀ (v : V), ∃ (n : ℕ), e q ^ n • v = 0) ∧ ∀ (v : V), ∃ (n : ℕ), f q ^ n • v = 0) ↔ IsLocallyFiniteModule ℂ (UqSl2 q) V

Signed type-1 modules. At a generic parameter, a module is of signed type 1 with E and F acting locally nilpotently exactly when it is locally finite.