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.
Engel, the trace criterion, and Killing nondegeneracy
Statement
Let be a finite-dimensional complex vector space. If a Lie subalgebra consists entirely of nilpotent operators and , it has a common nonzero annihilated vector; it admits a basis in which all its operators are strictly upper triangular. If instead satisfies for all , , then is solvable.
For every finite-dimensional complex semisimple Lie algebra, the Killing form is symmetric, invariant and nondegenerate. All these assertions are choice-free, including the zero Lie algebra.
Facts & Assumptions
Given: The finite-dimensional complex Lie and trace conventions of Finite semisimple Lie algebras and the symmetric adjoint action.
A finite-dimensional endomorphism decomposes into the kernels of the irreducible powers in its minimal polynomial by Primary decomposition: the irreducible-power factors of split into their invariant kernels.
Finitely many residues at pairwise comaximal polynomial ideals are interpolated by Chinese remainder theorem for pairwise comaximal ideals.
Every nonconstant complex polynomial has a complex root by Fundamental theorem of algebra: every nonconstant complex polynomial has a complex root; finite division then splits it into linear factors.
Proof
If on , the commuting operators of left and right multiplication by on give For every summand is zero. Hence is nilpotent on any invariant subspace or quotient, in particular on a quotient of subalgebras stable under its action.
For a finite-dimensional Lie algebra , trace cyclicity proves symmetry of . Jacobi and trace cyclicity also give Consequently its radical is an ideal: for .
We record a finite spectral construction. By F3 and F1, an operator on a nonzero has a direct-sum decomposition with , each nilpotent. Define to act on by the scalar . For a map in , equals plus the difference of commuting nilpotent left and right actions. Its nilpotent part has exponent at most , by the same binomial expansion as in step 1.1. For every distinct difference , F2 supplies a polynomial with . These ideals are pairwise comaximal: distinct linear factors generate the unit ideal, and expanding a sufficiently high power of such a unit expression proves the same for their th powers. Therefore acts on this Hom space by , exactly . The difference zero is among the interpolation nodes, so . Thus Also , since each nilpotent block has trace zero.
Prove the common-zero-vector assertion by induction on , for all finite-dimensional nonzero representation spaces on which every operator is nilpotent. The zero algebra is immediate. Choose a proper subalgebra of maximal dimension. For , step 1.1 makes its adjoint action on nilpotent. Its image is a Lie algebra of dimension at most , so the induction hypothesis gives a nonzero coset annihilated by every . Hence , and is a subalgebra strictly containing . Maximality forces and makes a codimension-one ideal.
The induction hypothesis applied to on makes nonzero. It is -invariant because for , . The nilpotent restriction of to has a nonzero kernel: take the last nonzero vector in the finite power string of any nonzero vector of . This vector is killed by both and , hence by , completing the induction. Apply the same common-vector result to successive quotients of to obtain a finite invariant flag with zero action on each one-dimensional quotient. Lifting a basis of that flag gives strict upper triangularity. A product of strictly upper triangular operators is zero; expanding iterated brackets into products shows this algebra, and every subalgebra of it, is solvable (indeed nilpotent).
Now suppose the trace-zero hypothesis holds and fix . Use the operator and polynomial from step 2.1. Write with , a finite sum by the definition of the derived subspace. Cyclicity of finite matrix trace gives Indeed is an ideal by Jacobi, and implies , so each last trace vanishes by the hypothesis. Step 2.1 now gives a sum of nonnegative real numbers . Each is zero, so is nilpotent on .
Thus every element of is a nilpotent operator. Step 3.1 makes this derived algebra solvable. If its derived series vanishes after steps, that of vanishes after , proving the trace criterion. If , then and the same conclusion is immediate without spectral decomposition.
Suppose is semisimple. For , the adjoint actions preserve and act by zero on . Computing trace in a basis extending one of gives . Thus satisfies step 4.1's trace hypothesis and is solvable. Its kernel in is the center, which is abelian; explicitly, if then lies in that center and . Hence is a solvable ideal of and is zero by semisimplicity. This proves nondegeneracy. For the unique form has zero radical. Every induction, basis, polynomial interpolation and eigenvalue factorization above is finite; no algebraic closure or arbitrary-index selection is taken, so no AC is used.
Depends on
- Finite semisimple Lie algebras and the symmetric adjoint action
- Primary decomposition: the irreducible-power factors of $\mu_T$ split $V$ into their invariant kernels
- Chinese remainder theorem for pairwise comaximal ideals
- Fundamental theorem of algebra: every nonconstant complex polynomial has a complex root
Used by
Dependency tree · two levels
17 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, Lie Groups and Lie Algebras, §§15–17; finite-dimensional local trace proof (standard reference, not scraped)