structure SmallQuantumSl2 (n : ℕ) (k : Type u_1) [Field k] : Type u_1

A concrete representative of the small quantum group u_q(sl_2) as a k-vector space, recording an element by its coefficients on a finite n × n × n PBW basis.

• coeff : Fin n × Fin n × Fin n → k

theorem SmallQuantumSl2.ext_iff {n : ℕ} {k : Type u_1} {inst✝ : Field k} {x y : SmallQuantumSl2 n k} : x = y ↔ x.coeff = y.coeff

theorem SmallQuantumSl2.ext {n : ℕ} {k : Type u_1} {inst✝ : Field k} {x y : SmallQuantumSl2 n k} (coeff : x.coeff = y.coeff) : x = y

@[implicit_reducible]

noncomputable instance SmallQuantumSl2.instZero {n : ℕ} {k : Type u_1} [Field k] : Zero (SmallQuantumSl2 n k)

Zero element: the all-zero coefficient vector.

@[implicit_reducible]

noncomputable instance SmallQuantumSl2.instAdd {n : ℕ} {k : Type u_1} [Field k] : Add (SmallQuantumSl2 n k)

Coefficient-wise addition.

@[implicit_reducible]

noncomputable instance SmallQuantumSl2.instNeg {n : ℕ} {k : Type u_1} [Field k] : Neg (SmallQuantumSl2 n k)

Coefficient-wise negation.

@[implicit_reducible]

noncomputable instance SmallQuantumSl2.instSub {n : ℕ} {k : Type u_1} [Field k] : Sub (SmallQuantumSl2 n k)

Coefficient-wise subtraction.

@[implicit_reducible]

noncomputable instance SmallQuantumSl2.instSMul {n : ℕ} {k : Type u_1} [Field k] : SMul k (SmallQuantumSl2 n k)

Scalar multiplication by k on coefficients.

@[simp]

theorem SmallQuantumSl2.coeff_zero' {n : ℕ} {k : Type u_1} [Field k] (i : Fin n × Fin n × Fin n) : coeff 0 i = 0

Coefficients of the zero element vanish.

@[simp]

theorem SmallQuantumSl2.coeff_add {n : ℕ} {k : Type u_1} [Field k] (a b : SmallQuantumSl2 n k) (i : Fin n × Fin n × Fin n) : (a + b).coeff i = a.coeff i + b.coeff i

Coefficients of a sum are sums of coefficients.

@[simp]

theorem SmallQuantumSl2.coeff_neg {n : ℕ} {k : Type u_1} [Field k] (a : SmallQuantumSl2 n k) (i : Fin n × Fin n × Fin n) : (-a).coeff i = -a.coeff i

Coefficients of a negation are negations of coefficients.

@[simp]

theorem SmallQuantumSl2.coeff_sub {n : ℕ} {k : Type u_1} [Field k] (a b : SmallQuantumSl2 n k) (i : Fin n × Fin n × Fin n) : (a - b).coeff i = a.coeff i - b.coeff i

Coefficients of a difference are differences of coefficients.

@[simp]

theorem SmallQuantumSl2.coeff_smul {n : ℕ} {k : Type u_1} [Field k] (r : k) (a : SmallQuantumSl2 n k) (i : Fin n × Fin n × Fin n) : (r • a).coeff i = r * a.coeff i

Coefficients of a scalar multiple.

@[implicit_reducible]

noncomputable instance SmallQuantumSl2.instAddCommGroup {n : ℕ} {k : Type u_1} [Field k] : AddCommGroup (SmallQuantumSl2 n k)

Componentwise additive abelian group structure.

@[implicit_reducible]

noncomputable instance SmallQuantumSl2.instModule {n : ℕ} {k : Type u_1} [Field k] : Module k (SmallQuantumSl2 n k)

Componentwise k-module structure.

noncomputable def SmallQuantumSl2.toFunEquiv {n : ℕ} {k : Type u_1} [Field k] : SmallQuantumSl2 n k ≃ₗ[k] Fin n × Fin n × Fin n → k

Linear equivalence between SmallQuantumSl2 n k and the coordinate space Fin n × Fin n × Fin n → k.

instance SmallQuantumSl2.instFinite {n : ℕ} {k : Type u_1} [Field k] : Module.Finite k (SmallQuantumSl2 n k)

SmallQuantumSl2 n k is a finite k-module.

instance SmallQuantumSl2.finiteDimensional {n : ℕ} {k : Type u_1} [Field k] : FiniteDimensional k (SmallQuantumSl2 n k)

SmallQuantumSl2 n k is finite-dimensional over k.

noncomputable def SmallQuantumSl2.basisVec {n : ℕ} {k : Type u_1} [Field k] (i : Fin n × Fin n × Fin n) : SmallQuantumSl2 n k

