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.
The Casimir operator is basis-independent and intertwining
Statement
The Casimir element is independent of the chosen dual bases and belongs to the center of . Consequently its action on every -module is a -intertwiner.
Facts & Assumptions
Given: The data in the Casimir definition.
The element is the image of the dual-basis tensor under multiplication in (Casimir operator relative to an invariant form).
Invariance means (Trace forms are symmetric and invariant).
A representation extends uniquely to an algebra homomorphism from the universal enveloping algebra (Universal property of the enveloping algebra).
Proof
The form isomorphism sends . Under , the identity corresponds to . Hence is the inverse tensor of and is independent of the basis. Multiplication into proves the same for .
For , the diagonal adjoint action on the inverse tensor is . Pairing its second factor with an arbitrary vector and using [L2] shows that this tensor is zero. Multiplication sends it to , hence that commutator is zero. Since generates , is central.
By [L3], any module action extends to . Centrality gives for every , precisely the intertwining condition. For , the inverse tensor and Casimir are empty sums and all assertions reduce to .
Depends on
Used by
- Second Whitehead lemma Theorem
- Weyl's complete reducibility theorem Theorem
Cited to discharge well-definedness by Casimir operator relative to an invariant form.
Dependency tree · two levels
10 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 5.17 (standard reference, not scraped)