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.
Injectivity is not part of the enveloping quotient definition
Statement
The canonical map is injective merely by the definition of as a quotient.
Facts & Assumptions
Given: The claim that quotient formation alone proves injectivity.
The definition makes the canonical map the composite (Universal enveloping algebra).
Its injectivity is a PBW corollary (The canonical map g→U(g) is injective).
Refutation
From [L1] alone, the kernel of the composite is exactly , with viewed in tensor degree one. A quotient definition supplies no assertion that this intersection is zero; for comparison, the quotient kills its entire degree-one subspace.
PBW proves that the special enveloping ideal has , yielding [L2]. Thus injectivity is true, but it is a theorem using PBW rather than a consequence built into the quotient definition, so the statement as phrased is false.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
6 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
- Etingof, MIT 18.745 notes, Corollary 13.3, printed p. 75 (standard reference, not scraped)