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.

Existence and characteristicity of the nilradical in characteristic zero

Statement

Every finite-dimensional characteristic-zero Lie algebra has a unique largest nilpotent ideal, and this ideal is characteristic.

Facts & Assumptions

Given: A finite-dimensional Lie algebra g over a characteristic-zero field k.

[L1]

The nilradical, when it exists, is the largest nilpotent ideal (Nilradical).

[L2]

Every nilpotent Lie algebra is solvable (Nilpotent Lie algebras are solvable).

[L3]

Quotients and extensions of solvable Lie algebras are solvable (Subalgebras, quotients, and extensions of solvable Lie algebras).

[L4]

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

[L5]

If every adjoint endomorphism of a finite-dimensional Lie algebra is nilpotent, then the Lie algebra is nilpotent (Engel's theorem).

[L6]

Extension of scalars from F to a field extension K is KF (Restriction of scalars and extension of scalars SRM along a ring homomorphism RS).

Proof

technique · direct
1.1

Let i and j be nilpotent ideals of g, and put s=i+j. This is an ideal. Both summands are solvable by [L2], and the map js/i, yy+i, is a surjective Lie homomorphism, so the quotient is solvable by the quotient assertion in [L3]. The extension assertion in [L3] then makes s solvable.

givenL2L3algebra
2.1

Choose a basis of g adapted simultaneously to ij, i, and j, and let k0k be generated over Q by its finitely many structure constants. The same table and the corresponding coordinate subspaces define g0, i0, j0, and s0=i0+j0 over k0, whose extensions to k are the original objects. Direct expansion on pure tensors and induction give γr(KFa)=KFγr(a) and (KFa)(r)=KFa(r) for every field extension K/F. Since a finite basis stays a basis after field extension, extension is faithful here. Thus i0 and j0 are nilpotent and s0 is solvable by step 1.1.

L6step 1.1algebra
3.1

The finitely generated field k0/Q is countable, enumerated by rational expressions in its generators. In ZF construct an algebraic closure K by a fixed countable tower: dovetail the polynomials over all earlier stages, take the least-coded monic irreducible factor of the next nonconstant polynomial, adjoin one root, and take the union. Every polynomial over the union occurs at a finite stage and later acquires a root, so K is algebraically closed. Put G=Kk0g0 and similarly I=Kk0i0, J=Kk0j0, and S=I+J. By step 2.1, S is a finite-dimensional solvable ideal of G, while I and J are nilpotent ideals. The construction uses a fixed enumeration and least natural-number codes, not a choice function.

L6step 2.1algebra
4.1

Apply [L4] to the adjoint representation of S on G. For xI, ideality gives (adx)r(G)γr(I) for r1, so adx is nilpotent; the same holds for every yJ. In the common upper-triangular basis supplied by [L4], each such operator therefore has zero diagonal. Every s=x+yS consequently has ads=adx+ady strictly upper triangular, so its restriction to S is nilpotent. Engel's theorem [L5] makes S nilpotent.

L4L5step 3.1algebra
5.1

If γc+1(S)=0, step 2.1 gives 0=Kk0γc+1(s0), so faithfulness yields γc+1(s0)=0 and then γc+1(s)=kk0γc+1(s0)=0. Thus the sum of any two nilpotent ideals of g is nilpotent. This includes zero summands.

L6step 2.1step 4.1
6.1

Let n be the algebraic sum of all nilpotent ideals of g, with the sum of the empty subfamily understood as 0. It is an ideal. A finite basis of n consists of finite sums of elements from finitely many nilpotent ideals, so n is already the sum of finitely many of them. Repeated application of step 5.1 makes n nilpotent. It contains every nilpotent ideal, hence is the unique largest one and is the object defined in [L1]. The reduction uses only finitely many witnesses attached to a finite basis, so it is valid in ZF.

L1step 5.1algebra
7.1

If f is an automorphism of g, bracket preservation carries every nilpotent ideal to a nilpotent ideal, so maximality gives f(n)n. Applying the same argument to f1 gives the reverse inclusion. Therefore f(n)=n, and the nilradical is characteristic. For g=0, the construction gives n=0 and the same conclusion. Characteristic zero is used in steps 2.1–4.1 through Qk and Lie triangularization; no form of AC is used.

L1step 6.1algebra

Depends on

Used by

Cited to discharge well-definedness by Nilradical.

Dependency tree · two levels

19 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