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.
Codimension-one ideal in a nonzero solvable Lie algebra
Statement
A nonzero finite-dimensional solvable Lie algebra over an algebraically closed field of characteristic zero has an ideal of codimension one. In fact, this lemma is valid over every field.
Facts & Assumptions
Given: A nonzero finite-dimensional solvable Lie algebra .
Solvability means the derived series eventually vanishes (Derived series and solvable Lie algebras).
An ideal has a quotient Lie algebra with a canonical projection (Quotient Lie algebras).
Rank-nullity computes codimension through a surjective linear map (Rank-nullity: ).
Proof
The derived algebra is proper. Otherwise , so every derived term would equal the nonzero algebra , contradicting solvability in [L1]. Thus the abelianization in [L2] is nonzero and finite-dimensional.
Choose a hyperplane : take one nonzero vector, extend it to a finite basis, and span all basis vectors except that one. The inverse image of in contains , so and is an ideal. By [L3], its codimension equals that of , namely one. Only a finite basis extension is used, so algebraic closure and characteristic zero are unnecessary and no Choice principle is invoked.
Depends on
Used by
- Lie's theorem Theorem
Dependency tree · two levels
11 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.23 (standard reference, not scraped)