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.
Subalgebras, quotients, and extensions of solvable Lie algebras
Statement
Subalgebras and quotients of solvable Lie algebras are solvable. If is a solvable ideal of and is solvable, then is solvable; more precisely,
Facts & Assumptions
Given: A Lie algebra , a subalgebra , and, for the quotient and extension assertions, an ideal .
Solvability is termination of the derived series (Derived series and solvable Lie algebras).
An ideal defines a quotient Lie algebra and a surjective canonical projection (Quotient Lie algebras).
The kernel of a Lie homomorphism is an ideal and its quotient by the kernel identifies with its image (Kernels, images, and the first isomorphism theorem for Lie algebras).
Proof
Induction on gives : it is clear at , and bracketing a subspace with itself preserves containment. Therefore a vanishing derived term of forces the corresponding term of to vanish.
Bracket preservation and surjectivity of the canonical map in [L2] give for every . Thus every solvable quotient of terminates no later than ; [L3] records the same calculation for any homomorphic image.
Suppose and . Step 1.2 gives , so . Iterating the derived operation further times gives . This proves solvability and the bound, including or .
Depends on
Used by
- The radical is characteristic and its quotient has zero radical Proposition
- Cartan's solvability criterion Theorem
- Existence and characteristicity of the nilradical in characteristic zero Theorem
- Levi decomposition theorem Theorem
- Solvability criterion via the derived algebra Theorem
- The commutator with the radical lies in the nilradical Theorem
- The sum of solvable ideals is solvable Theorem
Dependency tree · two levels
8 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
- Milne, Lie Algebras, Proposition 3.4 (standard reference, not scraped)