Documentation

TauCeti.QuantumGroups.UqSl2.Basic

The quantized enveloping algebra of sl₂ #

This file defines the algebra UqSl2 q by generators E, F, K, and K⁻¹ and relations

K K⁻¹ = K⁻¹ K = 1,
K E = q² E K and K F = q⁻² F K, and
E F - F E = (K - K⁻¹) / (q - q⁻¹).

The quotient is defined for every complex q. The generic representation theory uses parameters for which q ≠ 0 and no positive power of q is one; in particular its displayed denominator is nonzero. The presentation-level identities below hold for every q; when q = 0, the relations force E = F = 0.

The quotient construction supplies a universal property for tuples satisfying these relations. Since the generators generate the algebra, a property of elements holding for the scalars and the generators and closed under sums and products holds everywhere (TauCeti.UqSl2.induction). A complex-linear map between UqSl2 q-modules that commutes with E, F and K is therefore UqSl2 q-linear, and an element of UqSl2 q that commutes with E, F and K is central. We also package K as a unit and derive the commutation rules with K⁻¹ and with K on the right, together with the invariance K F E K⁻¹ = F E; these are the basic presentation-level identities used when putting words into triangular order. Establishing a PBW basis, and hence nontriviality of this presentation, requires additional Ore-extension arguments and is not part of the presentation API: TauCeti.QuantumGroups.UqSl2.OreTower identifies UqSl2 q, for nonzero q, with an iterated Ore extension of ℂ[K, K⁻¹].

Main definitions #

TauCeti.UqSl2: the quotient algebra.
TauCeti.UqSl2.GeneratorTuple: a tuple in a complex algebra satisfying the defining relations.
TauCeti.UqSl2.lift: the algebra map induced by such a tuple.
TauCeti.UqSl2.kUnit: the unit represented by K.

References #

A. Virelizier, Quantum groups, Sections 2.3--2.4, for this rank-one presentation and Hopf convention.
The quotient and universal-property API follows the construction pattern of Mathlib.LinearAlgebra.CliffordAlgebra.Basic.

inductive TauCeti.UqSl2.Generator :

The four generators of the presentation of UqSl2 q.

Instances For

@[instance_reducible]

instance TauCeti.UqSl2.instDecidableEqGenerator :

DecidableEq Generator

inductive TauCeti.UqSl2.Rel (q : ℂ) :

FreeAlgebra ℂ Generator → FreeAlgebra ℂ Generator → Prop

The defining relations for the quantized enveloping algebra of sl₂, as a relation on the free complex algebra on E, F, K, and K⁻¹.

k_mul_kInv {q : ℂ} : Rel q (FreeAlgebra.ι ℂ Generator.k * FreeAlgebra.ι ℂ Generator.kInv) 1
kInv_mul_k {q : ℂ} : Rel q (FreeAlgebra.ι ℂ Generator.kInv * FreeAlgebra.ι ℂ Generator.k) 1
k_mul_e {q : ℂ} : Rel q (FreeAlgebra.ι ℂ Generator.k * FreeAlgebra.ι ℂ Generator.e) (q ^ 2 • (FreeAlgebra.ι ℂ Generator.e * FreeAlgebra.ι ℂ Generator.k))
k_mul_f {q : ℂ} : Rel q (FreeAlgebra.ι ℂ Generator.k * FreeAlgebra.ι ℂ Generator.f) (q⁻¹ ^ 2 • (FreeAlgebra.ι ℂ Generator.f * FreeAlgebra.ι ℂ Generator.k))
e_mul_f_sub_f_mul_e {q : ℂ} : Rel q (FreeAlgebra.ι ℂ Generator.e * FreeAlgebra.ι ℂ Generator.f - FreeAlgebra.ι ℂ Generator.f * FreeAlgebra.ι ℂ Generator.e) ((q - q⁻¹)⁻¹ • (FreeAlgebra.ι ℂ Generator.k - FreeAlgebra.ι ℂ Generator.kInv))

Instances For

def TauCeti.UqSl2 (q : ℂ) :

