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 Killing form identifies roots with coroot directions
Example
Assume AC (The Axiom of Choice). In with the diagonal Cartan subalgebra of Diagonal Cartan subalgebra and roots of sl_n and the root , the Killing form establishes the isomorphism and the root corresponds to , while its coroot is Thus the coroot is the vector in whose direction is the Killing-dual direction of the root, rescaled so that ; the scalars are .
Facts & Assumptions
Given: AC; the algebra with diagonal Cartan subalgebra and root from Diagonal Cartan subalgebra and roots of sl_n, the Killing form of Killing form with the nondegeneracy on of Orthogonality of root spaces and nondegeneracy on the Cartan subalgebra, and the dual vector and coroot of Killing-dual vector of a root, Coroot of a Lie-algebra root and The Killing length of a root is nonzero.
Verification
The Killing form of is , so for and a diagonal traceless with coordinates one gets . Hence is exactly the Killing-dual vector of from Killing-dual vector of a root, and the map is an isomorphism onto because is nondegenerate by Orthogonality of root spaces and nondegeneracy on the Cartan subalgebra.
Since is traceless diagonal, , and therefore , which is nonzero as required by The Killing length of a root is nonzero and agrees with the direct computation .
Hence by Coroot of a Lie-algebra root, and the coroot triple , , is the one computed in The root sl_2 triple inside sl_n; in particular the coroot direction is the dual direction of the root under the Killing form, and the normalization is exactly .
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
29 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)