class SmallQuantumSl2Instance.QuantumSl2Hypotheses (n : ℕ) (k : Type u_2) [Field k] (q : k) : Prop

Standing hypotheses needed to construct the Hopf algebra structure on the small quantum group u_q(sl_2): n ≥ 2, q is a primitive n-th root of unity, and so is q^2.

• hn : 2 ≤ n
• hq_prim : IsPrimitiveRoot q n
• hq2_prim : IsPrimitiveRoot (q ^ 2) n

theorem SmallQuantumSl2Instance.q_ne_zero (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] : q ≠ 0

A primitive n-th root of unity (n ≥ 2) is nonzero.

theorem SmallQuantumSl2Instance.q2_pow_n (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] : (q ^ 2) ^ n = 1

The relation (q^2)^n = 1, from primitivity of q^2.

theorem SmallQuantumSl2Instance.one_lt_n (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] : 1 < n

From n ≥ 2, 1 < n.

theorem SmallQuantumSl2Instance.one_le_n (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] : 1 ≤ n

From n ≥ 2, 1 ≤ n.

theorem SmallQuantumSl2Instance.n_ne_zero (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] : n ≠ 0

From n ≥ 2, n ≠ 0.

noncomputable def SmallQuantumSl2Instance.DeltaK (n : ℕ) (k : Type u_1) [Field k] (q : k) : TensorProduct k (SmallQuantumSl2Alg n k q) (SmallQuantumSl2Alg n k q)

The candidate comultiplication of K: K ⊗ K.

noncomputable def SmallQuantumSl2Instance.DeltaE (n : ℕ) (k : Type u_1) [Field k] (q : k) : TensorProduct k (SmallQuantumSl2Alg n k q) (SmallQuantumSl2Alg n k q)

The candidate comultiplication of E: E ⊗ K + 1 ⊗ E.

noncomputable def SmallQuantumSl2Instance.DeltaF (n : ℕ) (k : Type u_1) [Field k] (q : k) : TensorProduct k (SmallQuantumSl2Alg n k q) (SmallQuantumSl2Alg n k q)

The candidate comultiplication of F: F ⊗ 1 + K^{-1} ⊗ F.

theorem SmallQuantumSl2Instance.DeltaK_pow_n (n : ℕ) (k : Type u_1) [Field k] (q : k) : DeltaK n k q ^ n = 1

Verification: (K ⊗ K)^n = 1 follows from K^n = 1.

theorem SmallQuantumSl2Instance.DeltaE_pow_n (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] : DeltaE n k q ^ n = 0

Verification: (DeltaE)^n = 0 follows from E^n = 0 and the q-binomial identity.

theorem SmallQuantumSl2Instance.K_pow_mul_F (n : ℕ) (k : Type u_1) [Field k] (q : k) (j : ℕ) : SmallQuantumSl2Alg.K n k q ^ j * SmallQuantumSl2Alg.F n k q = (q ^ 2)⁻¹ ^ j • (SmallQuantumSl2Alg.F n k q * SmallQuantumSl2Alg.K n k q ^ j)

Iterated commutation: K^j · F = q^{-2j} · (F · K^j).

theorem SmallQuantumSl2Instance.inv_q2_pow_pred (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] : (q ^ 2)⁻¹ ^ (n - 1) = q ^ 2

Identity at a root of unity: ((q^2)⁻¹)^{n-1} = q^2.

theorem SmallQuantumSl2Instance.Kinv_mul_F (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] : SmallQuantumSl2Alg.Kinv n k q * SmallQuantumSl2Alg.F n k q = q ^ 2 • (SmallQuantumSl2Alg.F n k q * SmallQuantumSl2Alg.Kinv n k q)

K^{-1} · F = q^2 · (F · K^{-1}).

theorem SmallQuantumSl2Instance.DeltaF_pow_n (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] : DeltaF n k q ^ n = 0

Verification: (DeltaF)^n = 0 follows from F^n = 0 and the q-binomial identity.

