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 Heisenberg algebra from a two-cocycle
Example
Let be abelian and let be the trivial one-dimensional -module. The alternating form determined by
is a -cocycle. Its associated abelian extension is the three-dimensional Heisenberg algebra
Facts & Assumptions
Given: The displayed two-dimensional abelian algebra and trivial module over a characteristic-zero field.
Verification
Since both the bracket of and its action on are zero, every term in the Chevalley–Eilenberg differential of a -cochain vanishes. Equivalently, the possible target is already zero because . Hence .
The same triviality makes the differential zero, so the nonzero form is not a coboundary. Indeed is one-dimensional, generated by .
On define ; this is the usual cocycle-extension formula here because the action and the bracket of are both zero. It is bilinear and alternating, and Jacobi holds because every bracket lies in , which brackets to zero. Its kernel is abelian, its quotient is , and the induced action is trivial, so it is the abelian extension represented by . Its only nonzero basis bracket is . Renaming the three basis vectors gives exactly the displayed Heisenberg relations. This checks the zero and one-dimensional boundary spaces explicitly and uses no choice.
Used by
Nothing in the library uses this result yet.
Dependency tree · 0 levels
Nothing. This result depends on no other item in the library.
Sources
- Weibel, An Introduction to Homological Algebra, extension construction (standard reference, not scraped)