The standard basis vector indexed by i, with coefficient 1 at i and 0 elsewhere.

@[simp]

theorem SmallQuantumSl2.coeff_basisVec {n : ℕ} {k : Type u_1} [Field k] (i j : Fin n × Fin n × Fin n) : (basisVec i).coeff j = if i = j then 1 else 0

Coefficient formula for basisVec.

theorem SmallQuantumSl2.coeff_finset_sum {n : ℕ} {k : Type u_1} [Field k] (s : Finset (Fin n × Fin n × Fin n)) (f : Fin n × Fin n × Fin n → SmallQuantumSl2 n k) (j : Fin n × Fin n × Fin n) : (∑ i ∈ s, f i).coeff j = ∑ i ∈ s, (f i).coeff j

Coefficients commute with finite sums.

inductive SmallQuantumRel (n : ℕ) (k : Type u_2) [Field k] (q : k) : FreeAlgebra k (Fin 3) → FreeAlgebra k (Fin 3) → Prop

Relations defining the small quantum sl_2 algebra u_q(sl_2) of dimension n: nilpotency relations K^n = 1, E^n = 0, F^n = 0 together with the q-commutation relations between K, E, F adapted to the small quantum group setting.

• K_pow_n {n : ℕ} {k : Type u_2} [Field k] {q : k} : SmallQuantumRel n k q (FreeAlgebra.ι k 0 ^ n) 1
• E_pow_n {n : ℕ} {k : Type u_2} [Field k] {q : k} : SmallQuantumRel n k q (FreeAlgebra.ι k 1 ^ n) 0
• F_pow_n {n : ℕ} {k : Type u_2} [Field k] {q : k} : SmallQuantumRel n k q (FreeAlgebra.ι k 2 ^ n) 0
• KE_comm {n : ℕ} {k : Type u_2} [Field k] {q : k} : SmallQuantumRel n k q (FreeAlgebra.ι k 0 * FreeAlgebra.ι k 1) (q ^ 2 • (FreeAlgebra.ι k 1 * FreeAlgebra.ι k 0))
• KF_comm {n : ℕ} {k : Type u_2} [Field k] {q : k} : SmallQuantumRel n k q (FreeAlgebra.ι k 0 * FreeAlgebra.ι k 2) ((q ^ 2)⁻¹ • (FreeAlgebra.ι k 2 * FreeAlgebra.ι k 0))
• EF_comm {n : ℕ} {k : Type u_2} [Field k] {q : k} : SmallQuantumRel n k q (FreeAlgebra.ι k 1 * FreeAlgebra.ι k 2 - FreeAlgebra.ι k 2 * FreeAlgebra.ι k 1) ((q - q⁻¹)⁻¹ • (FreeAlgebra.ι k 0 - FreeAlgebra.ι k 0 ^ (n - 1)))

@[reducible, inline]

abbrev SmallQuantumSl2Alg (n : ℕ) (k : Type u_2) [Field k] (q : k) : Type u_2

The small quantum sl_2 algebra: the quotient of the free k-algebra on three generators by the small quantum relations SmallQuantumRel n k q.

@[reducible, inline]

noncomputable abbrev SmallQuantumSl2Alg.π (n : ℕ) (k : Type u_2) [Field k] (q : k) : FreeAlgebra k (Fin 3) →ₐ[k] SmallQuantumSl2Alg n k q

The canonical algebra projection from the free algebra to the small quantum algebra.

noncomputable def SmallQuantumSl2Alg.K (n : ℕ) (k : Type u_2) [Field k] (q : k) : SmallQuantumSl2Alg n k q

The generator K of the small quantum group u_q(sl_2).

noncomputable def SmallQuantumSl2Alg.E (n : ℕ) (k : Type u_2) [Field k] (q : k) : SmallQuantumSl2Alg n k q

The generator E of the small quantum group u_q(sl_2).

noncomputable def SmallQuantumSl2Alg.F (n : ℕ) (k : Type u_2) [Field k] (q : k) : SmallQuantumSl2Alg n k q

The generator F of the small quantum group u_q(sl_2).

noncomputable def SmallQuantumSl2Alg.Kinv (n : ℕ) (k : Type u_2) [Field k] (q : k) : SmallQuantumSl2Alg n k q

The inverse K⁻¹ of K, realized as K^{n-1} (using K^n = 1).

theorem SmallQuantumSl2Alg.K_pow_n_eq (n : ℕ) (k : Type u_2) [Field k] (q : k) : K n k q ^ n = 1

The defining relation K^n = 1 in u_q(sl_2).

theorem SmallQuantumSl2Alg.E_pow_n_eq (n : ℕ) (k : Type u_2) [Field k] (q : k) : E n k q ^ n = 0

