The Casimir element of U_q(sl₂)

This file defines the quantum Casimir element Ω = F E + (q K + q⁻¹ K⁻¹) / (q - q⁻¹)² of UqSl2 q, proves that it also equals E F + (q⁻¹ K + q K⁻¹) / (q - q⁻¹)², and proves that it is central. These identities hold for every complex parameter q.

On a vector of weight μ killed by E, the Casimir element acts by the scalar casimirScalar q μ = (q μ + q⁻¹ μ⁻¹) / (q - q⁻¹)², and by centrality it acts by the same scalar on the cyclic submodule generated by such a vector. On a vector of weight μ killed by F it acts by casimirScalar q μ⁻¹. For the signed highest weights ε q^m, with m : ℕ and a sign ε : ℤˣ, the scalar is ε (q^(m+1) + q^(-(m+1))) / (q - q⁻¹)², and at a generic parameter these scalars are pairwise distinct. This is the input for splitting a finite-dimensional module into generalized eigenspaces of the Casimir element, one for each signed highest weight.

Main definitions

• TauCeti.UqSl2.casimir: the Casimir element Ω.
• TauCeti.UqSl2.casimirScalar: the scalar by which Ω acts on a highest-weight vector.
• TauCeti.UqSl2.casimirBlock: the generalized eigenspace of Ω for a scalar, as a submodule.

Main results

• TauCeti.UqSl2.casimir_mem_center: Ω is central.
• TauCeti.UqSl2.casimir_smul_of_e_smul_eq_zero: the action of Ω on a highest-weight vector.
• TauCeti.UqSl2.casimirScalar_eq_casimirScalar_iff: two nonzero weights have the same Casimir scalar exactly when they are equal or related by μ ↦ q⁻² μ⁻¹.
• TauCeti.UqSl2.casimirScalar_eq_of_mem_casimirBlock and TauCeti.UqSl2.casimirScalar_inv_eq_of_mem_casimirBlock: a nonzero highest-weight vector of weight μ (resp. lowest-weight vector) lies only in the Casimir block for casimirScalar q μ (resp. casimirScalar q μ⁻¹).
• TauCeti.UqSl2.map_casimirBlock_le: module maps send Casimir blocks into Casimir blocks.
• TauCeti.UqSl2.casimirScalar_units_mul_pow_inj: at a generic parameter, the scalars of the signed highest weights ε q^m determine m and ε.
• TauCeti.UqSl2.iSup_casimirBlock_eq_top: a finite-dimensional module is the sum of its Casimir blocks.

References

• A. Virelizier, Quantum groups, Sections 2.3--2.4.
• C. Kassel, Quantum Groups, Graduate Texts in Mathematics 155, Section VI.4.

noncomputable def TauCeti.UqSl2.casimir (q : ℂ) : UqSl2 q

The quantum Casimir element Ω = F E + (q K + q⁻¹ K⁻¹) / (q - q⁻¹)² of UqSl2 q.

theorem TauCeti.UqSl2.casimir_def {q : ℂ} : casimir q = f q * e q + ((q - q⁻¹) ^ 2)⁻¹ • (q • k q + q⁻¹ • kInv q)

The defining formula for the Casimir element.

theorem TauCeti.UqSl2.casimir_eq_e_mul_f {q : ℂ} : casimir q = e q * f q + ((q - q⁻¹) ^ 2)⁻¹ • (q⁻¹ • k q + q • kInv q)

The Casimir element in the opposite normal order: Ω = E F + (q⁻¹ K + q K⁻¹) / (q - q⁻¹)².

theorem TauCeti.UqSl2.commute_casimir {q : ℂ} (a : UqSl2 q) : Commute a (casimir q)

Every element of UqSl2 q commutes with the Casimir element.

theorem TauCeti.UqSl2.casimir_mem_center {q : ℂ} : casimir q ∈ Subalgebra.center ℂ (UqSl2 q)

The Casimir element is central in UqSl2 q.

noncomputable def TauCeti.UqSl2.casimirScalar (q μ : ℂ) : ℂ

The scalar (q μ + q⁻¹ μ⁻¹) / (q - q⁻¹)² by which the Casimir element acts on a vector of weight μ killed by E.

theorem TauCeti.UqSl2.casimirScalar_def {q : ℂ} (μ : ℂ) : casimirScalar q μ = (q * μ + q⁻¹ * μ⁻¹) / (q - q⁻¹) ^ 2

The defining formula for the Casimir scalar.

theorem TauCeti.UqSl2.casimir_smul_of_e_smul_eq_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) : casimir q • v = casimirScalar q μ • v

The Casimir element acts on a vector of weight μ killed by E by casimirScalar q μ.

theorem TauCeti.UqSl2.casimir_smul_of_f_smul_eq_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 μ) (hf : f q • v = 0) : casimir q • v = casimirScalar q μ⁻¹ • v

The Casimir element acts on a vector of weight μ killed by F by casimirScalar q μ⁻¹.