The quantized enveloping algebra of sl₂ with parameter q, presented by generators E, F, K, and K⁻¹ and the standard rank-one relations.

Instances For

@[instance_reducible]

instance TauCeti.instRingUqSl2 (q : ℂ) :

@[instance_reducible]

instance TauCeti.instAlgebraComplexUqSl2 (q : ℂ) :

Algebra ℂ (UqSl2 q)

def TauCeti.UqSl2.mkAlgHom (q : ℂ) :

FreeAlgebra ℂ Generator →ₐ[ℂ ] UqSl2 q

The quotient map from the free algebra to UqSl2 q.

Instances For

def TauCeti.UqSl2.generator (q : ℂ) (g : Generator) :

The image of a free generator in UqSl2 q.

Instances For

@[simp]

theorem TauCeti.UqSl2.mkAlgHom_ι (q : ℂ) (g : Generator) :

(mkAlgHom q) (FreeAlgebra.ι ℂ g) = generator q g

The quotient map takes a free generator to the corresponding generator of UqSl2 q.

@[reducible, inline]

abbrev TauCeti.UqSl2.e (q : ℂ) :

The raising generator E of UqSl2 q.

Instances For

@[reducible, inline]

abbrev TauCeti.UqSl2.f (q : ℂ) :

The lowering generator F of UqSl2 q.

Instances For

@[reducible, inline]

abbrev TauCeti.UqSl2.k (q : ℂ) :

The weight generator K of UqSl2 q.

Instances For

@[reducible, inline]

abbrev TauCeti.UqSl2.kInv (q : ℂ) :

The inverse weight generator K⁻¹ of UqSl2 q.

Instances For

@[simp]

theorem TauCeti.UqSl2.k_mul_kInv {q : ℂ} :

k q * kInv q = 1

K is a left inverse of K⁻¹.

@[simp]

theorem TauCeti.UqSl2.kInv_mul_k {q : ℂ} :

kInv q * k q = 1

K⁻¹ is a left inverse of K.

theorem TauCeti.UqSl2.k_mul_e {q : ℂ} :

k q * e q = q ^ 2 • (e q * k q)

The defining commutation relation K E = q² E K.

theorem TauCeti.UqSl2.k_mul_f {q : ℂ} :

k q * f q = q⁻¹ ^ 2 • (f q * k q)

The defining commutation relation K F = q⁻² F K.

theorem TauCeti.UqSl2.e_mul_f_sub_f_mul_e {q : ℂ} :

e q * f q - f q * e q = (q - q⁻¹)⁻¹ • (k q - kInv q)

The defining commutator relation between E and F.

def TauCeti.UqSl2.kUnit (q : ℂ) :

The generator K, packaged with the specified inverse K⁻¹.

Instances For

@[simp]

theorem TauCeti.UqSl2.kUnit_val {q : ℂ} :

↑(kUnit q) = k q

The value of kUnit q is the generator K.

@[simp]

theorem TauCeti.UqSl2.kUnit_inv {q : ℂ} :

↑(kUnit q)⁻¹ = kInv q

The inverse of kUnit q has value K⁻¹.

@[simp]

theorem TauCeti.UqSl2.k_mul_kInv_mul {q : ℂ} (x : UqSl2 q) :

k q * (kInv q * x) = x

Left multiplication by K cancels left multiplication by K⁻¹.

@[simp]

theorem TauCeti.UqSl2.kInv_mul_k_mul {q : ℂ} (x : UqSl2 q) :

kInv q * (k q * x) = x

Left multiplication by K⁻¹ cancels left multiplication by K.

theorem TauCeti.UqSl2.k_mul_kUnit_zpow {q : ℂ} (b : ℤ) :

k q * ↑(kUnit q ^ b) = ↑(kUnit q ^ (b + 1))

Multiplying an integer power of K by K on the left raises the exponent by one.

theorem TauCeti.UqSl2.kInv_mul_kUnit_zpow {q : ℂ} (b : ℤ) :

kInv q * ↑(kUnit q ^ b) = ↑(kUnit q ^ (b - 1))

