LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

The full divided-power integral form is a Hopf form

Statement

Assume the Axiom of Choice inherited from the integral triangular-decomposition supplier. The full form $U_{A}$ of The Lusztig divided-power integral form $U_{A}$ , including every $T_{i, c, t}$ , is stable under the library coproduct, counit, antipode and inverse antipode. Consequently every scalar specialization, including $U_{ζ}^{L}$ , is a Hopf algebra with bijective antipode. In the following formulas $a, b, r, t \geq 0$ , $c \in Z$ , and $q = q_{i}$ , $K = K_{i}$ when the color is suppressed:

$Δ E_{i}^{(r)} = \sum_{a + b = r} q_{i}^{a b} E_{i}^{(a)} \otimes K_{i}^{- a} E_{i}^{(b)}, Δ F_{i}^{(r)} = \sum_{a + b = r} q_{i}^{- a b} F_{i}^{(a)} K_{i}^{b} \otimes F_{i}^{(b)} .$

$Δ T_{i, c, t} = \sum_{a + b = t} q_{i}^{- b c} T_{i, c, a} K_{i}^{- b} \otimes K_{i}^{a} T_{i, 0, b} .$

$S (E_{i}^{(r)}) = (- 1)^{r} q_{i}^{r (r - 1)} E_{i}^{(r)} K_{i}^{r}, S (F_{i}^{(r)}) = (- 1)^{r} q_{i}^{- r (r - 1)} K_{i}^{- r} F_{i}^{(r)} .$

$S (T_{i, c, t}) = (- 1)^{t} T_{i, t - c - 1, t}, ε (T_{i, c, t}) = {[\begin{array}{c} c \\ t \end{array}]}_{q_{i}} .$

The generalized Gaussian for integral $c$ denotes its Laurent-polynomial value; for $c = - b < 0$ it equals $(- 1)^{t} {[\begin{array}{c} b + t - 1 \\ t \end{array}]}_{q_{i}}$ .

Facts & Assumptions

Given: The full integral form, its generic embedding and the library generic Hopf structure.

[F1]

The generic Hopf formulas are $Δ E_{i} = E_{i} \otimes K_{i}^{- 1} + 1 \otimes E_{i}$ , $Δ F_{i} = F_{i} \otimes 1 + K_{i} \otimes F_{i}$ , $S (E_{i}) = - E_{i} K_{i}$ , $S (F_{i}) = - K_{i}^{- 1} F_{i}$ , $Δ K_{h} = K_{h} \otimes K_{h}$ and $S (K_{h}) = K_{- h}$ (The Drinfeld–Jimbo formulas define a Hopf algebra).

[F2]

The integral form is free and its tensor powers inject into their fraction-field extensions (Integral triangular decomposition and freeness of the Lusztig form). This supplier uses The Axiom of Choice; that is the sole inherited Choice use here.

[F3]

Quantum Pascal recurrence gives Laurent-polynomial integral Gaussian coefficients (The quantum Pascal recurrences, the Gauss product formula and Gaussian integrality).

Proof

1.1F1F3algebra

Expanding a $q$ -commuting binomial by induction gives the two displayed divided coproducts: the induction recurrence is the quantum Pascal recurrence in [F3], and the toral orders shown in the statement are retained. Directly applying the anti-map in [F1], $(E_{i} K_{i})^{r} = q_{i}^{r (r - 1)} E_{i}^{r} K_{i}^{r}$ and $(K_{i}^{- 1} F_{i})^{r} = q_{i}^{- r (r - 1)} K_{i}^{- r} F_{i}^{r}$ give the displayed antipodes, before specialization. Thus these maps preserve every divided generator and every toral group element.

1.2F3algebra

Here is the toral calculation, including arbitrary shifts. For nonnegative integers $m, n$ the coefficient identity obtained by splitting the product $\prod_{j = 0}^{m + n - 1} (1 + q^{m + n - 1 - 2 j} z)$ into blocks of lengths $m, n$ is ${[\begin{array}{c} m + n \\ t \end{array}]}_{q} = \sum_{a + b = t} q^{- b m + a n} {[\begin{array}{c} m \\ a \end{array}]}_{q} {[\begin{array}{c} n \\ b \end{array}]}_{q}$ . Regard this as an identity of Laurent polynomials in independent $X, Y$ over $Q (q)$ , replacing $q^{m}, q^{n}$ by $X, Y$ . It holds for every sufficiently large pair $m, n$ , and a Laurent polynomial vanishing on all pairs $(q^{m}, q^{n})$ is zero: fixing one variable gives infinitely many distinct roots, then applying this again to the coefficients proves the assertion. Substituting $X = q^{c} K \otimes 1$ and $Y = 1 \otimes K$ yields exactly the displayed $Δ T_{i, c, t}$ . Its right side belongs to $U_{A} \otimes_{A} U_{A}$ with no denominator.

1.3F1F3algebra

Substituting $K \mapsto K^{- 1}$ into the product defining $T_{i, c, t}$ , negating each numerator and reversing the $t$ factors gives $S (T_{i, c, t}) = (- 1)^{t} T_{i, t - c - 1, t}$ . Substituting $K = 1$ gives its stated counit; negative upper indices have the polynomial expression stated above, by reversing and negating the numerator factors. Hence the counit has values in $A$ and the antipode preserves all toral binomials.

2.1step 1.1step 1.2step 1.3F2algebra∎

By steps 1.1–1.3 all generic structure maps restrict to the integral form. Since its tensor powers inject into the generic tensor powers by [F2], the generic coassociativity, counit and antipode identities hold as integral identities. Moreover $S^{2} (E_{i}^{(r)}) = q_{i}^{- 2 r} E_{i}^{(r)}$ , $S^{2} (F_{i}^{(r)}) = q_{i}^{2 r} F_{i}^{(r)}$ and $S^{2}$ fixes the torus and all its binomials. These formulas and their inverses preserve the integral generators, so $S^{2}$ and hence $S$ are bijective on $U_{A}$ . Base change preserves every identity and the inverse antipode. This proves all assertions without division by any vanishing root factorial.

Depends on

Used by

Dependency tree · two levels

30 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

George Lusztig, Introduction to Quantum Groups (standard reference, not scraped)