Alphabeta Math
TheoremStatement: 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.

PBW symmetrization in characteristic zero

Statement

Suppose char⁡k=0 and a basis of g equipped with a total order is supplied. The linear map defined on homogeneous products by

sym⁡(v1⋯vn)=1n!∑π∈Snιg(vπ(1))⋯ιg(vπ(n))

is a filtered vector-space isomorphism sym⁡:S(g)→U(g). In general it is not an algebra homomorphism.

Facts & Assumptions

Given: A characteristic-zero field k, a Lie algebra g over k, and a specified totally ordered basis of g.

[L3]

PBW identifies the symbol map σ:S(g)→gr⁡U(g) as a graded-algebra isomorphism (Poincaré–Birkhoff–Witt theorem).

Proof

technique · induction on filtration degree after constructing the map
1.1L1L2construct

By [L1] the coefficient 1/n! exists. Reindexing the finite sum by π↦πτ for any τ∈Sn shows by [L2] that the displayed multilinear expression is invariant under permuting the inputs, so it descends to a linear map on Sn(g); for n=0 it sends 1 to 1. Taking the graded direct sum defines sym⁡, and degree n maps into FnU(g).

1.2baseL3

In degree zero, sym⁡:S0(g)=k→F0U(g) has associated-graded map σ0, hence is bijective by [L3].

1.3ihassume-hyp

Assume that every element of Fn−1U(g) has a unique preimage in ⨁r<nSr(g).

2.1step 1.1L1L3algebra

In Fn/Fn−1 all reordered products of v1,…,vn have the same symbol, because interchanging adjacent factors changes a word by a bracket term of degree n−1. Thus the leading symbol of sym⁡(v1⋯vn) is the average of n! identical symbols, namely σ(v1⋯vn). Hence gr⁡(sym⁡)=σ.

3.1step 2.1step 1.3L3choose

Given u∈Fn, use the surjectivity of σn and step 2.1 to choose sn∈Sn(g) whose symmetrization has the same class as u in Fn/Fn−1. Then u−sym⁡(sn)∈Fn−1 and step 1.3 supplies a preimage, proving surjectivity through degree n.

3.2step 2.1step 1.3L3algebra

If s=∑r≤nsr and sym⁡(s)=0, its top filtration class is σn(sn) by step 2.1, so sn=0 by injectivity of [L3]. Descending in degree, or using the uniqueness clause in step 1.3, gives every sr=0. Thus symmetrization is injective through degree n.

4.1step 1.2step 3.1step 3.2discharge-induction: step 1.2∎

Steps 1.2–3.2 complete the filtration induction. Every element of either algebra has finite degree, so sym⁡ is a filtered vector-space isomorphism on the full direct sums. The proof asserts no multiplicativity.

Depends on

Used by

Dependency tree · two levels

44 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