Multiplying an integer power of K by K⁻¹ on the left lowers the exponent by one.

@[simp]

theorem TauCeti.UqSl2.e_zero :

e 0 = 0

At q = 0 the relation K E = 0 • E K forces E = 0.

@[simp]

theorem TauCeti.UqSl2.f_zero :

f 0 = 0

At q = 0 the relation K F = 0 • F K forces F = 0.

theorem TauCeti.UqSl2.e_mul_kInv {q : ℂ} :

e q * kInv q = q ^ 2 • (kInv q * e q)

The relation E K⁻¹ = q² K⁻¹ E, obtained from the defining K E relation.

theorem TauCeti.UqSl2.kInv_mul_e {q : ℂ} :

kInv q * e q = q⁻¹ ^ 2 • (e q * kInv q)

The inverse-generator commutation relation K⁻¹ E = q⁻² E K⁻¹.

theorem TauCeti.UqSl2.f_mul_kInv {q : ℂ} :

f q * kInv q = q⁻¹ ^ 2 • (kInv q * f q)

The relation F K⁻¹ = q⁻² K⁻¹ F, obtained from the defining K F relation.

theorem TauCeti.UqSl2.kInv_mul_f {q : ℂ} :

kInv q * f q = q ^ 2 • (f q * kInv q)

The inverse-generator commutation relation K⁻¹ F = q² F K⁻¹.

theorem TauCeti.UqSl2.e_mul_k {q : ℂ} :

e q * k q = q⁻¹ ^ 2 • (k q * e q)

The relation E K = q⁻² K E, obtained by conjugating K⁻¹ E = q⁻² E K⁻¹ by K.

theorem TauCeti.UqSl2.f_mul_k {q : ℂ} :

f q * k q = q ^ 2 • (k q * f q)

The relation F K = q² K F, obtained by conjugating K⁻¹ F = q² F K⁻¹ by K.

theorem TauCeti.UqSl2.k_mul_f_mul_e_mul_kInv {q : ℂ} :

k q * f q * (e q * kInv q) = f q * e q

Conjugation by K fixes F E: K F E K⁻¹ = F E.

structure TauCeti.UqSl2.GeneratorTuple (q : ℂ) (A : Type u_1) [Ring A] [Algebra ℂ A] :

Type u_1

A tuple in a complex algebra satisfying the defining relations of UqSl2 q.

e : A
The proposed image of E.
f : A
The proposed image of F.
k : A
The proposed image of K.
kInv : A
The proposed image of K⁻¹.
k_mul_kInv : self.k * self.kInv = 1
The proposed images of K and K⁻¹ multiply to one in this order.
kInv_mul_k : self.kInv * self.k = 1
The proposed images of K⁻¹ and K multiply to one in this order.
k_mul_e : self.k * self.e = q ^ 2 • (self.e * self.k)
The proposed images satisfy K E = q² E K.
k_mul_f : self.k * self.f = q⁻¹ ^ 2 • (self.f * self.k)
The proposed images satisfy K F = q⁻² F K.
e_mul_f_sub_f_mul_e : self.e * self.f - self.f * self.e = (q - q⁻¹)⁻¹ • (self.k - self.kInv)
The proposed images satisfy the E--F commutator relation.

Instances For

theorem TauCeti.UqSl2.GeneratorTuple.ext {q : ℂ} {A : Type u_1} {inst✝ : Ring A} {inst✝¹ : Algebra ℂ A} {x y : GeneratorTuple q A} (e : x.e = y.e) (f : x.f = y.f) (k : x.k = y.k) (kInv : x.kInv = y.kInv) :

x = y

theorem TauCeti.UqSl2.GeneratorTuple.ext_iff {q : ℂ} {A : Type u_1} {inst✝ : Ring A} {inst✝¹ : Algebra ℂ A} {x y : GeneratorTuple q A} :

x = y ↔ x.e = y.e ∧ x.f = y.f ∧ x.k = y.k ∧ x.kInv = y.kInv

def TauCeti.UqSl2.GeneratorTuple.toFun {q : ℂ} {A : Type u_1} [Ring A] [Algebra ℂ A] (x : GeneratorTuple q A) :