theorem SmallQuantumSl2Instance.DeltaKE_comm (n : ℕ) (k : Type u_1) [Field k] (q : k) : DeltaK n k q * DeltaE n k q = q ^ 2 • (DeltaE n k q * DeltaK n k q)

Verification: DeltaK · DeltaE = q^2 · (DeltaE · DeltaK).

theorem SmallQuantumSl2Instance.DeltaKF_comm (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] : DeltaK n k q * DeltaF n k q = (q ^ 2)⁻¹ • (DeltaF n k q * DeltaK n k q)

Verification: DeltaK · DeltaF = q^{-2} · (DeltaF · DeltaK).

theorem SmallQuantumSl2Instance.K_pow_mul_E (n : ℕ) (k : Type u_1) [Field k] (q : k) (j : ℕ) : SmallQuantumSl2Alg.K n k q ^ j * SmallQuantumSl2Alg.E n k q = (q ^ 2) ^ j • (SmallQuantumSl2Alg.E n k q * SmallQuantumSl2Alg.K n k q ^ j)

Iterated commutation: K^j · E = q^{2j} · (E · K^j).

theorem SmallQuantumSl2Instance.E_mul_K_pow (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] (j : ℕ) : SmallQuantumSl2Alg.E n k q * SmallQuantumSl2Alg.K n k q ^ j = (q ^ 2)⁻¹ ^ j • (SmallQuantumSl2Alg.K n k q ^ j * SmallQuantumSl2Alg.E n k q)

Iterated commutation: E · K^j = q^{-2j} · (K^j · E).

theorem SmallQuantumSl2Instance.E_mul_Kinv (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] : SmallQuantumSl2Alg.E n k q * SmallQuantumSl2Alg.Kinv n k q = q ^ 2 • (SmallQuantumSl2Alg.Kinv n k q * SmallQuantumSl2Alg.E n k q)

Commutation: E · K^{-1} = q^2 · (K^{-1} · E).

theorem SmallQuantumSl2Instance.cross_term_eq (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] : (SmallQuantumSl2Alg.E n k q * SmallQuantumSl2Alg.Kinv n k q) ⊗ₜ[k] (SmallQuantumSl2Alg.K n k q * SmallQuantumSl2Alg.F n k q) = (SmallQuantumSl2Alg.Kinv n k q * SmallQuantumSl2Alg.E n k q) ⊗ₜ[k] (SmallQuantumSl2Alg.F n k q * SmallQuantumSl2Alg.K n k q)

Cross term identity used in the verification of the comultiplication EF relation.

theorem SmallQuantumSl2Instance.DeltaK_pow_pred (n : ℕ) (k : Type u_1) [Field k] (q : k) : DeltaK n k q ^ (n - 1) = SmallQuantumSl2Alg.Kinv n k q ⊗ₜ[k] SmallQuantumSl2Alg.Kinv n k q

DeltaK^{n-1} = K^{-1} ⊗ K^{-1} (using K^n = 1).

theorem SmallQuantumSl2Instance.DeltaEF_comm (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] : DeltaE n k q * DeltaF n k q - DeltaF n k q * DeltaE n k q = (q - q⁻¹)⁻¹ • (DeltaK n k q - DeltaK n k q ^ (n - 1))

Verification of the EF commutator for the candidate comultiplications: [DeltaE, DeltaF] = (q - q^{-1})^{-1}(DeltaK - DeltaK^{n-1}).

noncomputable def SmallQuantumSl2Instance.comulHomAux (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] : SmallQuantumSl2Alg n k q →ₐ[k] TensorProduct k (SmallQuantumSl2Alg n k q) (SmallQuantumSl2Alg n k q)

The candidate comultiplication on SmallQuantumSl2Alg, obtained by lifting the prescribed values DeltaK, DeltaE, DeltaF through the universal property.

