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 over a characteristic-zero field .
The nilradical, when it exists, is the largest nilpotent ideal (Nilradical).
Every nilpotent Lie algebra is solvable (Nilpotent Lie algebras are solvable).
Quotients and extensions of solvable Lie algebras are solvable (Subalgebras, quotients, and extensions of solvable Lie algebras).
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).
If every adjoint endomorphism of a finite-dimensional Lie algebra is nilpotent, then the Lie algebra is nilpotent (Engel's theorem).
Extension of scalars from to a field extension is (Restriction of scalars and extension of scalars along a ring homomorphism ).
Proof
Let and be nilpotent ideals of , and put . This is an ideal. Both summands are solvable by [L2], and the map , , is a surjective Lie homomorphism, so the quotient is solvable by the quotient assertion in [L3]. The extension assertion in [L3] then makes solvable.
Choose a basis of adapted simultaneously to , , and , and let be generated over by its finitely many structure constants. The same table and the corresponding coordinate subspaces define , , , and over , whose extensions to are the original objects. Direct expansion on pure tensors and induction give and for every field extension . Since a finite basis stays a basis after field extension, extension is faithful here. Thus and are nilpotent and is solvable by step 1.1.
The finitely generated field is countable, enumerated by rational expressions in its generators. In ZF construct an algebraic closure 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 is algebraically closed. Put and similarly , , and . By step 2.1, is a finite-dimensional solvable ideal of , while and are nilpotent ideals. The construction uses a fixed enumeration and least natural-number codes, not a choice function.
Apply [L4] to the adjoint representation of on . For , ideality gives for , so is nilpotent; the same holds for every . In the common upper-triangular basis supplied by [L4], each such operator therefore has zero diagonal. Every consequently has strictly upper triangular, so its restriction to is nilpotent. Engel's theorem [L5] makes nilpotent.
If , step 2.1 gives , so faithfulness yields and then . Thus the sum of any two nilpotent ideals of is nilpotent. This includes zero summands.
Let be the algebraic sum of all nilpotent ideals of , with the sum of the empty subfamily understood as . It is an ideal. A finite basis of consists of finite sums of elements from finitely many nilpotent ideals, so is already the sum of finitely many of them. Repeated application of step 5.1 makes 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.
If is an automorphism of , bracket preservation carries every nilpotent ideal to a nilpotent ideal, so maximality gives . Applying the same argument to gives the reverse inclusion. Therefore , and the nilradical is characteristic. For , the construction gives and the same conclusion. Characteristic zero is used in steps 2.1–4.1 through and Lie triangularization; no form of AC is used.
Depends on
Used by
- Derivations preserve the nilradical in characteristic zero Proposition
- The commutator with the radical lies in the nilradical Theorem
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
- Knapp, Lie Groups Beyond an Introduction, Proposition 1.40 and Corollary 1.41 (standard reference, not scraped)