Generator → A

The function on generator names underlying a generator tuple.

Instances For

@[simp]

theorem TauCeti.UqSl2.GeneratorTuple.toFun_e {q : ℂ} {A : Type u_1} [Ring A] [Algebra ℂ A] (x : GeneratorTuple q A) :

x.toFun Generator.e = x.e

The function underlying a tuple takes the raising label to its raising element.

@[simp]

theorem TauCeti.UqSl2.GeneratorTuple.toFun_f {q : ℂ} {A : Type u_1} [Ring A] [Algebra ℂ A] (x : GeneratorTuple q A) :

x.toFun Generator.f = x.f

The function underlying a tuple takes the lowering label to its lowering element.

@[simp]

theorem TauCeti.UqSl2.GeneratorTuple.toFun_k {q : ℂ} {A : Type u_1} [Ring A] [Algebra ℂ A] (x : GeneratorTuple q A) :

x.toFun Generator.k = x.k

The function underlying a tuple takes the weight label to its weight element.

@[simp]

theorem TauCeti.UqSl2.GeneratorTuple.toFun_kInv {q : ℂ} {A : Type u_1} [Ring A] [Algebra ℂ A] (x : GeneratorTuple q A) :

x.toFun Generator.kInv = x.kInv

The function underlying a tuple takes the inverse-weight label to its inverse-weight element.

def TauCeti.UqSl2.lift {q : ℂ} {A : Type u_1} [Ring A] [Algebra ℂ A] (x : GeneratorTuple q A) :

UqSl2 q →ₐ[ℂ ] A

The universal property of the presentation: a tuple satisfying the defining relations extends to a complex algebra map from UqSl2 q.

Instances For

@[simp]

theorem TauCeti.UqSl2.lift_generator {q : ℂ} {A : Type u_1} [Ring A] [Algebra ℂ A] (x : GeneratorTuple q A) (g : Generator) :

(lift x) (generator q g) = x.toFun g

The map induced by a generator tuple has the prescribed value on every generator.

theorem TauCeti.UqSl2.hom_ext {q : ℂ} {A : Type u_1} [Ring A] [Algebra ℂ A] {F G : UqSl2 q →ₐ[ℂ ] A} (he : F (e q) = G (e q)) (hf : F (f q) = G (f q)) (hk : F (k q) = G (k q)) :

F = G

Two algebra maps from UqSl2 q agreeing on E, F and K are equal; agreement on K⁻¹ follows since it is the inverse of K.

theorem TauCeti.UqSl2.hom_ext_iff {q : ℂ} {A : Type u_1} [Ring A] [Algebra ℂ A] {F G : UqSl2 q →ₐ[ℂ ] A} :

F = G ↔ F (e q) = G (e q) ∧ F (f q) = G (f q) ∧ F (k q) = G (k q)

theorem TauCeti.UqSl2.adjoin_range_generator (q : ℂ) :

Algebra.adjoin ℂ (Set.range (generator q)) = ⊤

The four presentation generators generate the entire algebra.

theorem TauCeti.UqSl2.induction {q : ℂ} {C : UqSl2 q → Prop} (algebraMap : ∀ (c : ℂ), C ((algebraMap ℂ (UqSl2 q)) c)) (generator : ∀ (g : Generator), C (generator q g)) (mul : ∀ (a b : UqSl2 q), C a → C b → C (a * b)) (add : ∀ (a b : UqSl2 q), C a → C b → C (a + b)) (a : UqSl2 q) :

C a

An induction principle for UqSl2 q: a property of its elements that holds for the scalars and the four generators and is closed under products and sums holds everywhere.

