DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

PBW symbol map from the symmetric algebra

Definition

The degree-one assignment

$x ⟼ ι_{g} (x) + F_{0} U (g) \in F_{1} U (g) / F_{0} U (g)$

is linear. Since $gr U (g)$ is commutative, the symmetric-algebra universal property gives a unique algebra homomorphism

$σ : S (g) ⟶ gr U (g) .$

It is graded because generators of degree one go to degree one. This is the PBW symbol map. Neither injectivity nor surjectivity is part of its definition.

Depends on

Dependency tree · 2 levels

Sources

Etingof, MIT 18.745 notes, §13.1, printed pp. 74–75