LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10

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.

Serre elements vanish before Serre generation

Statement

For every finite GCM and $i \neq j$ , the maximal-ideal quotient satisfies $(ad e_{i})^{1 - a_{i j}} e_{j} = 0$ and $(ad f_{i})^{1 - a_{i j}} f_{j} = 0$ . This asserts vanishing, without yet asserting generation of the defining ideal.

Facts & Assumptions

Given: The standard simple generators in g(A), and i≠j.

[F1]

A negative vector killed by all opposite simple generators is zero. (The opposite simple centralizer in a Kac Moody half vanishes).

[F2]

The algebra $g (A)$ is the quotient of $\tilde{g} (A)$ by the largest Cartan-disjoint ideal and retains the generator names $h, e_{i}, f_{i}$ . (Kac moody algebra associated to a gcm).

[F3]

Before the quotient, the generators satisfy $[h, h^{'}] = 0$ , $[h, e_{i}] = α_{i} (h) e_{i}$ , $[h, f_{i}] = - α_{i} (h) f_{i}$ , and $[e_{i}, f_{j}] = δ_{i j} h_{i}$ . (Contragredient lie algebra before the maximal ideal quotient).

Proof

1.1

The relations of F3 descend through the quotient of F2. For operators $E, F, H$ with $[E, F] = H$ and $[H, F] = - 2 F$ , the identity $[E, F^{m}] = m F^{m - 1} (H - m + 1)$ follows from $[E, F^{m + 1}] = [E, F^{m}] F + F^{m} H$ and $H F = F (H - 2)$ , starting at $m = 1$ . Take the adjoint operators of $e_{i}, f_{i}, h_{i}$ . On $v = f_{j}$ , $E v = 0$ and $H v = - a_{i j} v$ . For $m = 1 - a_{i j}$ , the identity gives $E F^{m} v = m (- a_{i j} - m + 1) F^{m - 1} v = 0$ .

F2F3given

2.1

For $k \notin {i, j}$ , $ad e_{k}$ commutes with $ad f_{i}$ and kills $f_{j}$ , so kills $F^{m} v$ . For $k = j$ , it commutes with $F$ and sends $f_{j}$ to $h_{j}$ , so sends $F^{m} v$ to $F^{m} h_{j}$ . Now $F h_{j} = a_{j i} f_{i}$ and $F^{2} h_{j} = 0$ . If $m \geq 2$ this vanishes; if $m = 1$ , $a_{i j} = 0$ and the symmetric-zero axiom gives $a_{j i} = 0$ . Thus all $e_{k}$ kill the negative Serre vector.

F2F3givenstep 1.1

3.1

F1 kills this vector in $n^{-}$ . The sign-changing involution descending in F2 proves the positive relation with the same exponent. At no point has an ideal been asserted to be generated by these vectors.

F1F2step 1.1step 2.1∎

Sources

Source comparison: Kleshchev, §1.4 Serre vanishing and Lemma 3.1.1; Perrin Propositions 4.2.6–4.2.7, pp.35–37.

Additional source: Perrin, section 4.2, at the numbered locators above.

Depends on

Used by

Dependency tree · two levels

8 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

Kleshchev, Lectures on Infinite Dimensional Lie Algebras — §1.4 Serre vanishing and Lemma 3.1.1; Perrin Propositions 4.2.6–4.2.7, pp.35–37 (standard reference, not scraped)
Nicolas Perrin, Introduction to Kac-Moody groups and Lie algebras, section 4.2 (standard reference, not scraped)