theorem LinearMap.map_smul_of_commute_uqSl2 {q : ℂ} {V : Type u_2} {W : Type u_3} [AddCommGroup V] [Module ℂ V] [Module (TauCeti.UqSl2 q) V] [IsScalarTower ℂ (TauCeti.UqSl2 q) V] [AddCommGroup W] [Module ℂ W] [Module (TauCeti.UqSl2 q) W] [IsScalarTower ℂ (TauCeti.UqSl2 q) W] (φ : V →ₗ[ℂ ] W) (he : ∀ (x : V), φ (TauCeti.UqSl2.e q • x) = TauCeti.UqSl2.e q • φ x) (hf : ∀ (x : V), φ (TauCeti.UqSl2.f q • x) = TauCeti.UqSl2.f q • φ x) (hk : ∀ (x : V), φ (TauCeti.UqSl2.k q • x) = TauCeti.UqSl2.k q • φ x) (a : TauCeti.UqSl2 q) (x : V) :

φ (a • x) = a • φ x

A complex-linear map between UqSl2 q-modules that commutes with E, F and K commutes with every element of UqSl2 q; commuting with K⁻¹ is automatic.

theorem TauCeti.UqSl2.commute_of_commute_generators {q : ℂ} {z : UqSl2 q} (he : Commute (e q) z) (hf : Commute (f q) z) (hk : Commute (k q) z) (a : UqSl2 q) :

An element of UqSl2 q that commutes with E, F and K commutes with every element of UqSl2 q; commuting with K⁻¹ is automatic.

theorem Submodule.smul_mem_of_uqSl2_generators {q : ℂ} {V : Type u_2} [AddCommGroup V] [Module ℂ V] [Module (TauCeti.UqSl2 q) V] [IsScalarTower ℂ (TauCeti.UqSl2 q) V] (W : Submodule ℂ V) (he : ∀ x ∈ W, TauCeti.UqSl2.e q • x ∈ W) (hf : ∀ x ∈ W, TauCeti.UqSl2.f q • x ∈ W) (hk : ∀ x ∈ W, TauCeti.UqSl2.k q • x ∈ W) (hkInv : ∀ x ∈ W, TauCeti.UqSl2.kInv q • x ∈ W) (a : TauCeti.UqSl2 q) {x : V} (hx : x ∈ W) :

a • x ∈ W

A complex subspace of a UqSl2 q-module that is stable under E, F, K and K⁻¹ is stable under every element of UqSl2 q.

def TauCeti.UqSl2.liftEquiv {q : ℂ} {A : Type u_1} [Ring A] [Algebra ℂ A] :

(UqSl2 q →ₐ[ℂ ] A) ≃ GeneratorTuple q A

Algebra maps from UqSl2 q are equivalent to tuples satisfying its defining relations.

Instances For

@[simp]

theorem TauCeti.UqSl2.liftEquiv_apply_e {q : ℂ} {A : Type u_1} [Ring A] [Algebra ℂ A] (F : UqSl2 q →ₐ[ℂ ] A) :

(liftEquiv F).e = F (e q)

The tuple associated to an algebra map records its value on E.

@[simp]

theorem TauCeti.UqSl2.liftEquiv_apply_f {q : ℂ} {A : Type u_1} [Ring A] [Algebra ℂ A] (F : UqSl2 q →ₐ[ℂ ] A) :

(liftEquiv F).f = F (f q)

The tuple associated to an algebra map records its value on F.

@[simp]

theorem TauCeti.UqSl2.liftEquiv_apply_k {q : ℂ} {A : Type u_1} [Ring A] [Algebra ℂ A] (F : UqSl2 q →ₐ[ℂ ] A) :

(liftEquiv F).k = F (k q)

The tuple associated to an algebra map records its value on K.

@[simp]

theorem TauCeti.UqSl2.liftEquiv_apply_kInv {q : ℂ} {A : Type u_1} [Ring A] [Algebra ℂ A] (F : UqSl2 q →ₐ[ℂ ] A) :

(liftEquiv F).kInv = F (kInv q)

The tuple associated to an algebra map records its value on K⁻¹.

@[simp]

theorem TauCeti.UqSl2.liftEquiv_symm_apply {q : ℂ} {A : Type u_1} [Ring A] [Algebra ℂ A] (x : GeneratorTuple q A) :

liftEquiv.symm x = lift x

The inverse universal-property equivalence is the map induced by the tuple.