Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 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.

Ado's theorem with nilpotent nilradical action

Statement

For every finite-dimensional Lie algebra g over a characteristic-zero field, there is a finite-dimensional faithful representation ρ such that ρ(x) is nilpotent for every xnilrad(g).

Facts & Assumptions

Given: Such a Lie algebra g.

[L1]

PBW identifies the associated graded enveloping algebra with a finite-variable polynomial algebra after a finite basis is fixed (Poincaré–Birkhoff–Witt theorem).

[L2]

The canonical map hU(h) is injective (The canonical map g→U(g) is injective).

[L3]

The Hilbert basis theorem makes finite-variable polynomial algebras Noetherian (Hilbert basis theorem: if R is Noetherian then R[x] is Noetherian).

[L4]

Every finite-dimensional solvable action over an algebraically closed characteristic-zero field admits a complete invariant flag and hence a common upper-triangular basis (Simultaneous triangularization of solvable representations).

[L5]

For every finite-dimensional characteristic-zero Lie algebra a, one has [a,rad(a)]nilrad(a) (The commutator with the radical lies in the nilradical).

[L6]

A Levi decomposition writes g=rs (Levi decomposition theorem).

[L7]

The derived algebra of a finite-dimensional solvable characteristic-zero algebra lies in its nilradical (The derived algebra of a solvable Lie algebra is nilpotent in characteristic zero).

[L8]

A finite-dimensional nilpotent algebra has a codimension-one ideal containing any prescribed proper subalgebra (Codimension-one ideals in nilpotent Lie algebras).

[L9]

Derivations preserve the nilradical (Derivations preserve the nilradical in characteristic zero).

[L10]

Every finite-dimensional semisimple Lie algebra over a characteristic-zero field is centerless (Semisimple Lie algebras are centerless and perfect).

Proof

technique · Zassenhaus extension, induction, and scalar descent
1.1

We first establish the extension construction over an algebraically closed field. Let a solvable algebra hgl(W) act faithfully, with every element of its nilradical n acting nilpotently, and let dDer(h). The case h=0 is immediate, so assume N=dimW1. Every Dd extends uniquely to a derivation of U=U(h): extend by the Leibniz rule on the tensor algebra; the derivation identity preserves each generator xyyx[x,y] of the enveloping ideal.

algebra
2.1

Let A be the finite-dimensional associative matrix algebra generated by 1 and h, let I be the kernel of UA, and let D be the associative algebra of operators on U generated by the extended derivations and 1. Put I0={uI:TuI for every TD}. Leibniz expansion shows I0 is a two-sided ideal. By [L4], all matrices from h are upper triangular and those from n are strictly upper triangular; if N=dimW, every product of N elements of n maps to zero. If J is the two-sided ideal generated by n, the relations UxnU for xn move the nilradical factors together and give JNI.

L4step 1.1algebra
3.1

Fix Dd and form the one-dimensional semidirect extension a=kDh. The solvable algebra h is an ideal of a, so hrad(a). By [L5], D(h)=[D,h]nilrad(a)h. This intersection is a nilpotent ideal of h, hence it lies in nilrad(h)=n. The extension of D to U therefore maps every nonconstant PBW monomial, and hence all of U after killing the scalar term, into J. It also preserves J: [L9] gives D(n)n, and the Leibniz rule handles the two-sided factors. Consequently it preserves JN, and every nonempty composition of extended derivations maps U into J. For u1,,uNI, expand T(u1uN) by the iterated Leibniz rule. If some ui receives no derivation, that term lies in the two-sided ideal I; otherwise every factor lies in J, so the term lies in JNI. Thus INI0I. By [L1], grUS(h); [L3] makes this finite-variable polynomial algebra Noetherian, and the filtered leading-term argument therefore makes U left Noetherian. In particular each left ideal Ij has a finite set of left generators. The left action of I on Ij/Ij+1 is zero, so these generators make that quotient a finitely generated U/I-module. Since U/IA is finite-dimensional, every Ij/Ij+1 is finite-dimensional. The finite filtration of U/IN with subquotients U/I,I/I2,,IN1/IN now proves that U/IN is finite-dimensional. Its quotient E=U/I0 is therefore finite-dimensional as well.

L1L3L5L9step 2.1
4.1

Represent h on E by left multiplication and d by the induced derivations. The identity [D,Lx]=LD(x) makes this a representation of dh. It is faithful: evaluation at the class of 1 first kills the h component by I0I and the original faithful matrix action, then evaluation at classes of xh kills the derivation component. Elements of n act nilpotently because JNI0. If D is nilpotent on h, its extension is nilpotent on each bounded PBW filtration piece and hence on finite E. Apply [L4] to the solvable algebra kDn: in the resulting common upper-triangular basis, both D and every yn have zero diagonal because they are nilpotent. Thus D+y is strictly upper triangular and hence nilpotent.

L2L4step 3.1algebra
5.1

We now prove the theorem for solvable g by induction on its dimension. In dimension zero use the zero representation; in dimension one, t acts faithfully and nilpotently on k2 by t(0t00). Assume the claim below the present dimension. If g is not nilpotent, [L7] gives [g,g]ng; the inverse image of a hyperplane in the abelian quotient g/n is a codimension-one ideal h containing n. If g is nilpotent, [L8] supplies a codimension-one ideal h. Apply the induction hypothesis to h. For xh, if D=adxh=0, then necessarily g is nilpotent and is the direct sum of kx and h; add the displayed two-dimensional representation. If D0, step 4.1 applied to kDh restricts faithfully to g. When g is nilpotent, D is nilpotent and the whole image is nil; otherwise its nilradical lies in h, where step 4.1 makes its image nilpotent.

L4L7L8step 4.1baseIH
6.1

For general g, use [L6] and write g=rs. The nilradical of r equals that of g: one inclusion is clear, while [L9] makes nilrad(r) invariant under every adxr and hence an ideal of g. Step 5.1 gives a faithful representation of r with nilpotent action of this common nilradical. Transport the derivation action of s to its image and apply step 4.1. Precompose the resulting representation with sr and take its direct sum with the adjoint representation of s on itself, which is faithful by [L10]. The second summand kills any remaining kernel in s; the first is faithful on r. Thus the sum is faithful, and elements of the nilradical act nilpotently on both summands.

L6L9L10step 4.15.1
7.1

Finally, over an arbitrary characteristic-zero field k, choose a basis of g adapted to its nilradical and let k0k be the finitely generated subfield containing its structure constants. The span n0 of the selected nilradical basis vectors is a nilpotent ideal of the resulting k0-form, so it lies in that form's nilradical and extends to the original nilradical. Embed k0 in C and perform steps 1.1–6.1 after adjoining the finitely many eigenvalues used in the triangularizations. All subsequent operations are finite-dimensional linear algebra and PBW operations, so the finitely many matrix coefficients lie in a finite algebraic extension K/k0. Restrict scalars from K to k0 and then extend scalars from k0 to k. Injectivity is preserved. The characteristic-polynomial coefficients of every linear combination of the matrices representing a basis of n0 vanish over the infinite field k0 and hence identically, so every element of n0k0k=nilrad(g) still acts nilpotently. This proves the theorem over k. For g=0, the zero-dimensional representation is faithful and the nilpotence clause is vacuous. Every descent, algebraic adjunction, and basis choice is finite, so no axiom of choice is invoked.

step 5.1step 6.1discharge-induction: step 5.1

Depends on

Used by

Dependency tree · two levels

53 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