Lemma. The leading symbol is exterior [chevalley1954algebraic, II.1.6, pp. 41--42] [fcap-000H]
✍️source
changeForm_prod_map_ι_sub_prod_map_ι_mem_filtrationfiltrationLeadingTerm_apply_ιMulti
L∃∀N

    Retain the coordinate-free commutative-ring and module setting of Definition [fcap-000G], and assume that \(2\) is invertible in \(R\). This is TauCeti's extension of Chevalley's finite-basis, vector-space leading-symbol argument. For vectors \(v_1,\ldots ,v_n\in M\), the Clifford relation replaces an interchange by its alternating term plus a scalar contraction. Each contraction removes two generators. Consequently \[\iota (v_1)\cdots \iota (v_n) \equiv v_1\wedge \cdots \wedge v_n\pmod {F_{n-2}},\] where the right-hand side is read through the zero-form exterior model. In particular, the class of the Clifford word in \(F_n/F_{n-1}\) depends alternately on the vectors and is the leading exterior symbol.

    Proof. 

      Move a generator through the word using \[\iota (u)\iota (v)+\iota (v)\iota (u)=B_Q(u,v)1.\] The swapped word contributes the alternating sign, whereas the polar term has two fewer generators. Iterating separates the fully alternating word from terms in \(F_{n-2}\). Equivalently, changing from \(Q\) to the zero quadratic form changes a word only below its leading filtration degree.

      References

        Reference. The algebraic theory of spinors [chevalley1954algebraic]

        • 1954
        • Claude Chevalley
        @book{chevalley1954algebraic,
 title = {The Algebraic Theory of Spinors},
 author = {Chevalley, Claude},
 year = {1954},
 publisher = {Columbia University Press}
}

        Context

          The exterior shadow of a Clifford algebra [fcap-000F]

            The Clifford relation lowers word length by two. Filtering by word length therefore separates a word from its contraction terms: the highest-degree part is alternating, and the associated graded algebra is the exterior algebra. Reversal then distinguishes word order from parity, while orthogonality gives a scalar square for a volume word.

            § [ca-0001]

            Definition. Word-length filtration [chevalley1954algebraic, II.1.2 and II.1.6, pp. 40--42] [fcap-000G]
            filtrationfiltration_mul
            L∃∀N

              Chevalley constructs the classical filtration after choosing a finite basis of a vector space over a field. TauCeti's coordinate-free version below is defined for a quadratic form on a module over a commutative ring. The leading-symbol equivalences in Lemma [fcap-000H] and Theorem [fcap-000I] additionally assume that \(2\) is invertible.

              Let \(R\) be a commutative ring, let \(M\) be an \(R\)-module, and let \(Q:M\to R\) be a quadratic form. In the Clifford algebra \(\mathcal {C}\kern -2pt\ell (Q)\), define \(F_n\mathcal {C}\kern -2pt\ell (Q)\) to be the \(R\)-submodule spanned by all products of at most \(n\) generators: \[F_n\mathcal {C}\kern -2pt\ell (Q)=\operatorname {span}_R\left \{\iota (v_1)\cdots \iota (v_r):0\le r\le n\right \}.\] The empty product gives \(F_0\mathcal {C}\kern -2pt\ell (Q)=R1\). Concatenating words makes the filtration multiplicative; in fact, \[F_i\mathcal {C}\kern -2pt\ell (Q)\,F_j\mathcal {C}\kern -2pt\ell (Q)=F_{i+j}\mathcal {C}\kern -2pt\ell (Q).\] Thus multiplication descends to the successive quotients and makes \[\operatorname {gr}_F\mathcal {C}\kern -2pt\ell (Q)=\bigoplus _{n\ge 0}F_n\mathcal {C}\kern -2pt\ell (Q)/F_{n-1}\mathcal {C}\kern -2pt\ell (Q)\] a graded algebra, with \(F_{-1}\mathcal {C}\kern -2pt\ell (Q)=0\).

              Lemma. The leading symbol is exterior [chevalley1954algebraic, II.1.6, pp. 41--42] [fcap-000H]
              ✍️source
              changeForm_prod_map_ι_sub_prod_map_ι_mem_filtrationfiltrationLeadingTerm_apply_ιMulti
              L∃∀N

                Retain the coordinate-free commutative-ring and module setting of Definition [fcap-000G], and assume that \(2\) is invertible in \(R\). This is TauCeti's extension of Chevalley's finite-basis, vector-space leading-symbol argument. For vectors \(v_1,\ldots ,v_n\in M\), the Clifford relation replaces an interchange by its alternating term plus a scalar contraction. Each contraction removes two generators. Consequently \[\iota (v_1)\cdots \iota (v_n) \equiv v_1\wedge \cdots \wedge v_n\pmod {F_{n-2}},\] where the right-hand side is read through the zero-form exterior model. In particular, the class of the Clifford word in \(F_n/F_{n-1}\) depends alternately on the vectors and is the leading exterior symbol.

                Proof. 

                  Move a generator through the word using \[\iota (u)\iota (v)+\iota (v)\iota (u)=B_Q(u,v)1.\] The swapped word contributes the alternating sign, whereas the polar term has two fewer generators. Iterating separates the fully alternating word from terms in \(F_{n-2}\). Equivalently, changing from \(Q\) to the zero quadratic form changes a word only below its leading filtration degree.

                  Theorem. The graded pieces are exterior powers [chevalley1954algebraic, II.1.6, pp. 41--42] [fcap-000I]
                  gradedPieceEquivExteriorPowerfiltrationLeadingTerm_eq_filtrationGradedEquiv_symm
                  L∃∀N

                    Let \(R\), \(M\), and \(Q\) be as in Lemma [fcap-000H]. Chevalley's finite-dimensional field argument motivates the identification. TauCeti proves the following coordinate-free commutative-ring and module equivalence. For every \(n\ge 0\), the leading-symbol map gives \[F_n\mathcal {C}\kern -2pt\ell (Q)/F_{n-1}\mathcal {C}\kern -2pt\ell (Q)\simeq \bigwedge ^n_R M.\] At \(n=0\) this is the scalar equivalence \(F_0/0\simeq R=\bigwedge ^0_RM\). For \(n>0\), the inverse sends a decomposable exterior product to the class of the corresponding Clifford word.

                    The point of the quotient is that every contraction term has already fallen into a lower filtration step. Alternation is therefore exact in the graded piece even though it is not exact in the Clifford algebra itself.

                    Theorem. PBW equivalence with the exterior algebra [meinrenken2013clifford, Proposition 2.6, pp. 33--34] [fcap-000J]
                    associatedGradedEquivExterior
                    L∃∀N

                      Meinrenken's Proposition 2.6 assumes a finite-dimensional vector space over a characteristic-zero field. TauCeti proves the corresponding extension for an additive commutative group \(M\) with a module structure over a commutative ring \(R\), a quadratic form \(Q\) on \(M\), and invertible \(2\in R\). Under these hypotheses, the equivalences of Theorem [fcap-000I] respect multiplication of homogeneous classes and assemble into a graded-algebra equivalence \[\operatorname {gr}_F\mathcal {C}\kern -2pt\ell (Q)\simeq _{\mathrm {grAlg}}\bigwedge _R M.\] The class of a product of an \(i\)-word and a \(j\)-word is carried to the exterior product of their leading symbols in degree \(i+j\).

                      This is a PBW theorem for the Clifford filtration. It does not make \(\mathcal {C}\kern -2pt\ell (Q)\) and \(\bigwedge _RM\) isomorphic as algebras. The quadratic form survives in the lower-degree contraction terms of Clifford multiplication; only the associated graded multiplication forgets it.

                      Example. The degree-two symbol [chevalley1954algebraic, II.1.6, pp. 41--42] [fcap-000K]
                      filtrationLeadingTerm_apply_ιMulti
                      L∃∀N

                        Let \(R\), \(M\), and \(Q\) be as in Definition [fcap-000G], and assume \(2\) is invertible in \(R\), as in Lemma [fcap-000H]. For \(u,v\in M\), the degree-two leading-term map sends their exterior product to the class of the corresponding Clifford word. Writing that word as \[\iota (u)\iota (v) =\frac 12\bigl (\iota (u)\iota (v)-\iota (v)\iota (u)\bigr ) +\frac 12B_Q(u,v)1.\] The second summand belongs to \(F_0\), so it vanishes in \(F_2/F_1\). Thus \(u\wedge v\) maps to the class of \(\iota (u)\iota (v)\); equivalently, under the graded-piece equivalence, that class maps to \(u\wedge v\). This is the two-generator instance of Chevalley's leading-symbol calculation cited in the title. The surviving half-commutator is the Clifford bivector studied next; the scalar polar term is invisible to the leading symbol.

                        Remark. Basis proof and quotient proof [fcap-000L]

                          Chevalley's proof chooses a basis, proves that ordered Clifford monomials form a basis, and identifies the underlying vector space with the exterior algebra [chevalley1954algebraic, II.1.2 and II.1.6, pp. 40--42]. Panyushev uses the resulting stable filtration and exterior associated graded as standard representation-theoretic background [panyushev2001exterior, Section 2, p. 7].

                          The quotient construction above is TauCeti's coordinate-free commutative-ring and module extension of that finite-dimensional field proof. It builds each graded piece from the word-length submodule and its predecessor, handles degree zero separately, and then takes their direct sum. This is a change of packaging and generality, not a stronger claim about unfiltered Clifford multiplication.

                          Theorem. Scalar extension preserves the Clifford and exterior constructions [fcap-003V]
                          CliffordAlgebra.equivBaseChange
                          L∃∀N
                          exteriorAlgebraEquivBaseChange
                          L∃∀N

                            Changing the field need not require new generators or a new quadratic basis. Let \(L/K\) be a field extension with \(\operatorname {char}K\ne 2\), and let \((V,Q)\) be a finite-dimensional quadratic space, possibly degenerate. Its scalar extension is \(V_L=L\otimes _K V\) with quadratic form \(Q_L\) characterized by \(Q_L(a\otimes v)=a^2Q(v)\) and the extended polar form. There are canonical \(L\)-algebra isomorphisms \[\begin {aligned} \beta _Q:L\otimes _K\mathcal {C}\kern -2pt\ell _K(Q)&\longrightarrow \mathcal {C}\kern -2pt\ell _L(Q_L),\\ a\otimes \iota _Q(v)&\longmapsto a\,\iota _{Q_L}(1\otimes v),\\ \beta _\wedge :L\otimes _K\bigwedge _K V&\longrightarrow \bigwedge _L V_L,\\ a\otimes (v_1\wedge \cdots \wedge v_r)&\longmapsto a(1\otimes v_1)\wedge \cdots \wedge (1\otimes v_r). \end {aligned}\] The first preserves the word-length filtration and parity; the second preserves exterior degree. No nondegeneracy hypothesis or chosen basis is needed to define either map.

                            The Clifford statement is [chevalley1954algebraic, II.1.5, p. 41]. The proof below uses the universal property; applying it to the zero form gives the exterior algebra statement.

                            Proof. 

                              The assignment \(v\mapsto \iota _{Q_L}(1\otimes v)\) has square \(Q(v)1\). The universal property extends it to a \(K\)-algebra map; extending scalars gives \(\beta _Q\). For the inverse, take the \(L\)-linear map \[j:V_L\longrightarrow L\otimes _K\mathcal {C}\kern -2pt\ell _K(Q),\qquad j(a\otimes v)=a\otimes \iota _Q(v).\] The Clifford anticommutator is \(\iota _Q(v)\iota _Q(w)+ \iota _Q(w)\iota _Q(v)=B_Q(v,w)1\). Thus, for \(x=\sum _i a_i\otimes v_i\), \[j(x)^2=\left (\sum _i a_i^2Q(v_i)+ \sum _{i<j}a_ia_jB_Q(v_i,v_j)\right )1=Q_L(x)1.\] The same universal property therefore extends \(j\) to an \(L\)-algebra map in the opposite direction. Both composites fix scalars and vector generators, so they are identities. For \(Q=0\), this argument gives \(\beta _\wedge \). The two maps and their inverses preserve word length and parity because they send generators to generators.

                              Write \(C=\mathcal {C}\kern -2pt\ell _K(Q)\) and \(C_L=\mathcal {C}\kern -2pt\ell _L(Q_L)\), and denote the leading-symbol equivalences of Theorem [fcap-000I] by \(\sigma _K,\sigma _L\). Scalar extension and taking the exterior symbol commute:

                              Tensoring vector spaces preserves these filtration quotients. On each generator word, both paths give the exterior product of its extended vectors. Such words span every graded piece, so the square commutes.

                              For example, \(\beta _Q(1\otimes \iota _Q(v)^2)=Q(v)1\), whereas \((1\otimes v)\wedge (1\otimes v)=0\). The square compares associated graded multiplication. It does not turn the linear Clifford-to-exterior coordinates of Definition [fcap-0003] into an algebra map. Chevalley makes this product distinction immediately after II.1.5.

                              The marked declarations give the two algebra equivalences in the reverse direction. Mathlib allows arbitrary commutative base and extension rings with \(2\) invertible; TauCeti's exterior equivalence needs neither invertible two nor flatness. The symbol square above is the consequence proved here, using the existing leading-symbol equivalence. The separate Spin-lifting consequences remain in Theorem [fcap-003N] and Proposition [fcap-003O].

                              Theorem [ca-000C]Definition [ca-000E]

                              Example. Real structures in chosen complex coordinates [fcap-003W]

                                Why does the complex Clifford algebra forget a real signature, while its real vectors still remember it? Let \(V\) be a finite-dimensional real space with nondegenerate quadratic form \(Q\). Its complexification is the scalar extension \(V_{\mathbb C}=\mathbb C\otimes _{\mathbb R}V\). Complex conjugation on the first factor fixes \(V\) and induces the conjugate-linear algebra involution \[\sigma (z\otimes a)=\overline z\otimes a\] on \(\mathbb C\otimes _{\mathbb R}\mathcal {C}\kern -2pt\ell _{\mathbb R}(Q)\). It preserves product order and conjugates scalar coefficients; the grade reversion instead reverses product order and is complex-linear after scalar extension. A real structure on a complex vector space or algebra means a map with \(\sigma (\lambda v+\mu w)=\overline \lambda \sigma (v)+ \overline \mu \sigma (w)\) and \(\sigma ^2=1\), an algebra automorphism in the algebra case. The fixed algebra here is \(1\otimes \mathcal {C}\kern -2pt\ell _{\mathbb R}(Q)\): write an element uniquely as \(1\otimes a+i\otimes b\) with \(a,b\) real to check this.

                                For the underlying real module of \(\mathcal {C}\kern -2pt\ell _{\mathbb R}(Q)\), this coefficient map is TauCeti.tmulConj. Its involution law is TauCeti.tmulConj_involutive, and its fixed vectors are described by TauCeti.tmulConj_eq_self_iff. These supporting declarations concern the conjugate-linear involution and fixed vectors; multiplicativity and the coordinate comparisons below are the algebra calculations given here.

                                This is the conjugation construction in [meinrenken2013clifford, Section 2.2.6, p. 34]. Meinrenken's symmetric form is \(B=B_Q/2\), so his generator relation is \(uv+vu=2B(u,v)=B_Q(u,v)\). The following coordinate calculation applies that construction to the scalar-extension isomorphism of Theorem [fcap-003V].

                                Choose an orthogonal real basis \(e_1,\ldots ,e_n\) with \(Q(e_j)=1\) for \(j\le p\) and \(Q(e_j)=-1\) for \(j>p\), where \(n=p+q\). These are the signature signs of Convention [fcap-0011]. On \(\mathbb C^n\), put \(Q_0(z)=\sum _j z_j^2\), with coordinate vectors \(u_j\). The chosen complex isometry \[T(e_j)=\begin {cases}u_j&j\le p,\\i u_j&j>p\end {cases}\] induces \(\mathcal {C}\kern -2pt\ell (T):\mathcal {C}\kern -2pt\ell _{\mathbb C}(Q_{\mathbb C}) \simeq \mathcal {C}\kern -2pt\ell _{\mathbb C}(Q_0)\). Transporting \(\sigma \) through this map and Theorem [fcap-003V] gives \(\sigma _T\) on the standard complex algebra. On its generators, \[\sigma _T(\iota (u_j))=\begin {cases} \iota (u_j)&j\le p,\\-\iota (u_j)&j>p. \end {cases}\] Indeed, \(T^{-1}(u_j)=-i e_j\) for a negative direction, and conjugation sends this to \(i e_j\), whose image under \(T\) is \(-u_j\). The fixed real generators are consequently \(\iota (u_j)\) and \(i\iota (u_j)\) in the positive and negative directions, respectively.

                                Already in dimension one, the same complex algebra \(A=\mathbb C[u]/(u^2-1)\) has two different real structures: \[\begin {aligned} \sigma _+(z+wu)&=\overline z+\overline w u, & A^{\sigma _+}&=\mathbb R[ u]\simeq \mathbb R\oplus \mathbb R,\\ \sigma _-(z+wu)&=\overline z-\overline w u, & A^{\sigma _-}&=\mathbb R[iu]\simeq \mathbb C. \end {aligned}\] The first real-algebra isomorphism evaluates at \(u=1,-1\); the second uses \((iu)^2=-1\). Thus forgetting the real structure loses the distinction between \(\mathcal {C}\kern -2pt\ell (1,0)\) and \(\mathcal {C}\kern -2pt\ell (0,1)\). If a different complex isometry is \(T'=UT\), then \(\sigma _{T'}=\mathcal {C}\kern -2pt\ell (U)\sigma _T\mathcal {C}\kern -2pt\ell (U)^{-1}\). The real structure moves with the coordinates; it is not generally entrywise conjugation in every model.

                                The real-algebra identifications in this example are formalized as TauCeti.realCliffordOneZeroEquivProd and TauCeti.realCliffordZeroOneEquivComplex. These declarations identify the two real Clifford algebras; the comparison of their conjugations inside \(A\) is the calculation above.

                                Choosing the polarization data for a spinor carrier is a further choice. For \(Q(x,y)=x^2+y^2\), the complex isotropic lines \[W=\mathbb C(e_1+i e_2),\qquad W'=\mathbb C(e_1-i e_2)\] are complementary, and conjugation exchanges them. Their polar pairing is nonzero, so they give the split model after normalizing a dual basis. The carrier \(S=\bigwedge W\) uses \(W\) for creation and \(W'\) for contraction, as in Definition [fcap-001I]. Conjugation therefore maps this exterior space to \(\bigwedge W'\), rather than supplying a conjugation on \(S\) compatible with the same chosen operators. Comparing these carriers needs an additional intertwining map. This explains why the canonical real structure on the Clifford algebra alone does not choose a real structure on a particular spinor module. The creation/contraction construction is [chevalley1954algebraic, II.2.1--II.2.2, pp. 42--44].

                                Definition [ca-000J]

                                Lemma. Parity and reversal separate on bivectors [fcap-0021]
                                reverse_bivectorreverse_bivectorExterior
                                L∃∀N

                                  Let \(R\) be a commutative ring with invertible \(2\), let \(M\) be an \(R\)-module, and let \(Q\) be a quadratic form on \(M\). Write \(\alpha \) for the grading involution and \(\operatorname {rev}\) for reversal. For the half-commutator bivector of Convention [fcap-000N], \[\begin {aligned} \alpha (\beta _Q(u,v))&=\beta _Q(u,v),\\ \operatorname {rev}(\beta _Q(u,v))&=-\beta _Q(u,v). \end {aligned}\] The same reversal sign holds for every bivector in the image of \(\bigwedge _R^2 M\); reversal acts as minus the identity there.

                                  Chevalley defines the main antiautomorphism by reversing products while fixing generators [chevalley1954algebraic, Section 2.1, p. 38]. His parity decomposition identifies even exterior degree with the even Clifford part [chevalley1954algebraic, II.1.6, p. 42]. Those are finite-dimensional field-space conventions; the displayed bivector statement is Tau Ceti's commutative-ring extension.

                                  Proof. 

                                    Parity changes the sign of each generator, so it fixes a product of two. Reversal exchanges the order of those generators. Applied to the half-commutator, the exchange negates it. Linearity then gives the same sign on the exterior-square image CliffordAlgebra.reverse_bivectorExterior. The bivector is even CliffordAlgebra.bivector_mem_evenOdd_zero; on any even element reversal also agrees with Clifford conjugation \(x\mapsto x^*\), since parity is the identity there CliffordAlgebra.reverse_eq_star_of_mem_even.

                                    The same reversal and parity conventions determine the scalar norm signs and the distinction between even-unitary and Spin units in Remark [fcap-0028].

                                    Remark. Reverse norm signs and the Spin carrier [fcap-0028]

                                      Let \(R\) be a commutative ring, let \(M\) be an \(R\)-module, and let \(Q\) be a quadratic form on \(M\). Write \(\widehat v=\iota _Q(v)\) for a Clifford generator. Before imposing any invertibility condition, consider the two algebra-valued norm expressions \(N_{\mathrm {rev}}(x)=\operatorname {rev}(x)x\) and \(N_*(x)=x^*x\), where \(x^*=\operatorname {rev}(\alpha (x))\). Identifying a scalar with its image in the Clifford algebra gives \[\begin {aligned} N_{\mathrm {rev}}(\widehat v)&=Q(v), &N_*(\widehat v)&=-Q(v),\\ N_{\mathrm {rev}}(\widehat u\widehat v) &=\widehat v\widehat u\widehat u\widehat v =Q(u)Q(v), &N_*(\widehat u\widehat v)&=Q(u)Q(v). \end {aligned}\] Thus the two signs differ on one generator and agree on a product of two. More generally, reversal gives the product of the quadratic values on every vector word CliffordAlgebra.reverse_prod_map_ι_mul_prod_map_ι, and the two norm expressions agree on every even Clifford element CliffordAlgebra.star_mul_self_eq_reverse_mul_self_of_mem_even.

                                      For a Clifford unit \(x\), membership in the even-unitary carrier is equivalent to evenness together with \(N_{\mathrm {rev}}(x)=1\) CliffordAlgebra.evenUnitaryGroup.mem_iff_reverse_mul_self_eq_one. Those two conditions do not establish Lipschitz membership, which must be retained in the Spin criterion. Precisely, \[\operatorname {im}\bigl (\operatorname {Spin}(Q)\longrightarrow \operatorname {Cl}(Q)^\times \bigr ) =\operatorname {Lipschitz}(Q)\cap \operatorname {EvenUnitary}(Q)\] CliffordAlgebra.range_spinGroup_toUnits. Consequently, if \(Q(u)Q(v)=1\), then \(\widehat u\widehat v\) is an even product of Lipschitz vector units with reverse norm one, hence a Spin element CliffordAlgebra.ι_mul_ι_mem_spinGroup_of_norm_mul_norm_eq_one. This is an unquotiented scalar calculation. The passage to square classes, including the odd reflection sign and its cancellation on even products, is recorded separately in Theorem [fcap-0023].

                                      Chevalley obtains the same norm from what he calls the main antiautomorphism and records \(\lambda (v)=Q(v)\) and the paired values \(Q(u)Q(v)\) [chevalley1954algebraic, II.3.5--6, pp. 52--53]. His symbol \(\alpha \) in that passage denotes reversal, whereas \(\alpha \) in Lemma [fcap-0021] denotes the grading involution. Meinrenken calls reversal transposition, writes \(N(x)=x^\top x\), and defines Spin as its norm-one subgroup inside the special Clifford group [meinrenken2013clifford, Sections 2.2.6 and 3.1.1--2, pp. 34, 49--51]. His convention has \(Q(v)=B(v,v)\), so his \(B\) is the half-polar form \(b_Q\) of Convention [fcap-0027]. Both sources work in narrower finite-dimensional field settings; Meinrenken here assumes characteristic zero and a nondegenerate form. The formal identities linked above hold under the commutative-ring and module hypotheses stated here.

                                      Theorem. The square of an orthogonal Clifford volume word [fcap-0022]
                                      prod_map_ι_sq_scalar
                                      L∃∀N

                                        Let \(R\) be a commutative ring, \(M\) an \(R\)-module, and \(Q\) a quadratic form on \(M\). For a pairwise \(Q\)-orthogonal list \(\ell =(v_1,\ldots ,v_n)\), set \[\omega _\ell =\iota _Q(v_1)\cdots \iota _Q(v_n).\] Its square is the scalar \[\omega _\ell ^2 =(-1)^{\binom n2}\left (\prod _{i=1}^{n}Q(v_i)\right )1.\] The empty list gives \(\omega _\ell =1\). No basis, nondegeneracy, finite-dimensionality, or invertibility of \(2\) is required.

                                        Chevalley computes the corresponding square for an orthogonal basis of a nondegenerate even-dimensional quadratic space over a field of characteristic different from \(2\) [chevalley1954algebraic, Proof of II.2.3, p. 45]. His generator relation \(v_i^2=Q(v_i)1\) matches the convention above. Tau Ceti's list identity extends that calculation to arbitrary lengths and the stated commutative-ring setting.

                                        Proof. 

                                          Pairwise orthogonality gives \(\iota _Q(v_i)\iota _Q(v_j)=-\iota _Q(v_j)\iota _Q(v_i)\) for \(i\ne j\). Move each factor of the second copy of \(\omega _\ell \) next to its matching factor in the first copy. This takes \((n-1)+(n-2)+\cdots +1=\binom n2\) swaps. Each adjacent pair then contracts to \(\iota _Q(v_i)^2=Q(v_i)1\), giving the formula.

                                          Backlinks

                                            Example. The degree-two symbol [chevalley1954algebraic, II.1.6, pp. 41--42] [fcap-000K]
                                            filtrationLeadingTerm_apply_ιMulti
                                            L∃∀N

                                              Let \(R\), \(M\), and \(Q\) be as in Definition [fcap-000G], and assume \(2\) is invertible in \(R\), as in Lemma [fcap-000H]. For \(u,v\in M\), the degree-two leading-term map sends their exterior product to the class of the corresponding Clifford word. Writing that word as \[\iota (u)\iota (v) =\frac 12\bigl (\iota (u)\iota (v)-\iota (v)\iota (u)\bigr ) +\frac 12B_Q(u,v)1.\] The second summand belongs to \(F_0\), so it vanishes in \(F_2/F_1\). Thus \(u\wedge v\) maps to the class of \(\iota (u)\iota (v)\); equivalently, under the graded-piece equivalence, that class maps to \(u\wedge v\). This is the two-generator instance of Chevalley's leading-symbol calculation cited in the title. The surviving half-commutator is the Clifford bivector studied next; the scalar polar term is invisible to the leading symbol.

                                              Theorem. The graded pieces are exterior powers [chevalley1954algebraic, II.1.6, pp. 41--42] [fcap-000I]
                                              gradedPieceEquivExteriorPowerfiltrationLeadingTerm_eq_filtrationGradedEquiv_symm
                                              L∃∀N

                                                Let \(R\), \(M\), and \(Q\) be as in Lemma [fcap-000H]. Chevalley's finite-dimensional field argument motivates the identification. TauCeti proves the following coordinate-free commutative-ring and module equivalence. For every \(n\ge 0\), the leading-symbol map gives \[F_n\mathcal {C}\kern -2pt\ell (Q)/F_{n-1}\mathcal {C}\kern -2pt\ell (Q)\simeq \bigwedge ^n_R M.\] At \(n=0\) this is the scalar equivalence \(F_0/0\simeq R=\bigwedge ^0_RM\). For \(n>0\), the inverse sends a decomposable exterior product to the class of the corresponding Clifford word.

                                                The point of the quotient is that every contraction term has already fallen into a lower filtration step. Alternation is therefore exact in the graded piece even though it is not exact in the Clifford algebra itself.

                                                Definition. Word-length filtration [chevalley1954algebraic, II.1.2 and II.1.6, pp. 40--42] [fcap-000G]
                                                filtrationfiltration_mul
                                                L∃∀N

                                                  Chevalley constructs the classical filtration after choosing a finite basis of a vector space over a field. TauCeti's coordinate-free version below is defined for a quadratic form on a module over a commutative ring. The leading-symbol equivalences in Lemma [fcap-000H] and Theorem [fcap-000I] additionally assume that \(2\) is invertible.

                                                  Let \(R\) be a commutative ring, let \(M\) be an \(R\)-module, and let \(Q:M\to R\) be a quadratic form. In the Clifford algebra \(\mathcal {C}\kern -2pt\ell (Q)\), define \(F_n\mathcal {C}\kern -2pt\ell (Q)\) to be the \(R\)-submodule spanned by all products of at most \(n\) generators: \[F_n\mathcal {C}\kern -2pt\ell (Q)=\operatorname {span}_R\left \{\iota (v_1)\cdots \iota (v_r):0\le r\le n\right \}.\] The empty product gives \(F_0\mathcal {C}\kern -2pt\ell (Q)=R1\). Concatenating words makes the filtration multiplicative; in fact, \[F_i\mathcal {C}\kern -2pt\ell (Q)\,F_j\mathcal {C}\kern -2pt\ell (Q)=F_{i+j}\mathcal {C}\kern -2pt\ell (Q).\] Thus multiplication descends to the successive quotients and makes \[\operatorname {gr}_F\mathcal {C}\kern -2pt\ell (Q)=\bigoplus _{n\ge 0}F_n\mathcal {C}\kern -2pt\ell (Q)/F_{n-1}\mathcal {C}\kern -2pt\ell (Q)\] a graded algebra, with \(F_{-1}\mathcal {C}\kern -2pt\ell (Q)=0\).

                                                  Related

                                                    Definition. Word-length filtration [chevalley1954algebraic, II.1.2 and II.1.6, pp. 40--42] [fcap-000G]
                                                    filtrationfiltration_mul
                                                    L∃∀N

                                                      Chevalley constructs the classical filtration after choosing a finite basis of a vector space over a field. TauCeti's coordinate-free version below is defined for a quadratic form on a module over a commutative ring. The leading-symbol equivalences in Lemma [fcap-000H] and Theorem [fcap-000I] additionally assume that \(2\) is invertible.

                                                      Let \(R\) be a commutative ring, let \(M\) be an \(R\)-module, and let \(Q:M\to R\) be a quadratic form. In the Clifford algebra \(\mathcal {C}\kern -2pt\ell (Q)\), define \(F_n\mathcal {C}\kern -2pt\ell (Q)\) to be the \(R\)-submodule spanned by all products of at most \(n\) generators: \[F_n\mathcal {C}\kern -2pt\ell (Q)=\operatorname {span}_R\left \{\iota (v_1)\cdots \iota (v_r):0\le r\le n\right \}.\] The empty product gives \(F_0\mathcal {C}\kern -2pt\ell (Q)=R1\). Concatenating words makes the filtration multiplicative; in fact, \[F_i\mathcal {C}\kern -2pt\ell (Q)\,F_j\mathcal {C}\kern -2pt\ell (Q)=F_{i+j}\mathcal {C}\kern -2pt\ell (Q).\] Thus multiplication descends to the successive quotients and makes \[\operatorname {gr}_F\mathcal {C}\kern -2pt\ell (Q)=\bigoplus _{n\ge 0}F_n\mathcal {C}\kern -2pt\ell (Q)/F_{n-1}\mathcal {C}\kern -2pt\ell (Q)\] a graded algebra, with \(F_{-1}\mathcal {C}\kern -2pt\ell (Q)=0\).