noncomputable def SmallQuantumSl2Instance.counitHomAux (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] : SmallQuantumSl2Alg n k q →ₐ[k] k

The candidate counit on SmallQuantumSl2Alg: K ↦ 1, E ↦ 0, F ↦ 0.

class SmallQuantumSl2Instance.QuantumSl2StructuralAxioms (n : ℕ) (k : Type u_2) [Field k] (q : k) [QuantumSl2Hypotheses n k q] : Prop

Auxiliary structural axioms packaging the existence of an antipode and the coassociativity / counitality / Hopf-algebra axioms for the candidate comulHomAux, counitHomAux on the small quantum group.

• antipode_exists : ∃ (S : SmallQuantumSl2Alg n k q →ₗ[k] SmallQuantumSl2Alg n k q), S (SmallQuantumSl2Alg.K n k q) = SmallQuantumSl2Alg.Kinv n k q ∧ S (SmallQuantumSl2Alg.E n k q) = -(SmallQuantumSl2Alg.E n k q * SmallQuantumSl2Alg.Kinv n k q) ∧ S (SmallQuantumSl2Alg.F n k q) = -(SmallQuantumSl2Alg.K n k q * SmallQuantumSl2Alg.F n k q)
• coassoc : (↑(Algebra.TensorProduct.assoc k k k (SmallQuantumSl2Alg n k q) (SmallQuantumSl2Alg n k q) (SmallQuantumSl2Alg n k q))).comp ((Algebra.TensorProduct.map (comulHomAux n k q) (AlgHom.id k (SmallQuantumSl2Alg n k q))).comp (comulHomAux n k q)) = (Algebra.TensorProduct.map (AlgHom.id k (SmallQuantumSl2Alg n k q)) (comulHomAux n k q)).comp (comulHomAux n k q)
• rTensor_counit : (Algebra.TensorProduct.map (counitHomAux n k q) (AlgHom.id k (SmallQuantumSl2Alg n k q))).comp (comulHomAux n k q) = ↑(Algebra.TensorProduct.lid k (SmallQuantumSl2Alg n k q)).symm
• lTensor_counit : (Algebra.TensorProduct.map (AlgHom.id k (SmallQuantumSl2Alg n k q)) (counitHomAux n k q)).comp (comulHomAux n k q) = ↑(Algebra.TensorProduct.rid k k (SmallQuantumSl2Alg n k q)).symm
• hopf_right (S : SmallQuantumSl2Alg n k q →ₗ[k] SmallQuantumSl2Alg n k q) : S (SmallQuantumSl2Alg.K n k q) = SmallQuantumSl2Alg.Kinv n k q → S (SmallQuantumSl2Alg.E n k q) = -(SmallQuantumSl2Alg.E n k q * SmallQuantumSl2Alg.Kinv n k q) → S (SmallQuantumSl2Alg.F n k q) = -(SmallQuantumSl2Alg.K n k q * SmallQuantumSl2Alg.F n k q) → LinearMap.mul' k (SmallQuantumSl2Alg n k q) ∘ₗ LinearMap.rTensor (SmallQuantumSl2Alg n k q) S ∘ₗ (comulHomAux n k q).toLinearMap = Algebra.linearMap k (SmallQuantumSl2Alg n k q) ∘ₗ (counitHomAux n k q).toLinearMap
• hopf_left (S : SmallQuantumSl2Alg n k q →ₗ[k] SmallQuantumSl2Alg n k q) : S (SmallQuantumSl2Alg.K n k q) = SmallQuantumSl2Alg.Kinv n k q → S (SmallQuantumSl2Alg.E n k q) = -(SmallQuantumSl2Alg.E n k q * SmallQuantumSl2Alg.Kinv n k q) → S (SmallQuantumSl2Alg.F n k q) = -(SmallQuantumSl2Alg.K n k q * SmallQuantumSl2Alg.F n k q) → LinearMap.mul' k (SmallQuantumSl2Alg n k q) ∘ₗ LinearMap.lTensor (SmallQuantumSl2Alg n k q) S ∘ₗ (comulHomAux n k q).toLinearMap = Algebra.linearMap k (SmallQuantumSl2Alg n k q) ∘ₗ (counitHomAux n k q).toLinearMap