The nilpotency relation E^n = 0 in u_q(sl_2).

theorem SmallQuantumSl2Alg.F_pow_n_eq (n : ℕ) (k : Type u_2) [Field k] (q : k) : F n k q ^ n = 0

The nilpotency relation F^n = 0 in u_q(sl_2).

theorem SmallQuantumSl2Alg.K_mul_E_eq (n : ℕ) (k : Type u_2) [Field k] (q : k) : K n k q * E n k q = q ^ 2 • (E n k q * K n k q)

The commutation relation K E = q^2 (E K) in u_q(sl_2).

theorem SmallQuantumSl2Alg.K_mul_F_eq (n : ℕ) (k : Type u_2) [Field k] (q : k) : K n k q * F n k q = (q ^ 2)⁻¹ • (F n k q * K n k q)

The commutation relation K F = q^{-2} (F K) in u_q(sl_2).

theorem SmallQuantumSl2Alg.E_mul_F_comm (n : ℕ) (k : Type u_2) [Field k] (q : k) : E n k q * F n k q - F n k q * E n k q = (q - q⁻¹)⁻¹ • (K n k q - K n k q ^ (n - 1))

The commutator relation [E, F] = (K - K^{-1})/(q - q^{-1}) in u_q(sl_2), written using K^{n-1} as the explicit inverse of K.

theorem SmallQuantumSl2Alg.K_mul_Kinv (n : ℕ) (k : Type u_2) [Field k] (q : k) (hn : 1 ≤ n) : K n k q * Kinv n k q = 1

K · K^{-1} = 1 (right inverse property) when 1 ≤ n.

theorem SmallQuantumSl2Alg.Kinv_mul_K (n : ℕ) (k : Type u_2) [Field k] (q : k) (hn : 1 ≤ n) : Kinv n k q * K n k q = 1

K^{-1} · K = 1 (left inverse property) when 1 ≤ n.

noncomputable def SmallQuantumSl2Alg.lift (n : ℕ) (k : Type u_2) [Field k] (q : k) {A : Type u_3} [Ring A] [Algebra k A] (K' E' F' : A) (hK : K' ^ n = 1) (hE : E' ^ n = 0) (hF : F' ^ n = 0) (hKE : K' * E' = q ^ 2 • (E' * K')) (hKF : K' * F' = (q ^ 2)⁻¹ • (F' * K')) (hEF : E' * F' - F' * E' = (q - q⁻¹)⁻¹ • (K' - K' ^ (n - 1))) : SmallQuantumSl2Alg n k q →ₐ[k] A

Universal property of SmallQuantumSl2Alg: any choice of images K', E', F' in a k-algebra A satisfying the small quantum relations extends uniquely to a k-algebra homomorphism from SmallQuantumSl2Alg n k q.

class SmallQuantumSl2HopfData (n : ℕ) (k : Type u_3) [Field k] (q : k) : Type u_3

A bundle of data witnessing that SmallQuantumSl2Alg n k q carries a bialgebra/Hopf-algebra structure with prescribed values of the comultiplication, counit, and antipode on the generators K, E, F, together with the coherence axioms.

