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 be a field of characteristic not , let be finite-dimensional of dimension , and let be any symmetric bilinear form on , possibly degenerate; put . Fix an ordered basis . Then
is a -basis of , so . Give the word-length filtration and, for , let be the span of products of at most canonical generators. The natural graded algebra map
that sends to the degree-one class of is an isomorphism, where the graded product is induced by . No nondegeneracy hypothesis is needed.
Facts & Assumptions
Given: A field of characteristic not , a finite-dimensional -vector space with ordered basis , a symmetric bilinear form (possibly degenerate), and . In the proof, denotes the unital -algebra of -linear maps , with composition as multiplication.
In the canonical image satisfies (Universal Clifford algebra of a quadratic space).
The polarized relation is (Polarized relations in a Clifford algebra).
A linear map satisfying extends uniquely to an algebra homomorphism (Universal property of the Clifford algebra).
is the tensor algebra quotient by the two-sided ideal generated by for (Exterior Algebra Of A Finite Free Module).
For an ordered basis of , the increasing square-free wedges form a basis of (Exterior Algebra Basis Monomials).
The operators on are well defined and satisfy (Wedge and contraction operators satisfy the Clifford relations).
A linear map into a unital associative -algebra extends uniquely to a unital algebra homomorphism (Universal property of the tensor algebra).
Proof
By [F6], is linear and satisfies the quadratic relation. With endomorphism multiplication given by composition, [F3] gives a representation . For , the degree- part of is exactly , since it comes from choosing every exterior-multiplication term; any contraction lowers the resulting degree.
The defining relation [F1] gives , while [F2] gives whenever .
Use well-founded induction on the lexicographically ordered pair (word length, inversion count), where the inversion count of is the number of pairs with . 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.
If a linear relation among the spanning words were nonzero, choose its greatest word length with a nonzero coefficient and apply to . Shorter words have exterior degree at most their word length, so the degree- component is a relation among distinct basis wedges from [F5]; their linear independence forces all coefficients of length to vanish, a contradiction. Descending over the finitely many lengths proves independence.
For each , the relations in [F1] and [F2] never increase word length, so the words of length at most span . Steps 2.1 and 2.2 show that the ordered square-free words of length at most are a basis of .
The filtration is multiplicative because concatenating words of lengths at most and has length at most . Send to the class of in and extend to by [F7]. The square of each degree-one class is zero, since ; 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 .
In degree , [F5] gives the basis of and step 3.1 gives the corresponding basis of . 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.
Steps 2.1 and 2.2 prove the ordered-word basis; its words are indexed by subsets of the basis vectors, and partitioning those subsets by size gives . Steps 4.1 and 5.1 prove the associated-graded assertion, including the boundary case .
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
- Universal Clifford algebra of a quadratic space
- Polarized relations in a Clifford algebra
- Universal property of the Clifford algebra
- Universal property of the tensor algebra
- Wedge and contraction operators satisfy the Clifford relations
- Exterior Algebra Of A Finite Free Module
- Exterior Algebra Basis Monomials
Used by
- Euclidean Spin is the universal cover of SO(n) for n at least three Corollary
- A degenerate one-dimensional Clifford algebra need not be semisimple Counterexample
- A one-dimensional Clifford algebra for any quadratic coefficient Example
- Low-signature real Clifford algebras as C, H, and matrix algebras Example
- Pin lift squares and the Spin(2) double-angle map Example
- The split even Clifford algebra in signature (1,1) Example
- The zero quadratic form gives the exterior algebra Example
- Even subalgebras of real and complex Clifford algebras Lemma
- Graded Cₙ modules and ungraded C_(n−1) modules Lemma
- Local Spin lift from the matrix logarithm Lemma
- Low-dimensional real Clifford algebra models Lemma
- Real Clifford signature recurrences and eightfold periodicity Lemma
- Twisted Clifford action, reflections, and scalar kernel Lemma
- Uniqueness of the stable Clifford–Hopf decomposition Lemma
- The spin factor and the plus-quadratic Clifford convention Proposition
- Antiunitary AZ symmetry classes give Clifford extension problems Theorem
- Complex spinor modules and complete reducibility for Euclidean Spin Theorem
- Irreducible graded Clifford modules and real, complex, and quaternionic types Theorem
- Real and complex Clifford algebra classification with explicit signature Theorem
- Real Spin modules from the even Clifford algebra Theorem
- The Finite-Mode CAR Algebra Is a Full Matrix Algebra Theorem
- The graded tensor product for orthogonal sums of quadratic spaces Theorem
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
- Jean Gallier, Clifford Algebras, Clifford Groups, and a Generalization of the Quaternions: The Pin and Spin Groups, §1.2 (standard reference, not scraped)
- M. F. Atiyah, R. Bott, and A. Shapiro, Clifford Modules, Part I, §1 (standard reference, not scraped)