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.

Higher divided quantum Serre relations from a skew derivation

Statement

For distinct simple indices $i, j$ , put $a = - a_{i j} \geq 0$ and $v = q_{i}$ . In the actual divided-power integral form, for $n, m \geq 0$ and $m > a n$ , $\sum_{r + s = m} (- 1)^{r} v^{r (a n - m + 1)} E_{i}^{(r)} E_{j}^{(n)} E_{i}^{(s)} = 0.$ The same identity holds with $E$ replaced by $F$ . Since it is an equality of integral elements, it survives every specialization of the integral form, even when its divided-power indices have vanishing quantum factorials after specialization. This assertion does not assume a presentation theorem for that integral form.

Facts & Assumptions

Given: The generic Drinfeld–Jimbo algebra and its actual integral subalgebra.

[F1]

The ordinary positive and negative quantum Serre relations are defining relations of The Drinfeld-Jimbo quantized enveloping algebra by generators and relations. The root grading of Positive, negative and toral quantum subalgebras and their root gradings gives $i$ -weight $⟨ h_{i}, β ⟩$ to degree $β$ .

[F2]

Divided powers are generic powers divided by their nonzero quantum factorials, and generate actual integral subalgebras (The Lusztig divided-power integral form $U_{A}$ ). Gaussian coefficients satisfy their Pascal recurrence and $G (m, r; v^{2}) = v^{r (m - r)} {[\begin{matrix} m \\ r \end{matrix}]}_{v}$ (The quantum Pascal recurrences, the Gauss product formula and Gaussian integrality).

Proof

Given: The data above.

1.1F1F2givenconstructalgebra

For a homogeneous positive element $x$ of $i$ -weight $w$ , define $δ (x) = E_{i} x - v^{w} x E_{i}$ . It has weight $w + 2$ , and multiplication directly gives $δ (x y) = δ (x) y + v^{{wt}_{i} (x)} x δ (y)$ . Induction using this rule and Gaussian Pascal gives $δ^{m} (x) = \sum_{r = 0}^{m} (- 1)^{r} v^{r w + r (r - 1)} G (m, r; v^{2}) E_{i}^{m - r} x E_{i}^{r}$ : applying $δ$ to a summand raises the total weight from $w + 2 m$ to $w + 2 m + 2$ , and if $c_{m, r}$ is the coefficient of $E_{i}^{m - r} x E_{i}^{r}$ , its two contributions give $c_{m + 1, r} = c_{m, r} - v^{w + 2 m} c_{m, r - 1}$ . Substitution of the displayed coefficient reduces this to $G (m + 1, r; v^{2}) = G (m, r; v^{2}) + v^{2 (m - r + 1)} G (m, r - 1; v^{2})$ , exactly Pascal. Equivalently, substituting the Gaussian conversion in [F2], its coefficient is $(- 1)^{r} v^{r (w + m - 1)} {[\begin{matrix} m \\ r \end{matrix}]}_{v}$ .

2.1F1step 1.1algebra

The ordinary Serre relation is exactly $δ^{a + 1} (E_{j}) = 0$ , up to its nonzero scalar and reversal of the summation index: here $w = - a$ , so the exponent $r (w + m - 1)$ is zero when $m = a + 1$ . Applying the skew Leibniz rule repeatedly to $E_{j}^{n}$ , every summand of $δ^{m} (E_{j}^{n})$ is a scalar times $δ^{r_{1}} (E_{j}) \dots δ^{r_{n}} (E_{j})$ with $\sum r_{k} = m$ . If $m > a n$ , some $r_{k} > a$ , so that factor vanishes by the Serre relation and further applications of $δ$ . For $n = 0$ , $δ (1) = 0$ gives the same conclusion. Thus $δ^{m} (E_{j}^{n}) = 0$ under the asserted inequality.

3.1F2step 2.1algebra

Divide this zero identity generically by $[m]_{i}! [n]_{j}!$ and replace the index $r$ in step 1.1 by $m - r$ . The common nonzero scalar is $(- 1)^{m} v^{m (- a n + m - 1)}$ ; the remaining sum is exactly the one in the statement. Each of its factors is a divided power in the actual integral subalgebra, so this generic equality is already an equality there. Tensoring an equality with any specialization retains it; no specialized vanishing factorial is inverted.

4.1F1F2step 3.1algebra∎

The proof for $F$ takes place in the negative half with its positive-height grading: assign degree $α_{k}$ to $F_{k}$ for this argument and define $δ_{-} (x) = F_{i} x - v^{{wt}_{i} (x)} x F_{i}$ . Its same-sign Serre relations and the same multiplication computation give every preceding step verbatim, with $E$ replaced by $F$ . This completes both integral identities by finite algebraic computations.

Depends on

Used by

Quantum Frobenius and its kernel in the good odd-order regime Theorem

Dependency tree · two levels

16 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)