ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedaudited 2026-09-22

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 root sl_2 triple inside sl_n

Example

Assume AC (The Axiom of Choice). In ${s l}_{n} (C)$ with the diagonal Cartan subalgebra $h$ and the root $α = ε_{i} - ε_{j}$ of Diagonal Cartan subalgebra and roots of sl_n ( $i \neq j$ ), the triple $e_{α} = E_{i j}, f_{α} = E_{j i}, h_{α} = E_{i i} - E_{j j}$ satisfies $[e_{α}, f_{α}] = h_{α}$ , $[h_{α}, e_{α}] = 2 e_{α}$ and $[h_{α}, f_{α}] = - 2 f_{α}$ , so it is a root ${s l}_{2}$ triple in the sense of The root sl_2 triple; moreover the Killing-dual vector is $H_{α} = \frac{1}{2 n} (E_{i i} - E_{j j})$ , consistently with $h_{α} = 2 H_{α} / α (H_{α})$ (Killing-dual vector of a root, Coroot of a Lie-algebra root).

Facts & Assumptions

Given: AC; the algebra ${s l}_{n} (C)$ with its diagonal Cartan subalgebra $h$ and root $α = ε_{i} - ε_{j}$ , $i \neq j$ , as in Diagonal Cartan subalgebra and roots of sl_n, the matrix units $E_{a b}$ , and the notions of Killing-dual vector and coroot from Killing-dual vector of a root and Coroot of a Lie-algebra root.

Verification

technique · direct

1.1

The Killing form of ${s l}_{n} (C)$ is $B (X, Y) = 2 n tr (X Y)$ on traceless matrices: on the basis of matrix units, ${ad}_{E_{a b}} (E_{c d}) = δ_{b c} E_{a d} - δ_{d a} E_{c b}$ , and summing the diagonal contributions of ${ad}_{E_{a b}} {ad}_{E_{c d}}$ over the basis gives $2 n δ_{a d} δ_{b c} - 2 δ_{a b} δ_{c d}$ , which is $2 n tr (E_{a b} E_{c d})$ on traceless elements because the correction term vanishes there.

givenalgebra

2.1

With this form, $B (\frac{1}{2 n} (E_{i i} - E_{j j}), H) = tr ((E_{i i} - E_{j j}) H) = x_{i} - x_{j} = α (H)$ for $H = diag (x_{1}, \dots, x_{n}) \in h$ , so $H_{α} = \frac{1}{2 n} (E_{i i} - E_{j j})$ . Since $H_{α}$ is a multiple of the traceless diagonal matrix $E_{i i} - E_{j j}$ , we get $α (H_{α}) = \frac{1}{2 n} α (E_{i i} - E_{j j}) = \frac{2}{2 n} = \frac{1}{n}$ , and therefore $2 H_{α} / α (H_{α}) = 2 n H_{α} = E_{i i} - E_{j j}$ .

givenstep 1.1algebra

3.1

The bracket relations are matrix multiplications: $[E_{i j}, E_{j i}] = E_{i i} - E_{j j}$ , $[E_{i i} - E_{j j}, E_{i j}] = 2 E_{i j}$ and $[E_{i i} - E_{j j}, E_{j i}] = - 2 E_{j i}$ . Hence the displayed triple satisfies exactly the relations of The special linear Lie algebra sl_2 with $h_{α}$ in the role of $h$ , which is the claim of The root sl_2 triple realized concretely.

givenstep 2.1algebra∎

Depends on

Used by

Root strings in type A₂ Example
The Killing form identifies roots with coroot directions Example

Dependency tree · two levels

27 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

Pavel Etingof, MIT 18.745 Lie Groups and Lie Algebras I, Lectures 19–24 (standard reference, not scraped)