• comulHom : SmallQuantumSl2Alg n k q →ₐ[k] TensorProduct k (SmallQuantumSl2Alg n k q) (SmallQuantumSl2Alg n k q)
• counitHom : SmallQuantumSl2Alg n k q →ₐ[k] k
• antipodeLin : SmallQuantumSl2Alg n k q →ₗ[k] SmallQuantumSl2Alg n k q
• comulHom_K : comulHom (SmallQuantumSl2Alg.K n k q) = SmallQuantumSl2Alg.K n k q ⊗ₜ[k] SmallQuantumSl2Alg.K n k q
• comulHom_E : comulHom (SmallQuantumSl2Alg.E n k q) = SmallQuantumSl2Alg.E n k q ⊗ₜ[k] SmallQuantumSl2Alg.K n k q + 1 ⊗ₜ[k] SmallQuantumSl2Alg.E n k q
• comulHom_F : comulHom (SmallQuantumSl2Alg.F n k q) = SmallQuantumSl2Alg.F n k q ⊗ₜ[k] 1 + SmallQuantumSl2Alg.Kinv n k q ⊗ₜ[k] SmallQuantumSl2Alg.F n k q
• counitHom_K : counitHom (SmallQuantumSl2Alg.K n k q) = 1
• counitHom_E : counitHom (SmallQuantumSl2Alg.E n k q) = 0
• counitHom_F : counitHom (SmallQuantumSl2Alg.F n k q) = 0
• antipodeLin_K : antipodeLin (SmallQuantumSl2Alg.K n k q) = SmallQuantumSl2Alg.Kinv n k q
• antipodeLin_E : antipodeLin (SmallQuantumSl2Alg.E n k q) = -(SmallQuantumSl2Alg.E n k q * SmallQuantumSl2Alg.Kinv n k q)
• antipodeLin_F : antipodeLin (SmallQuantumSl2Alg.F n k q) = -(SmallQuantumSl2Alg.K n k q * SmallQuantumSl2Alg.F n k q)
• coassoc_axiom : (↑(Algebra.TensorProduct.assoc k k k (SmallQuantumSl2Alg n k q) (SmallQuantumSl2Alg n k q) (SmallQuantumSl2Alg n k q))).comp ((Algebra.TensorProduct.map comulHom (AlgHom.id k (SmallQuantumSl2Alg n k q))).comp comulHom) = (Algebra.TensorProduct.map (AlgHom.id k (SmallQuantumSl2Alg n k q)) comulHom).comp comulHom
• rTensor_counit_axiom : (Algebra.TensorProduct.map counitHom (AlgHom.id k (SmallQuantumSl2Alg n k q))).comp comulHom = ↑(Algebra.TensorProduct.lid k (SmallQuantumSl2Alg n k q)).symm
• lTensor_counit_axiom : (Algebra.TensorProduct.map (AlgHom.id k (SmallQuantumSl2Alg n k q)) counitHom).comp comulHom = ↑(Algebra.TensorProduct.rid k k (SmallQuantumSl2Alg n k q)).symm
• mul_antipode_rTensor_axiom : LinearMap.mul' k (SmallQuantumSl2Alg n k q) ∘ₗ LinearMap.rTensor (SmallQuantumSl2Alg n k q) antipodeLin ∘ₗ comulHom.toLinearMap = Algebra.linearMap k (SmallQuantumSl2Alg n k q) ∘ₗ counitHom.toLinearMap
• mul_antipode_lTensor_axiom : LinearMap.mul' k (SmallQuantumSl2Alg n k q) ∘ₗ LinearMap.lTensor (SmallQuantumSl2Alg n k q) antipodeLin ∘ₗ comulHom.toLinearMap = Algebra.linearMap k (SmallQuantumSl2Alg n k q) ∘ₗ counitHom.toLinearMap

@[implicit_reducible]

noncomputable instance SmallQuantumSl2Alg.instBialgebra {n : ℕ} {k : Type u_3} [Field k] {q : k} [hd : SmallQuantumSl2HopfData n k q] : Bialgebra k (SmallQuantumSl2Alg n k q)

Given SmallQuantumSl2HopfData, the small quantum algebra becomes a k-bialgebra.

@[implicit_reducible]

noncomputable instance SmallQuantumSl2Alg.instHopfAlgebra {n : ℕ} {k : Type u_3} [Field k] {q : k} [hd : SmallQuantumSl2HopfData n k q] : HopfAlgebra k (SmallQuantumSl2Alg n k q)

Given SmallQuantumSl2HopfData, the small quantum algebra becomes a k-Hopf algebra.

theorem SmallQuantumSl2Alg.comul_eq {n : ℕ} {k : Type u_3} [Field k] {q : k} [hd : SmallQuantumSl2HopfData n k q] (x : SmallQuantumSl2Alg n k q) : CoalgebraStruct.comul x = SmallQuantumSl2HopfData.comulHom x

The bialgebra comul agrees with the comultiplication supplied in hd.

theorem SmallQuantumSl2Alg.counit_eq {n : ℕ} {k : Type u_3} [Field k] {q : k} [hd : SmallQuantumSl2HopfData n k q] (x : SmallQuantumSl2Alg n k q) : CoalgebraStruct.counit x = SmallQuantumSl2HopfData.counitHom x

The bialgebra counit agrees with the counit supplied in hd.

theorem SmallQuantumSl2Alg.antipode_eq {n : ℕ} {k : Type u_3} [Field k] {q : k} [hd : SmallQuantumSl2HopfData n k q] (x : SmallQuantumSl2Alg n k q) : (HopfAlgebraStruct.antipode k) x = SmallQuantumSl2HopfData.antipodeLin x

The Hopf algebra antipode agrees with the antipode supplied in hd.

@[implicit_reducible]

noncomputable instance SmallQuantumSl2Alg.instQuantumSl2 {n : ℕ} {k : Type u_3} [Field k] {q : k} [hd : SmallQuantumSl2HopfData n k q] (hn : 2 ≤ n) (hq : q ≠ 0) (hq2 : q ^ 2 ≠ 1) : QuantumSl2 k (SmallQuantumSl2Alg n k q)

Given Hopf data and n ≥ 2, q ≠ 0, q^2 ≠ 1, the small quantum algebra SmallQuantumSl2Alg n k q is a QuantumSl2.