noncomputable def qAnalog {k : Type u_1} [Field k] (q : k) (n : ℕ) : k

The q-analog [n]_q = (q^n - q^{-n}) / (q - q^{-1}) of a natural number n.

noncomputable def qAnalogFactorial {k : Type u_1} [Field k] (q : k) (n : ℕ) : k

The q-analog factorial [n]_q! = ∏_{l=1}^{n} [l]_q.

noncomputable def qSerreCoeff {k : Type u_1} [Field k] (q : k) (N l : ℕ) : k

The coefficient (-1)^l / ([l]_q! · [N-l]_q!) appearing in the q-Serre relations.

theorem qAnalog_one {k : Type u_1} [Field k] (q : k) (hq : q - q⁻¹ ≠ 0) : qAnalog q 1 = 1

The q-analog of 1 equals 1, provided q - q⁻¹ ≠ 0.

structure CartanDatum (r : ℕ) : Type

A Cartan datum of rank r: a symmetrizable Cartan matrix together with a choice of symmetrizing positive integers d_i.

• cartanMatrix : Fin r → Fin r → ℤ
• symm : Fin r → ℕ
• diag (i : Fin r) : self.cartanMatrix i i = 2
• off_diag_nonpos (i j : Fin r) : i ≠ j → self.cartanMatrix i j ≤ 0
• symm_pos (i : Fin r) : 0 < self.symm i
• symmetrizable (i j : Fin r) : ↑(self.symm i) * self.cartanMatrix i j = ↑(self.symm j) * self.cartanMatrix j i

def CartanDatum.sl2 : CartanDatum 1

The rank-1 Cartan datum for sl_2: Cartan matrix [2] with symmetrizer 1.

class QuantumGroup {r : ℕ} (C : CartanDatum r) (k : Type u) [Field k] (A : Type v) [Ring A] [HopfAlgebra k A] : Type (max u v)

Definition 1.26.2 (Etingof–Gelaki–Nikshych–Ostrik): The quantum group U_q(g) attached to a Cartan datum C. It is the Hopf algebra over k generated by elements E_i, F_i and invertible elements K_i (with inverses Kinv_i), subject to the standard commutation, Cartan, and q-Serre relations, with comultiplication Δ(K_i) = K_i ⊗ K_i, Δ(E_i) = E_i ⊗ K_i + 1 ⊗ E_i, Δ(F_i) = F_i ⊗ 1 + K_i^{-1} ⊗ F_i.

• q : k
• hq_ne_zero : q C A ≠ 0
• hq_sq_ne_one : q C A ^ 2 ≠ 1
• E : Fin r → A
• F : Fin r → A
• K : Fin r → A
• Kinv : Fin r → A
• K_mul_Kinv (i : Fin r) : K C k i * Kinv C k i = 1
• Kinv_mul_K (i : Fin r) : Kinv C k i * K C k i = 1
• K_comm (i j : Fin r) : K C k i * K C k j = K C k j * K C k i
• K_E_Kinv (i j : Fin r) : K C k i * E C k j * Kinv C k i = q C A ^ C.cartanMatrix i j • E C k j
• K_F_Kinv (i j : Fin r) : K C k i * F C k j * Kinv C k i = q C A ^ (-C.cartanMatrix i j) • F C k j
• EF_comm (i j : Fin r) : E C k i * F C k j - F C k j * E C k i = if i = j then (q C A ^ ↑(C.symm i) - q C A ^ (-↑(C.symm i)))⁻¹ • (K C k i ^ C.symm i - Kinv C k i ^ C.symm i) else 0
• qSerre_E (i j : Fin r) : i ≠ j → ∑ l ∈ Finset.range ((1 - C.cartanMatrix i j).toNat + 1), qSerreCoeff (q C A ^ ↑(C.symm i)) (1 - C.cartanMatrix i j).toNat l • (E C k i ^ ((1 - C.cartanMatrix i j).toNat - l) * E C k j * E C k i ^ l) = 0
• qSerre_F (i j : Fin r) : i ≠ j → ∑ l ∈ Finset.range ((1 - C.cartanMatrix i j).toNat + 1), qSerreCoeff (q C A ^ ↑(C.symm i)) (1 - C.cartanMatrix i j).toNat l • (F C k i ^ ((1 - C.cartanMatrix i j).toNat - l) * F C k j * F C k i ^ l) = 0
• comul_K (i : Fin r) : CoalgebraStruct.comul (K C k i) = K C k i ⊗ₜ[k] K C k i
• comul_E (i : Fin r) : CoalgebraStruct.comul (E C k i) = E C k i ⊗ₜ[k] K C k i + 1 ⊗ₜ[k] E C k i
• comul_F (i : Fin r) : CoalgebraStruct.comul (F C k i) = F C k i ⊗ₜ[k] 1 + Kinv C k i ⊗ₜ[k] F C k i

theorem QuantumGroup.hopf_unique_from_generators {k : Type u_1} [Field k] {r : ℕ} {C : CartanDatum r} {A : Type v} [Ring A] [HopfAlgebra k A] [h : QuantumGroup C k A] (f : A →ₗ[k] TensorProduct k A A) (hf_alg : ∀ (a b : A), f (a * b) = f a * f b) (hf_K : ∀ (i : Fin r), f (K C k i) = K C k i ⊗ₜ[k] K C k i) (hf_E : ∀ (i : Fin r), f (E C k i) = E C k i ⊗ₜ[k] K C k i + 1 ⊗ₜ[k] E C k i) (hf_F : ∀ (i : Fin r), f (F C k i) = F C k i ⊗ₜ[k] 1 + Kinv C k i ⊗ₜ[k] F C k i) (a : A) : f a = CoalgebraStruct.comul a

Theorem 1.26.3 (Etingof–Gelaki–Nikshych–Ostrik): There exists a unique Hopf algebra structure on U_q(g) whose coproduct satisfies the prescribed values on the generators K_i, E_i, F_i. Any k-linear algebra map f : A → A ⊗ A agreeing with the comultiplication on generators must agree everywhere.