ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Coproduct, antipode and $q$ -binomial expansion in $U_{q} ({s l}_{2})$

Example

In the rank-one Drinfeld–Jimbo algebra $U_{q} ({s l}_{2})$ (the Cartan datum $I = {1}$ , $A = (2)$ , $d_{1} = 1$ , $P^{\lor} = Z h_{1}$ , $P = Z α_{1}$ , $⟨ α_{1}, h_{1} ⟩ = 2$ , so $q_{1} = q$ and $K = K_{h_{1}}$ ) with generators $E, F, K^{\pm 1}$ and relations $K E K^{- 1} = q^{2} E$ , $K F K^{- 1} = q^{- 2} F$ , $E F - F E = (K - K^{- 1}) / (q - q^{- 1})$ :

(i) the coproduct, counit and antipode of The Drinfeld–Jimbo formulas define a Hopf algebra are $Δ (E) = E \otimes K^{- 1} + 1 \otimes E$ , $Δ (F) = F \otimes 1 + K \otimes F$ , $Δ (K^{\pm 1}) = K^{\pm 1} \otimes K^{\pm 1}$ , $ε (E) = ε (F) = 0$ , $ε (K) = 1$ , $S (E) = - E K$ , $S (F) = - K^{- 1} F$ , $S (K) = K^{- 1}$ ;

(ii) for every $n \geq 0$ the $q$ -binomial expansion holds: $Δ (E^{n}) = \sum_{r = 0}^{n} q^{r (n - r)} {(\binom{n}{r})}_{q} E^{r} \otimes K^{- r} E^{n - r}$ ; and both antipode identities hold on the generators: $m (S \otimes id) Δ (E) = - E + E = 0$ and $m (id \otimes S) Δ (E) = E K - E K = 0$ , with the same two computations for $F$ and the trivial $K^{\pm 1}$ checks;

(iii) $S^{2} (E) = q^{- 2} E$ and $S^{2} (F) = q^{2} F$ ; since $E \neq 0$ and $K \neq 1$ in $U_{q} ({s l}_{2})$ -- proved below by the oscillator model -- the antipode is not an involution;

(iv) the coproduct is not cocommutative: $Δ (E) - τ Δ (E) = E \otimes (K^{- 1} - 1) + (1 - K^{- 1}) \otimes E \neq 0$ , where $τ$ is the tensor flip.

All four computations use no choice principle. The nonvanishing statements in (iii) and (iv) are proved by an explicit representation of $U_{q} ({s l}_{2})$ on the Laurent polynomial ring, independently of triangular decomposition.

Facts & Assumptions

Given: The rank-one Drinfeld–Jimbo algebra, with generators $E, F, K^{\pm 1}$ and relations as displayed.

[F1]

The Drinfeld–Jimbo algebra of a symmetrizable Cartan datum has the displayed coproduct, counit and antipode, its antipode is unique and $S^{2} (E_{i}) = q_{i}^{- 2} E_{i}$ , $S^{2} (F_{i}) = q_{i}^{2} F_{i}$ , and any assignment of generators satisfying the defining relations extends to an algebra homomorphism (The Drinfeld–Jimbo formulas define a Hopf algebra, The Drinfeld-Jimbo quantized enveloping algebra by generators and relations).

[F2]

The rank-one datum with $P^{\lor} = Z h_{1}$ , $P = Z α_{1}$ and $⟨ α_{1}, h_{1} ⟩ = 2$ has exactly the relations displayed above (The Drinfeld-Jimbo quantized enveloping algebra by generators and relations).

[F3]

If $y x = t x y$ in a unital algebra, then $(x + y)^{N} = \sum_{r} B_{N, r} (t) x^{r} y^{N - r}$ with $B_{N, r} (t)$ the asymmetric Gaussian coefficient; for $t = q_{i}^{2}$ this reads $(x + y)^{N} = \sum_{r} q_{i}^{r (N - r)} {(\binom{N}{r})}_{i} x^{r} y^{N - r}$ (The quantum binomial expansion for $q$ -commuting elements).

[F4]

In $Q (q)$ one has $q \neq 0$ , $q \neq 1$ , $q^{2} \neq 1$ , $q^{2 n} \neq 1$ for $n \neq 0$ , and $(K - K^{- 1}) / (q - q^{- 1})$ is defined (Quantum integers, factorials, Gaussian binomials and divided powers at $q_{i}$ , The Drinfeld-Jimbo quantized enveloping algebra by generators and relations).

[F5]

