Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)
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 basis and exterior associated graded for a Clifford algebra

Statement

Let k be a field of characteristic not 2, let V be finite-dimensional of dimension n, and let B be any symmetric bilinear form on V, possibly degenerate; put Q(v)=B(v,v). Fix an ordered basis e1,…,en. Then

1,eˉi1⋯eˉir(1≤i1<⋯<ir≤n)

is a k-basis of Cl(V,Q), so dim⁡kCl(V,Q)=2n. Give Cl(V,Q) the word-length filtration F−1=0 and, for m≥0, let Fm be the span of products of at most m canonical generators. The natural graded algebra map

ΛV⟶gr⁡FCl(V,Q)=⨁m≥0Fm/Fm−1

that sends v∈V to the degree-one class of vˉ is an isomorphism, where the graded product is induced by FpFq⊆Fp+q. No nondegeneracy hypothesis is needed.

Facts & Assumptions

Given: A field k of characteristic not 2, a finite-dimensional k-vector space V with ordered basis e1,…,en, a symmetric bilinear form B (possibly degenerate), and Q(v)=B(v,v). In the proof, End⁡k(W) denotes the unital k-algebra of k-linear maps W→W, with composition as multiplication.

[F1]

In Cl(V,Q) the canonical image satisfies vˉ 2=Q(v)1 (Universal Clifford algebra of a quadratic space).

[F2]

The polarized relation is vˉwˉ+wˉvˉ=2B(v,w)1 (Polarized relations in a Clifford algebra).

[F3]

A linear map V→A satisfying f(v)2=Q(v)1A extends uniquely to an algebra homomorphism Cl(V,Q)→A (Universal property of the Clifford algebra).

[F4]

ΛV is the tensor algebra quotient by the two-sided ideal generated by v2 for v∈V (Exterior Algebra Of A Finite Free Module).

[F5]

For an ordered basis of V, the increasing square-free wedges form a basis of ΛV (Exterior Algebra Basis Monomials).

[F6]

The operators c(v)=ϵv+ιv on ΛV are well defined and satisfy c(v)2=Q(v)I (Wedge and contraction operators satisfy the Clifford relations).

[F7]

A linear map V→A into a unital associative k-algebra extends uniquely to a unital algebra homomorphism Tk(V)→A (Universal property of the tensor algebra).

Proof

technique · direct
1.1F3F6construct

By [F6], c:V→End⁡k(ΛV) is linear and satisfies the quadratic relation. With endomorphism multiplication given by composition, [F3] gives a representation ρ:Cl(V,Q)→End⁡k(ΛV). For I=(i1<⋯<ir), the degree-r part of ρ(eˉi1⋯eˉir)(1) is exactly ei1∧⋯∧eir, since it comes from choosing every exterior-multiplication term; any contraction lowers the resulting degree.

1.2F1F2

The defining relation [F1] gives eˉi2=Q(ei)1, while [F2] gives eˉjeˉi=−eˉieˉj+2B(ei,ej)1 whenever j>i.

2.1step 1.2algebra

Use well-founded induction on the lexicographically ordered pair (word length, inversion count), where the inversion count of eˉi1⋯eˉir is the number of pairs a<b with ia>ib. Swapping an adjacent inversion lowers the inversion count in the same-length term and creates only a scalar correction of length two less; a sorted word with a repeated index has an adjacent square, which [F1] replaces by a scalar. Both resulting measures are smaller, so induction reduces every word to a linear combination of the displayed words and proves spanning.

2.2step 1.1F5algebra

If a linear relation among the spanning words were nonzero, choose its greatest word length r with a nonzero coefficient and apply ρ to 1. Shorter words have exterior degree at most their word length, so the degree-r component is a relation among distinct basis wedges from [F5]; their linear independence forces all coefficients of length r to vanish, a contradiction. Descending over the finitely many lengths proves independence.

3.1F1F2step 1.2step 2.1step 2.2

For each m, the relations in [F1] and [F2] never increase word length, so the words of length at most m span Fm. Steps 2.1 and 2.2 show that the ordered square-free words of length at most m are a basis of Fm.

4.1F1F4F7step 3.1

The filtration is multiplicative because concatenating words of lengths at most p and q has length at most p+q. Send v to the class of vˉ in F1/F0 and extend to Tk(V) by [F7]. The square of each degree-one class is zero, since vˉ2=Q(v)1∈F0⊆F1; hence this tensor-algebra map kills each exterior relation in [F4]. Its kernel is a two-sided ideal because the map preserves sums and products, so it contains the ideal generated by those relations and induces a graded algebra map Φ:ΛV→gr⁡FCl(V,Q).

5.1F5step 3.1step 4.1

In degree m, [F5] gives the basis of ΛmV and step 3.1 gives the corresponding basis of Fm/Fm−1. The map Φ sends each basis wedge to its matching Clifford-word class, so it is a vector-space isomorphism in every degree and therefore a graded algebra isomorphism.

6.1step 2.1step 2.2step 4.1step 5.1algebra∎

Steps 2.1 and 2.2 prove the ordered-word basis; its words are indexed by subsets of the n basis vectors, and partitioning those subsets by size gives ∑r=0n(nr)=2n. Steps 4.1 and 5.1 prove the associated-graded assertion, including the boundary case n=0.

Remarks

No choice axiom is used. The ordered basis is part of the theorem's hypotheses, and the contraction, reduction, and exterior-action constructions are explicit.

Depends on

Used by

Dependency tree · two levels

14 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