noncomputable def SmallQuantumSl2Instance.antipodeLinAux (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] [QuantumSl2StructuralAxioms n k q] : SmallQuantumSl2Alg n k q →ₗ[k] SmallQuantumSl2Alg n k q

A linear antipode for the small quantum group, extracted from the structural axioms QuantumSl2StructuralAxioms.

theorem SmallQuantumSl2Instance.antipodeLinAux_K (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] [QuantumSl2StructuralAxioms n k q] : (antipodeLinAux n k q) (SmallQuantumSl2Alg.K n k q) = SmallQuantumSl2Alg.Kinv n k q

The antipode satisfies S(K) = K^{-1}.

theorem SmallQuantumSl2Instance.antipodeLinAux_E (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] [QuantumSl2StructuralAxioms n k q] : (antipodeLinAux n k q) (SmallQuantumSl2Alg.E n k q) = -(SmallQuantumSl2Alg.E n k q * SmallQuantumSl2Alg.Kinv n k q)

The antipode satisfies S(E) = -E · K^{-1}.

theorem SmallQuantumSl2Instance.antipodeLinAux_F (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] [QuantumSl2StructuralAxioms n k q] : (antipodeLinAux n k q) (SmallQuantumSl2Alg.F n k q) = -(SmallQuantumSl2Alg.K n k q * SmallQuantumSl2Alg.F n k q)

The antipode satisfies S(F) = -K · F.

theorem SmallQuantumSl2Instance.comulHomAux_K (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] : (comulHomAux n k q) (SmallQuantumSl2Alg.K n k q) = SmallQuantumSl2Alg.K n k q ⊗ₜ[k] SmallQuantumSl2Alg.K n k q

comulHomAux(K) = K ⊗ K.

theorem SmallQuantumSl2Instance.comulHomAux_E (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] : (comulHomAux n k q) (SmallQuantumSl2Alg.E n k q) = SmallQuantumSl2Alg.E n k q ⊗ₜ[k] SmallQuantumSl2Alg.K n k q + 1 ⊗ₜ[k] SmallQuantumSl2Alg.E n k q

comulHomAux(E) = E ⊗ K + 1 ⊗ E.

theorem SmallQuantumSl2Instance.comulHomAux_F (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] : (comulHomAux n k q) (SmallQuantumSl2Alg.F n k q) = SmallQuantumSl2Alg.F n k q ⊗ₜ[k] 1 + SmallQuantumSl2Alg.Kinv n k q ⊗ₜ[k] SmallQuantumSl2Alg.F n k q

comulHomAux(F) = F ⊗ 1 + K^{-1} ⊗ F.

theorem SmallQuantumSl2Instance.counitHomAux_K (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] : (counitHomAux n k q) (SmallQuantumSl2Alg.K n k q) = 1

counitHomAux(K) = 1.

theorem SmallQuantumSl2Instance.counitHomAux_E (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] : (counitHomAux n k q) (SmallQuantumSl2Alg.E n k q) = 0

counitHomAux(E) = 0.

theorem SmallQuantumSl2Instance.counitHomAux_F (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] : (counitHomAux n k q) (SmallQuantumSl2Alg.F n k q) = 0

counitHomAux(F) = 0.

@[implicit_reducible]

noncomputable instance SmallQuantumSl2Instance.instSmallQuantumSl2HopfData (n : ℕ) (k : Type u_1) [Field k] (q : k) [hyp : QuantumSl2Hypotheses n k q] [QuantumSl2StructuralAxioms n k q] : SmallQuantumSl2HopfData n k q

Assembles the candidate comultiplication, counit, and antipode together with the structural axioms into a SmallQuantumSl2HopfData instance.