theorem TauCeti.UqSl2.casimir_smul_smul_of_e_smul_eq_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) (a : UqSl2 q) : casimir q • a • v = casimirScalar q μ • a • v

The Casimir element acts by casimirScalar q μ on the whole cyclic submodule generated by a vector of weight μ killed by E.

noncomputable def TauCeti.UqSl2.casimirBlock (q : ℂ) (V : Type u_1) [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (c : ℂ) : Submodule (UqSl2 q) V

The Casimir block of V for a scalar c: the maximal generalized eigenspace of the action of the Casimir element for the eigenvalue c. It is a submodule since Ω is central.

theorem TauCeti.UqSl2.restrictScalars_casimirBlock {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (c : ℂ) : Submodule.restrictScalars ℂ (casimirBlock q V c) = ((Algebra.lsmul ℂ ℂ V) (casimir q)).maxGenEigenspace c

As a complex subspace, the Casimir block for c is the native maximal generalized eigenspace of the action of the Casimir element.

@[simp]

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

A vector lies in the Casimir block for c exactly when some power of Ω - c kills it.

theorem TauCeti.UqSl2.eq_of_casimir_smul_of_mem_casimirBlock {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {v : V} {s c : ℂ} (hs : casimir q • v = s • v) (hb : v ∈ casimirBlock q V c) (hv0 : v ≠ 0) : s = c

A vector on which the Casimir element acts by the scalar s lies in the Casimir block for c only if it vanishes or s = c.

theorem TauCeti.UqSl2.casimirScalar_eq_of_mem_casimirBlock {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {μ : ℂ} {v : V} {c : ℂ} (hv : v ∈ weightSpace q V μ) (he : e q • v = 0) (hb : v ∈ casimirBlock q V c) (hv0 : v ≠ 0) : casimirScalar q μ = c

A nonzero vector of weight μ killed by E lies in the Casimir block for c only if casimirScalar q μ = c.

theorem TauCeti.UqSl2.casimirScalar_inv_eq_of_mem_casimirBlock {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] {μ : ℂ} {v : V} {c : ℂ} (hv : v ∈ weightSpace q V μ) (hf : f q • v = 0) (hb : v ∈ casimirBlock q V c) (hv0 : v ≠ 0) : casimirScalar q μ⁻¹ = c

A nonzero vector of weight μ killed by F lies in the Casimir block for c only if casimirScalar q μ⁻¹ = c.

theorem TauCeti.UqSl2.map_casimirBlock_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) (c : ℂ) : Submodule.map φ (casimirBlock q V c) ≤ casimirBlock q W c

A module map sends the Casimir block for c into the Casimir block for c.

theorem TauCeti.UqSl2.casimirBlock_casimirBlock_eq_top {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] (c : ℂ) : casimirBlock q (↥(casimirBlock q V c)) c = ⊤

The Casimir block for c, viewed as a module itself, is its own Casimir block for c.

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

Casimir blocks for distinct scalars are independent.

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

A finite-dimensional module is the sum of its Casimir blocks.

instance TauCeti.UqSl2.finiteDimensional_casimirBlock {q : ℂ} {V : Type u_1} [AddCommGroup V] [Module ℂ V] [Module (UqSl2 q) V] [IsScalarTower ℂ (UqSl2 q) V] [FiniteDimensional ℂ V] (c : ℂ) : FiniteDimensional ℂ ↥(casimirBlock q V c)

A Casimir block of a finite-dimensional module is finite-dimensional.

theorem TauCeti.UqSl2.casimirScalar_units_mul_pow {q : ℂ} (ε : ℤˣ) (m : ℕ) : casimirScalar q (↑↑ε * q ^ m) = ↑↑ε * (q ^ (m + 1) + q⁻¹ ^ (m + 1)) / (q - q⁻¹) ^ 2

The Casimir scalar of the signed highest weight ε q^m is ε (q^(m+1) + q^(-(m+1))) / (q - q⁻¹)².

theorem TauCeti.UqSl2.casimirScalar_eq_casimirScalar_iff {q : ℂ} (hq : q - q⁻¹ ≠ 0) {μ ν : ℂ} (hμ : μ ≠ 0) (hν : ν ≠ 0) : casimirScalar q μ = casimirScalar q ν ↔ μ = ν ∨ q ^ 2 * μ * ν = 1

Two nonzero weights have the same Casimir scalar exactly when they are equal or related by the reflection μ ↦ q⁻² μ⁻¹.

theorem TauCeti.UqSl2.casimirScalar_units_mul_pow_inj {q : ℂ} (hq : IsGenericQuantumParameter q) {m n : ℕ} {ε δ : ℤˣ} : casimirScalar q (↑↑ε * q ^ m) = casimirScalar q (↑↑δ * q ^ n) ↔ m = n ∧ ε = δ

At a generic parameter, the Casimir scalars of the signed highest weights ε q^m are pairwise distinct: they determine both m and the sign ε.