$M : = Q (q) [X^{\pm 1}]$ is explicitly the space of finite sums $\sum_{n \in Z} c_{n} X^{n}$ , $c_{n} \in Q (q)$ , with coefficientwise addition and product $X^{m} X^{n} = X^{m + n}$ . These finite convolution operations are associative and have unit $X^{0}$ by addition of integer exponents; the formal monomials form a basis by the coefficient-function definition. This is the same finite Laurent construction as The Laurent polynomial ring as the principal localisation of Z[t] at t, here with coefficient field $Q (q)$ ; the $Q (q)$ -linear endomorphisms of $M$ form a unital algebra under composition, and linear functionals on an algebra form a vector space (The Laurent polynomial ring as the principal localisation of Z[t] at t, The endomorphism ring ${End}_{R} (M)$ under addition and composition, Linear functionals and the algebraic dual $V^{*} = L (V, F)$ ).

[F6]

No choice principle is used: the model of step 1.3 is defined by an explicit formula, and every sum below is finite.

Verification

technique · Instantiate the Hopf formulas and expand $\Delta(E^n)$ with the $q$-binomial lemma; then build an explicit oscillator representation of $U_q(\mathfrak{sl}_2)$ on the Laurent polynomial ring and use one of its matrix functionals to separate the elements that occur

1.1F1F2algebra

Part (i). By [F2], $U_{q} ({s l}_{2})$ is the Drinfeld–Jimbo algebra of the rank-one datum, so [F1] gives $Δ (E) = E \otimes K^{- 1} + 1 \otimes E$ , $Δ (F) = F \otimes 1 + K \otimes F$ , $Δ (K^{\pm 1}) = K^{\pm 1} \otimes K^{\pm 1}$ , $ε (E) = ε (F) = 0$ , $ε (K) = 1$ . The antipode is the unique convolution inverse of the identity; on $E$ it is $S (E) = - E K$ because $- E K \cdot K^{- 1} + E = 0$ and $E \cdot K - E K = 0$ compute the two convolution equations of [F1] on $E$ (using $S (K^{- 1}) = K$ ), and on $F$ it is $S (F) = - K^{- 1} F$ by the mirrored computation.

1.2F1F3algebra

Part (ii), first assertion. Put $x : = E \otimes K^{- 1}$ and $y : = 1 \otimes E$ in $U_{q} ({s l}_{2}) \otimes U_{q} ({s l}_{2})$ . Then $y x = (1 \otimes E) (E \otimes K^{- 1}) = E \otimes E K^{- 1} = E \otimes q^{2} K^{- 1} E = q^{2} x y$ , using $E K^{- 1} = q^{2} K^{- 1} E$ , which follows from $K E K^{- 1} = q^{2} E$ by multiplying on the left by $K^{- 1}$ and on the right by $K$ . Since $Δ$ is an algebra homomorphism, $Δ (E^{n}) = Δ (E)^{n} = (x + y)^{n}$ , and [F3] with $q_{1} = q$ gives $Δ (E^{n}) = \sum_{r = 0}^{n} q^{r (n - r)} {(\binom{n}{r})}_{q} E^{r} \otimes K^{- r} E^{n - r}$ , because $x^{r} = E^{r} \otimes K^{- r}$ and $y^{n - r} = 1 \otimes E^{n - r}$ .

1.3F1F4F5construct

The oscillator model. Let $M = Q (q) [X^{\pm 1}]$ and define $Q (q)$ -linear endomorphisms by $\hat{E} (f) : = X f$ , $(\hat{K} f) (X) : = f (q^{2} X)$ , and $\hat{F} (X^{n}) : = λ_{n} X^{n - 1}$ with $λ_{n} : = α q^{2 n} + β q^{- 2 n}$ , $α : = 1 / [(q - q^{- 1}) (1 - q^{2})]$ , $β : = - 1 / [(q - q^{- 1}) (1 - q^{- 2})]$ ; both scalars are nonzero and defined by [F4], and $\hat{K}$ is invertible with ${\hat{K}}^{- 1} (f) (X) = f (q^{- 2} X)$ . Then $\hat{E} \hat{F} - \hat{F} \hat{E}$ acts on $X^{n}$ by the scalar $(q^{2 n} - q^{- 2 n}) / (q - q^{- 1})$ for every $n \in Z$ : indeed $(\hat{E} \hat{F} - \hat{F} \hat{E}) (X^{n}) = λ_{n} X^{n} - λ_{n + 1} X^{n} = (λ_{n} - λ_{n + 1}) X^{n}$ and $λ_{n} - λ_{n + 1} = α q^{2 n} (1 - q^{2}) + β q^{- 2 n} (1 - q^{- 2}) = (q^{2 n} - q^{- 2 n}) / (q - q^{- 1})$ , while $(\hat{K} - {\hat{K}}^{- 1}) / (q - q^{- 1})$ acts on $X^{n}$ by the same scalar; moreover $\hat{K} \hat{E} {\hat{K}}^{- 1} = q^{2} \hat{E}$ and $\hat{K} \hat{F} {\hat{K}}^{- 1} = q^{- 2} \hat{F}$ by direct evaluation on the basis. Hence by the universal property in [F1] there is a unital algebra homomorphism $ρ : U_{q} ({s l}_{2}) \to End (M)$ with $ρ (E) = \hat{E}$ , $ρ (F) = \hat{F}$ , $ρ (K) = \hat{K}$ .

