Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

The PBW filtration is multiplicative and has commutative associated graded

Statement

For the PBW filtration,

FmU(g)FnU(g)Fm+nU(g).

Moreover [Fm,Fn]Fm+n1 when m+n1, and therefore grU(g) is commutative.

Facts & Assumptions

Given: A Lie algebra g and the PBW filtration on its enveloping algebra.

[L1]

Fn is spanned by words of length at most n (PBW filtration on the enveloping algebra).

[L2]

In U(g), ιg(x)ιg(y)ιg(y)ιg(x)=ιg([x,y]) (The canonical map to U(g) is a Lie homomorphism).

[L3]

Associated-graded multiplication is that of Associated graded algebra of a filtered algebra.

Proof

technique · direct
1.1

Concatenating a word of length at most m with one of length at most n gives length at most m+n. Taking spans and quotient images proves FmFnFm+n.

L1algebra
1.2

For a generator x and a word b1bs, repeated use of [x,ab]=[x,a]b+a[x,b] gives [x,b1bs]=jb1[x,bj]bs. By [L2], every [x,bj] is again the image of one element of g, so this commutator lies in Fs.

L2algebra
2.1

For words a=ax of length r>0 and b of length s>0, the identity [ax,b]=a[x,b]+[a,b]x, together with step 1.2 and induction on r, puts both terms in Fr+s1. The scalar boundary cases commute, and bilinearity therefore gives [Fm,Fn]Fm+n1.

step 1.1step 1.2algebra
3.1

If aFm and bFn, step 2.1 says that ab and ba have the same class in Fm+n/Fm+n1. By [L3], all homogeneous elements of grU(g) commute, hence the whole associated graded algebra is commutative.

step 2.1L3

Depends on

Used by

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