def IsPrimitiveElement (R : Type u_1) [CommRing R] (H : Type u_2) [Ring H] [Bialgebra R H] (x : H) : Prop

An element x of a bialgebra H is primitive if Δ(x) = x ⊗ 1 + 1 ⊗ x (Definition 1.24.2 of Etingof–Gelaki–Nikshych–Ostrik).

def primitiveElements (R : Type u_1) [CommRing R] (H : Type u_2) [Ring H] [Bialgebra R H] : Submodule R H

The submodule Prim(H) of primitive elements of a bialgebra H.

class QuantumSl2 (k : Type u) [Field k] (A : Type v) [Ring A] [HopfAlgebra k A] : Type (max u v)

A QuantumSl2 k A structure bundles the quantum group U_q(sl_2) data on a k-Hopf algebra A: a parameter q ≠ 0 with q^2 ≠ 1, generators K, E, F and an inverse Kinv of K, the standard Drinfeld–Jimbo relations KEK^{-1} = q^2 E, KFK^{-1} = q^{-2} F, [E, F] = (K - K^{-1})/(q - q^{-1}), and the standard formulas for the comultiplication, counit and antipode on the generators.

• q : k
• hq_ne_zero : q A ≠ 0
• hq_sq_ne_one : q A ^ 2 ≠ 1
• K : A
• Kinv : A
• E : A
• F : A
• K_mul_Kinv : K k * Kinv k = 1
• Kinv_mul_K : Kinv k * K k = 1
• K_E_Kinv : K k * E k * Kinv k = q A ^ 2 • E k
• K_F_Kinv : K k * F k * Kinv k = (q A ^ 2)⁻¹ • F k
• EF_comm : E k * F k - F k * E k = (q A - (q A)⁻¹)⁻¹ • (K k - Kinv k)
• comul_K : CoalgebraStruct.comul (K k) = K k ⊗ₜ[k] K k
• comul_E : CoalgebraStruct.comul (E k) = E k ⊗ₜ[k] K k + 1 ⊗ₜ[k] E k
• comul_F : CoalgebraStruct.comul (F k) = F k ⊗ₜ[k] 1 + Kinv k ⊗ₜ[k] F k
• counit_K : CoalgebraStruct.counit (K k) = 1
• counit_E : CoalgebraStruct.counit (E k) = 0
• counit_F : CoalgebraStruct.counit (F k) = 0
• antipode_K : (HopfAlgebraStruct.antipode k) (K k) = Kinv k
• antipode_E : (HopfAlgebraStruct.antipode k) (E k) = -(E k * Kinv k)
• antipode_F : (HopfAlgebraStruct.antipode k) (F k) = -(K k * F k)

@[reducible, inline]

abbrev Definition_1_25_1 (k : Type u) [Field k] (A : Type v) [Ring A] [HopfAlgebra k A] : Type (max u v)

Reference abbreviation for Definition 1.25.1: the quantum group U_q(sl_2).

theorem QuantumSl2.comul_Kinv {k : Type u} [Field k] {A : Type v} [Ring A] [HopfAlgebra k A] [h : QuantumSl2 k A] : CoalgebraStruct.comul (Kinv k) = Kinv k ⊗ₜ[k] Kinv k

The comultiplication of K^{-1} equals K^{-1} ⊗ K^{-1}.

theorem QuantumSl2.counit_Kinv {k : Type u} [Field k] {A : Type v} [Ring A] [HopfAlgebra k A] [h : QuantumSl2 k A] : CoalgebraStruct.counit (Kinv k) = 1

The counit of K^{-1} equals 1.

theorem QuantumSl2.antipode_Kinv {k : Type u} [Field k] {A : Type v} [Ring A] [HopfAlgebra k A] [h : QuantumSl2 k A] : (HopfAlgebraStruct.antipode k) (Kinv k) = K k

The antipode of K^{-1} equals K.

noncomputable def QuantumSl2.cartanElement {k : Type u} [Field k] {A : Type v} [Ring A] [HopfAlgebra k A] [h : QuantumSl2 k A] : A

The Cartan-type element (q - q^{-1})^{-1} · (K - K^{-1}) of the quantum group.

theorem QuantumSl2.Theorem_1_25_2_Uq_sl2_Hopf {k : Type u} [Field k] {A : Type v} [Ring A] [HopfAlgebra k A] [h : QuantumSl2 k A] : CoalgebraStruct.comul (K k) = K k ⊗ₜ[k] K k ∧ CoalgebraStruct.comul (E k) = E k ⊗ₜ[k] K k + 1 ⊗ₜ[k] E k ∧ CoalgebraStruct.comul (F k) = F k ⊗ₜ[k] 1 + Kinv k ⊗ₜ[k] F k ∧ CoalgebraStruct.comul (Kinv k) = Kinv k ⊗ₜ[k] Kinv k ∧ CoalgebraStruct.counit (K k) = 1 ∧ CoalgebraStruct.counit (E k) = 0 ∧ CoalgebraStruct.counit (F k) = 0 ∧ CoalgebraStruct.counit (Kinv k) = 1 ∧ (HopfAlgebraStruct.antipode k) (K k) = Kinv k ∧ (HopfAlgebraStruct.antipode k) (E k) = -(E k * Kinv k) ∧ (HopfAlgebraStruct.antipode k) (F k) = -(K k * F k) ∧ (HopfAlgebraStruct.antipode k) (Kinv k) = K k

Theorem 1.25.2 (Etingof–Gelaki–Nikshych–Ostrik): There exists a unique Hopf algebra structure on U_q(sl_2) given by Δ(K) = K ⊗ K, Δ(E) = E ⊗ K + 1 ⊗ E, Δ(F) = F ⊗ 1 + K^{-1} ⊗ F. This theorem records the explicit values of comultiplication, counit, and antipode on K, K^{-1}, E, F.