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.
A Levi decomposition of the Euclidean-motion algebra of R^3
Example
The Euclidean-motion algebra of three-space has the Levi decomposition
where translations form the radical and rotations form a Levi factor.
Facts & Assumptions
Given: The standard action of on and the resulting semidirect-product bracket.
A Levi decomposition is a vector-space semidirect sum of the radical and a semisimple subalgebra (Levi subalgebras and Levi decompositions).
Verification
Put . In the semidirect product, . Hence is an abelian ideal, and the quotient by it is .
Under the vector-space identification , , one has . If an ideal of contains a nonzero , then the vectors as varies span , and a further bracket supplies the -direction. Thus the ideal is all of . The algebra is nonabelian and , so it is simple and not solvable.
Let be a solvable ideal of . Its image in the quotient is a solvable ideal of , hence is zero by step 1.2. Thus . Conversely is itself a solvable ideal by step 1.1, so it is the radical.
The subalgebra is semisimple, meets in zero, and together with spans the whole algebra. It is therefore a Levi factor by [L1]. The zero intersections and full quotient are explicit, and no choice is used.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
4 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
- Kirillov, An Introduction to Lie Groups and Lie Algebras, so(3) and its standard action (standard reference, not scraped)