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.
Cartan's semisimplicity criterion
Statement
A finite-dimensional Lie algebra over a characteristic-zero field is semisimple if and only if its Killing form is nondegenerate.
Facts & Assumptions
Given: A finite-dimensional characteristic-zero Lie algebra with Killing form .
The radical of an invariant form is an ideal (Orthogonal complements under invariant forms are ideals).
Cartan's solvability criterion detects solvability from the relevant trace pairing (Cartan's solvability criterion).
Semisimple means that the solvable radical is zero (Simple, semisimple, and reductive Lie algebras).
Proof
Suppose is semisimple and let be the radical of . It is an ideal by [L1]. For , the operator maps into and induces zero on ; its trace on therefore equals the trace of its restriction to . Thus the intrinsic Killing form of is the restriction of , hence zero.
Conversely suppose is nondegenerate and let be an abelian ideal. For and , put . Its image lies in , while vanishes on because and is abelian. Hence , so . Nondegeneracy forces ; thus has no nonzero abelian ideal.
By [L2], step 1.1 makes solvable. It is a solvable ideal of the semisimple algebra , so [L3] gives . Therefore is nondegenerate.
If had a nonzero solvable ideal , let be the last nonzero term of its derived series: it is nonzero and abelian, and it is an ideal of because derived terms of an ideal are ideals of the ambient algebra by Jacobi. This contradicts step 1.2. Thus the radical is zero and [L3] makes semisimple. For , the unique bilinear form has zero radical and is nondegenerate in the standard vacuous sense, so both directions still hold.
Depends on
Used by
- Levi factors are noncanonical but conjugate Corollary
- Semisimple Lie algebras are centerless and perfect Corollary
- Classical simple Lie algebras and their Killing forms Example
- Killing form of sl₂ Example
- Derivations of semisimple Lie algebras are inner Theorem
- Semisimple Lie algebras decompose into simple ideals Theorem
- Weyl's complete reducibility theorem Theorem
Dependency tree · two levels
13 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
- Milne, Lie Algebras, Theorem 4.13 (standard reference, not scraped)