Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-14
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 solvability criterion

Statement

Let g be finite-dimensional over a characteristic-zero field. Then g is solvable if and only if Kg(g,[g,g])=0.

More generally, a finite-dimensional linear Lie algebra h⊆gl(V) is solvable if tr⁡(xy)=0 for all x∈[h,h] and y∈h; when h is solvable, these traces do vanish.

Facts & Assumptions

Given: Finite-dimensional vector spaces and Lie algebras over a field of characteristic zero.

[L1]

Every finite-dimensional representation of a solvable algebra over an algebraically closed characteristic-zero field is simultaneously upper triangularizable (Simultaneous triangularization of solvable representations).

[L2]

If every adjoint operator of a finite-dimensional algebra is nilpotent, that algebra is nilpotent (Engel's theorem).

[L3]

An algebra is solvable exactly when its derived algebra is nilpotent in the linear situation used here (Solvability criterion via the derived algebra).

[L4]

Solvable ideals and solvable quotients give solvable extensions (Subalgebras, quotients, and extensions of solvable Lie algebras).

[L6]

Every finite-dimensional endomorphism over an algebraically closed field has Jordan canonical form (Every finite-dimensional endomorphism over an algebraically closed field has Jordan form).

[L7]

The Killing form is the trace form of the adjoint representation (Killing form).

Proof

technique · scalar reduction, Jordan decomposition, and Engel
1.1L1L5algebra

Suppose first that h is solvable. Choose bases of h and V, and let k0⊆k be the subfield generated over Q by the finitely many structure constants and matrix entries. The resulting k0-form h0 is solvable because its derived series becomes that of h after the faithful scalar extension k0⊆k. The finitely generated field k0 embeds in C. Over C, [L1] gives a basis in which h0 is upper triangular and its derived algebra is strictly upper triangular. Thus tr⁡(yx)=0 for all x∈[h0,h0] and y∈h0. These finitely many bilinear identities hold over k0 and hence after extension to k.

1.2L5algebra

We prove the converse first under the stronger hypothesis tr⁡(xy)=0 for every x,y∈h. Choose bases and let k0 be the characteristic-zero subfield generated by the finitely many matrix entries of a basis of h and its structure constants. The strong trace hypothesis is determined by the finitely many pairs of basis vectors, so it persists after extending the resulting k0-form to C. Solvability over C descends because every derived term commutes with scalar extension. We may therefore carry out the strong converse over C.

1.3L6algebra

Over C, fix x∈[h,h]. By [L6], choose a Jordan basis on V and write x=xs+xn, where xs is diagonal, xn is block-nilpotent, and they commute. The commuting left and right multiplication operators on End⁡(V) show that the semisimple part of ad⁡x=Lx−Rx is ad⁡xs. Write the diagonal entries of xs as a1,…,an, and let xs‾ have diagonal entries a1‾,…,an‾. On the generalized eigenspaces of ad⁡x, ad⁡xs‾ has eigenvalues ai−aj‾. Finite Hermite interpolation on the finitely many differences ai−aj, taking zero to zero, expresses ad⁡xs‾ as a polynomial without constant term in ad⁡x. Since h is stable under ad⁡x, it follows that [xs‾,h]⊆h.

2.1L2L3L5step 1.3algebra

Write x as a finite sum of commutators. By [L5], tr⁡(A[B,C])=tr⁡([A,B]C). Step 1.3 and the strong trace hypothesis therefore give tr⁡(xs‾x)=0. In the Jordan basis this trace is ∑iai‾ai, so every ai=0 and x is nilpotent. If xm=0 on V, then the commuting operators Lx,Rx on End⁡(V) satisfy (Lx−Rx)2m−1=0, because every binomial term contains either Lxm or Rxm. Restriction to the invariant derived algebra shows that each of its adjoint operators is nilpotent. Hence [L2] makes [h,h] nilpotent, and [L3] makes h solvable.

3.1step 1.1step 1.2step 1.3step 2.1algebra

Under the stated weaker hypothesis, apply steps 1.2–2.1 to the linear Lie algebra [h,h]: the required strong trace vanishing holds for every pair in it. Its solvability implies solvability of h by the derived-series definition. Together with step 1.1 this proves the linear criterion.

4.1L4L7step 1.1step 3.1∎

Apply the linear criterion to ad⁡(g). Its derived algebra is ad⁡([g,g]), and [L7] says that the trace hypothesis is precisely the asserted Killing-form condition. Hence ad⁡(g) is solvable. The exact sequence 0→Z(g)→g→ad⁡(g)→0 has abelian kernel, so [L4] makes g solvable. The reverse direction is step 1.1 for the adjoint representation. The zero algebra makes both conditions vacuous and is solvable.

Depends on

Dependency tree · 2 levels

Sources