2.1step 1.1F1algebra

Part (ii), antipode identities. Using 1.1, $m (S \otimes id) Δ (E) = S (E) K^{- 1} + E = - E K \cdot K^{- 1} + E = 0$ and $m (id \otimes S) Δ (E) = E \cdot S (K^{- 1}) + S (E) = E K - E K = 0$ , since $S (K^{- 1}) = K$ . The same two computations with $K$ replaced by $K^{- 1}$ and $E$ by $F$ give $m (S \otimes id) Δ (F) = S (F) + S (K) F = - K^{- 1} F + K^{- 1} F = 0$ and $m (id \otimes S) Δ (F) = F + K \cdot S (F) = F - F = 0$ ; for $K^{\pm 1}$ both sides are $K^{\pm 1} K^{\mp 1} = 1$ , and for the unit both are $1$ .

2.2step 1.1F1algebra

Part (iii), first assertion. $S^{2} (E) = S (- E K) = - S (K) S (E) = - K^{- 1} (- E K) = K^{- 1} E K = q^{- 2} E$ and $S^{2} (F) = S (- K^{- 1} F) = - S (F) S (K^{- 1}) = - (- K^{- 1} F) K = K^{- 1} F K = q^{2} F$ , using anti-multiplicativity of $S$ from [F1].

3.1F4F5step 2.2step 1.3algebra

Nonvanishing and separation. Since $\hat{E} (X^{0}) = X^{1} \neq 0$ and $\hat{K} \neq id$ (as $\hat{K} (X^{1}) = q^{2} X^{1} \neq X^{1}$ by [F4]), neither $E = 0$ nor $K = 1$ holds in $U_{q} ({s l}_{2})$ ; likewise $K^{- 1} \neq 1$ . Also $E \notin {span}_{Q (q)} {1, K^{- 1}}$ : if $E = a \cdot 1 + b K^{- 1}$ , applying $ρ$ gives $\hat{E} = a id + b {\hat{K}}^{- 1}$ , and evaluating on $X^{0}$ gives $X^{1} = (a + b) X^{0}$ , whose two sides have disjoint monomial supports, a contradiction. In particular $S^{2} (E) = q^{- 2} E \neq E$ , so $S^{2} \neq id$ , which completes (iii).

4.1step 1.1step 1.3step 3.1F5algebra∎

Part (iv). By 1.1, $Δ (E) - τ Δ (E) = E \otimes K^{- 1} + 1 \otimes E - K^{- 1} \otimes E - E \otimes 1 = E \otimes (K^{- 1} - 1) + (1 - K^{- 1}) \otimes E$ . Let $λ : U_{q} ({s l}_{2}) \to Q (q)$ be the linear functional $λ (g) : = [X^{1}] (ρ (g) (X^{0}))$ (coefficient extraction, [F5]). Then $λ (E) = 1$ , $λ (1) = 0$ and $λ (K^{- 1}) = 0$ by 1.3, so applying $id \otimes λ$ to the displayed element gives $E \cdot λ (K^{- 1} - 1) + (1 - K^{- 1}) \cdot λ (E) = 1 - K^{- 1} \neq 0$ by 3.1; hence $Δ (E) \neq τ Δ (E)$ and the coproduct is not cocommutative.

Remarks

Every displayed computation is finite and uses only [F1]–[F5]; the model of step 1.3 is given by explicit formulas and is the only place where an auxiliary construction is made, and it is choice-free by [F6].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

36 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Richard Borcherds, Mark Haiman, Theo Johnson-Freyd, Nicolai Reshetikhin and Vera Serganova, Berkeley Lectures on Lie Groups and Quantum Groups (book-length lecture notes, last updated 18 January 2024) (standard reference, not scraped)
Pavel Etingof and Mykola Semenyakin, A Brief Introduction to Quantum Groups (lecture notes, CMSA Math Science Literature Lecture Series, 2020) (standard reference, not scraped)

Coproduct, antipode and qq-binomial expansion in Uq(sl2)Uq​(sl2​)