The signed ladder modules of U_q(sl₂)

For a nonzero complex parameter q, a natural number m and a sign ε : ℤˣ, this file constructs the (m + 1)-dimensional UqSl2 q-module L_m^ε with basis v₀, …, v_m and action

• K v_j = ε q^(m - 2j) v_j and K⁻¹ v_j = ε q^(2j - m) v_j,
• F v_j = [j + 1]_q v_(j + 1), and
• E v_j = ε [m - j + 1]_q v_(j - 1),

where [r]_q is the symmetric quantum integer and the out-of-range vectors v_(-1) and v_(m + 1) are zero. The basis vectors are indexed by all integers, with v_j = 0 outside 0 ≤ j ≤ m; with this convention the action formulas hold for every integer j.

These are the signed simple modules of U_q(sl₂). For a generic parameter (nonzero and not a root of unity), L_m^ε is a simple module whose endomorphisms are the complex scalars (Schur's lemma), and L_m^ε and L_n^δ are isomorphic only when m = n and ε = δ.

A vector v of weight ε q^m in any UqSl2 q-module, killed by E and by F^(m+1), determines a unique module map from L_m^ε that sends v₀ to v, and more generally sends v_j to the normalized lowering string F^j v / ([1]_q ⋯ [j]_q).

Main definitions

• TauCeti.UqSl2.LadderModule q m ε: the module L_m^ε.
• TauCeti.UqSl2.LadderModule.basis: its basis v₀, …, v_m.
• TauCeti.UqSl2.LadderModule.vec: the integer-indexed vectors v_j.
• TauCeti.UqSl2.LadderModule.rep: the action as an algebra map to complex endomorphisms.
• TauCeti.UqSl2.LadderModule.homOfVec: a complex-linear map out of L_m^ε commuting with E, F, K on the ladder vectors, as a module map.
• TauCeti.UqSl2.LadderModule.lift: the module map determined by a highest vector of weight ε q^m whose lowering string has length at most m + 1.

Main results

• TauCeti.UqSl2.LadderModule.basis_repr_vec: the coordinates of v_j in the ladder basis.
• TauCeti.UqSl2.LadderModule.e_smul_vec, f_smul_vec, k_smul_vec, kInv_smul_vec: the action of the generators.
• TauCeti.UqSl2.LadderModule.e_pow_smul_vec, f_pow_smul_vec: the action of their powers.
• TauCeti.UqSl2.LadderModule.map_smul_of_vec: commutation of a complex-linear map out of L_m^ε with an element of UqSl2 q can be checked on the ladder vectors.
• TauCeti.UqSl2.LadderModule.isSimpleModule: L_m^ε is simple at a generic parameter.
• TauCeti.UqSl2.LadderModule.hom_ext: at a generic parameter, module maps out of L_m^ε are determined by their value at v₀.
• TauCeti.UqSl2.LadderModule.lift_vec_zero: lift sends v₀ to the given vector.
• TauCeti.UqSl2.LadderModule.lift_injective: the map induced by a nonzero vector is injective.
• TauCeti.UqSl2.LadderModule.algebraMap_end_bijective: Schur's lemma for L_m^ε.
• TauCeti.UqSl2.LadderModule.trace_rep_kInv, trace_rep_k: the traces of K⁻¹ and of K on L_m^ε are both ε [m + 1]_q.
• TauCeti.UqSl2.LadderModule.nonempty_linearEquiv_iff: L_m^ε ≅ L_n^δ iff m = n and ε = δ, at a generic parameter.

References

• A. Virelizier, Quantum groups, Section 2.4, for these modules in the rank-one convention.
• C. Kassel, Quantum Groups, Graduate Texts in Mathematics 155, Section VI.3, where the same modules appear as V_(ε,n).

def TauCeti.UqSl2.LadderModule (_q : ℂ) (m : ℕ) (_ε : ℤˣ) : Type

The underlying complex vector space ℂ^(m + 1) of the signed ladder module L_m^ε of UqSl2 q. Its UqSl2 q-module structure, defined for nonzero q, is LadderModule.instModule.

@[instance_reducible]

noncomputable instance TauCeti.UqSl2.LadderModule.instAddCommGroup (q : ℂ) (m : ℕ) (ε : ℤˣ) : AddCommGroup (LadderModule q m ε)

@[instance_reducible]

noncomputable instance TauCeti.UqSl2.LadderModule.instModuleComplex (q : ℂ) (m : ℕ) (ε : ℤˣ) : Module ℂ (LadderModule q m ε)

instance TauCeti.UqSl2.LadderModule.instFiniteDimensionalComplex (q : ℂ) (m : ℕ) (ε : ℤˣ) : FiniteDimensional ℂ (LadderModule q m ε)

noncomputable def TauCeti.UqSl2.LadderModule.basis (q : ℂ) (m : ℕ) (ε : ℤˣ) : Module.Basis (Fin (m + 1)) ℂ (LadderModule q m ε)

The ladder basis v₀, …, v_m of L_m^ε.

noncomputable def TauCeti.UqSl2.LadderModule.vec (q : ℂ) (m : ℕ) (ε : ℤˣ) (j : ℤ) : LadderModule q m ε

The ladder vector v_j of L_m^ε for an integer j: the basis vector for 0 ≤ j ≤ m and zero otherwise.

theorem TauCeti.UqSl2.LadderModule.vec_coe {q : ℂ} {m : ℕ} {ε : ℤˣ} (i : Fin (m + 1)) : vec q m ε ↑↑i = (basis q m ε) i

The ladder vector with index in range is the corresponding basis vector.

@[simp]

theorem TauCeti.UqSl2.LadderModule.vec_eq_zero_iff {q : ℂ} {m : ℕ} {ε : ℤˣ} {j : ℤ} : vec q m ε j = 0 ↔ j < 0 ∨ ↑m < j

The ladder vectors vanish exactly outside the range 0 ≤ j ≤ m.

@[simp]

theorem TauCeti.UqSl2.LadderModule.vec_eq_zero_of_neg {q : ℂ} {m : ℕ} {ε : ℤˣ} {j : ℤ} (hj : j < 0) : vec q m ε j = 0

The ladder vectors with negative index vanish.

@[simp]

theorem TauCeti.UqSl2.LadderModule.vec_eq_zero_of_lt {q : ℂ} {m : ℕ} {ε : ℤˣ} {j : ℤ} (hj : ↑m < j) : vec q m ε j = 0

The ladder vectors with index above m vanish.

@[simp]

theorem TauCeti.UqSl2.LadderModule.basis_repr_vec {q : ℂ} {m : ℕ} {ε : ℤˣ} (j : ℤ) (i : Fin (m + 1)) : ((basis q m ε).repr (vec q m ε j)) i = if ↑↑i = j then 1 else 0

The coordinates of a ladder vector in the ladder basis: v_j has coordinate 1 at j and 0 elsewhere, and all its coordinates vanish when j is out of range.

@[simp]

theorem TauCeti.UqSl2.LadderModule.finrank_eq {q : ℂ} {m : ℕ} {ε : ℤˣ} : Module.finrank ℂ (LadderModule q m ε) = m + 1

The complex dimension of L_m^ε is m + 1.

The generator operators

The module structure

noncomputable def TauCeti.UqSl2.LadderModule.rep (q : ℂ) (m : ℕ) (ε : ℤˣ) [Fact (q ≠ 0)] : UqSl2 q →ₐ[ℂ] Module.End ℂ (LadderModule q m ε)

The action of UqSl2 q on L_m^ε, as an algebra map to complex endomorphisms.

@[instance_reducible]

noncomputable instance TauCeti.UqSl2.LadderModule.instModule {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] : Module (UqSl2 q) (LadderModule q m ε)

The UqSl2 q-module structure of L_m^ε, given by LadderModule.rep.

theorem TauCeti.UqSl2.LadderModule.smul_def {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] (a : UqSl2 q) (x : LadderModule q m ε) : a • x = ((rep q m ε) a) x

An element of UqSl2 q acts on L_m^ε through LadderModule.rep.

instance TauCeti.UqSl2.LadderModule.instIsScalarTowerComplex {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] : IsScalarTower ℂ (UqSl2 q) (LadderModule q m ε)

@[simp]

theorem TauCeti.UqSl2.LadderModule.e_smul_vec {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] (j : ℤ) : e q • vec q m ε j = (↑↑ε * quantumInteger q (↑m - j + 1)) • vec q m ε (j - 1)

The action of E on the ladder vectors: E v_j = ε [m - j + 1]_q v_(j - 1).

@[simp]

theorem TauCeti.UqSl2.LadderModule.f_smul_vec {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] (j : ℤ) : f q • vec q m ε j = quantumInteger q (j + 1) • vec q m ε (j + 1)

The action of F on the ladder vectors: F v_j = [j + 1]_q v_(j + 1).

@[simp]

theorem TauCeti.UqSl2.LadderModule.k_smul_vec {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] (j : ℤ) : k q • vec q m ε j = (↑↑ε * q ^ (↑m - 2 * j)) • vec q m ε j

The action of K on the ladder vectors: K v_j = ε q^(m - 2j) v_j.

@[simp]

theorem TauCeti.UqSl2.LadderModule.kInv_smul_vec {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] (j : ℤ) : kInv q • vec q m ε j = (↑↑ε * q ^ (2 * j - ↑m)) • vec q m ε j

The action of K⁻¹ on the ladder vectors: K⁻¹ v_j = ε q^(2j - m) v_j.

@[simp]

theorem TauCeti.UqSl2.LadderModule.e_smul_basis {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] (i : Fin (m + 1)) : e q • (basis q m ε) i = (↑↑ε * quantumInteger q (↑m - ↑↑i + 1)) • vec q m ε (↑↑i - 1)

The action of E on a basis vector, with the boundary encoded by vec.

@[simp]

theorem TauCeti.UqSl2.LadderModule.f_smul_basis {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] (i : Fin (m + 1)) : f q • (basis q m ε) i = quantumInteger q (↑↑i + 1) • vec q m ε (↑↑i + 1)

The action of F on a basis vector, with the boundary encoded by vec.

@[simp]

theorem TauCeti.UqSl2.LadderModule.k_smul_basis {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] (i : Fin (m + 1)) : k q • (basis q m ε) i = (↑↑ε * q ^ (↑m - 2 * ↑↑i)) • (basis q m ε) i

Each basis vector is a K eigenvector of weight ε q^(m - 2i).

@[simp]

theorem TauCeti.UqSl2.LadderModule.kInv_smul_basis {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] (i : Fin (m + 1)) : kInv q • (basis q m ε) i = (↑↑ε * q ^ (2 * ↑↑i - ↑m)) • (basis q m ε) i

Each basis vector is a K⁻¹ eigenvector of weight ε q^(2i - m).

theorem TauCeti.UqSl2.LadderModule.e_pow_smul_vec {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] (n : ℕ) (j : ℤ) : e q ^ n • vec q m ε j = (∏ i ∈ Finset.range n, ↑↑ε * quantumInteger q (↑m - j + ↑i + 1)) • vec q m ε (j - ↑n)

The action of the powers of E on the ladder vectors.

theorem TauCeti.UqSl2.LadderModule.f_pow_smul_vec {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] (n : ℕ) (j : ℤ) : f q ^ n • vec q m ε j = (∏ i ∈ Finset.range n, quantumInteger q (j + ↑i + 1)) • vec q m ε (j + ↑n)

The action of the powers of F on the ladder vectors.

Simplicity

theorem TauCeti.UqSl2.LadderModule.isSimpleModule {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] (hq : IsGenericQuantumParameter q) : IsSimpleModule (UqSl2 q) (LadderModule q m ε)

At a generic parameter, the signed ladder module L_m^ε is a simple UqSl2 q-module.

theorem TauCeti.UqSl2.LadderModule.hom_ext {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] (hq : IsGenericQuantumParameter q) {V : Type u_1} [AddCommMonoid V] [Module (UqSl2 q) V] {φ ψ : LadderModule q m ε →ₗ[UqSl2 q] V} (h : φ (vec q m ε 0) = ψ (vec q m ε 0)) : φ = ψ

At a generic parameter, a UqSl2 q-module map out of L_m^ε is determined by its value at the highest vector v₀.

Universal property

theorem TauCeti.UqSl2.LadderModule.map_smul_of_vec {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (φ : LadderModule q m ε →ₗ[ℂ] V) (a : UqSl2 q) (h : ∀ j ≤ m, φ (a • vec q m ε ↑j) = a • φ (vec q m ε ↑j)) (x : LadderModule q m ε) : φ (a • x) = a • φ x

Commutation of a complex-linear map out of L_m^ε with an element of UqSl2 q can be checked on the ladder vectors.

noncomputable def TauCeti.UqSl2.LadderModule.homOfVec {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (φ : LadderModule q m ε →ₗ[ℂ] V) (he : ∀ j ≤ m, φ (e q • vec q m ε ↑j) = e q • φ (vec q m ε ↑j)) (hf : ∀ j ≤ m, φ (f q • vec q m ε ↑j) = f q • φ (vec q m ε ↑j)) (hk : ∀ j ≤ m, φ (k q • vec q m ε ↑j) = k q • φ (vec q m ε ↑j)) : LadderModule q m ε →ₗ[UqSl2 q] V

A complex-linear map out of L_m^ε commuting with E, F and K on the ladder vectors v₀, …, v_m is UqSl2 q-linear.

@[simp]

theorem TauCeti.UqSl2.LadderModule.homOfVec_apply {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (φ : LadderModule q m ε →ₗ[ℂ] V) (he : ∀ j ≤ m, φ (e q • vec q m ε ↑j) = e q • φ (vec q m ε ↑j)) (hf : ∀ j ≤ m, φ (f q • vec q m ε ↑j) = f q • φ (vec q m ε ↑j)) (hk : ∀ j ≤ m, φ (k q • vec q m ε ↑j) = k q • φ (vec q m ε ↑j)) (x : LadderModule q m ε) : (homOfVec φ he hf hk) x = φ x

homOfVec φ agrees with φ.

noncomputable def TauCeti.UqSl2.LadderModule.lift {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (hq : IsGenericQuantumParameter q) {v : V} (hv : v ∈ weightSpace q V (↑↑ε * q ^ m)) (he : e q • v = 0) (hf : f q ^ (m + 1) • v = 0) : LadderModule q m ε →ₗ[UqSl2 q] V

The UqSl2 q-module map L_m^ε → V determined by a vector v of weight ε q^m killed by E and by F^(m+1). It sends v_j to F^j v / ([1]_q ⋯ [j]_q).

theorem TauCeti.UqSl2.LadderModule.lift_vec {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (hq : IsGenericQuantumParameter q) {v : V} (hv : v ∈ weightSpace q V (↑↑ε * q ^ m)) (he : e q • v = 0) (hf : f q ^ (m + 1) • v = 0) (j : ℕ) : (lift hq hv he hf) (vec q m ε ↑j) = (quantumFactorial q j)⁻¹ • f q ^ j • v

The map induced by v sends v_j to F^j v / ([1]_q ⋯ [j]_q).

@[simp]

theorem TauCeti.UqSl2.LadderModule.lift_vec_zero {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (hq : IsGenericQuantumParameter q) {v : V} (hv : v ∈ weightSpace q V (↑↑ε * q ^ m)) (he : e q • v = 0) (hf : f q ^ (m + 1) • v = 0) : (lift hq hv he hf) (vec q m ε 0) = v

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

theorem TauCeti.UqSl2.LadderModule.lift_injective {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (hq : IsGenericQuantumParameter q) {v : V} (hv : v ∈ weightSpace q V (↑↑ε * q ^ m)) (he : e q • v = 0) (hf : f q ^ (m + 1) • v = 0) (hv0 : v ≠ 0) : Function.Injective ⇑(lift hq hv he hf)

The map induced by a nonzero vector is injective.

Schur's lemma and pairwise non-isomorphism

theorem TauCeti.UqSl2.LadderModule.algebraMap_end_bijective {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] (hq : IsGenericQuantumParameter q) : Function.Bijective ⇑(algebraMap ℂ (Module.End (UqSl2 q) (LadderModule q m ε)))

Schur's lemma for L_m^ε: at a generic parameter, every UqSl2 q-endomorphism of L_m^ε is multiplication by a unique complex scalar.

theorem TauCeti.UqSl2.LadderModule.trace_rep_kInv {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] (hq : q - q⁻¹ ≠ 0) : (LinearMap.trace ℂ (LadderModule q m ε)) ((rep q m ε) (kInv q)) = ↑↑ε * quantumInteger q (↑m + 1)

The trace of K⁻¹ on L_m^ε is ε [m + 1]_q.

theorem TauCeti.UqSl2.LadderModule.trace_rep_k {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] (hq : q - q⁻¹ ≠ 0) : (LinearMap.trace ℂ (LadderModule q m ε)) ((rep q m ε) (k q)) = ↑↑ε * quantumInteger q (↑m + 1)

The trace of K on L_m^ε is ε [m + 1]_q, the same as the trace of K⁻¹.

theorem TauCeti.UqSl2.LadderModule.nonempty_linearEquiv_iff {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] (hq : IsGenericQuantumParameter q) {n : ℕ} {δ : ℤˣ} : Nonempty (LadderModule q m ε ≃ₗ[UqSl2 q] LadderModule q n δ) ↔ m = n ∧ ε = δ

At a generic parameter, L_m^ε and L_n^δ are isomorphic exactly when m = n and ε = δ.

theorem TauCeti.UqSl2.LadderModule.isEmpty_linearEquiv_of_ne {q : ℂ} {m : ℕ} {ε : ℤˣ} [Fact (q ≠ 0)] (hq : IsGenericQuantumParameter q) {n : ℕ} {δ : ℤˣ} (h : m ≠ n ∨ ε ≠ δ) : IsEmpty (LadderModule q m ε ≃ₗ[UqSl2 q] LadderModule q n δ)

At a generic parameter, no module isomorphism exists between L_m^ε and L_n^δ when m ≠ n or ε ≠ δ.