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 2 and Theorem 3 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\).

Retain the coordinate-free commutative-ring and module setting of Definition 1, 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.

Let \(R\), \(M\), and \(Q\) be as in Lemma 2. 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.

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 3 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.

Let \(R\), \(M\), and \(Q\) be as in Definition 1, and assume \(2\) is invertible in \(R\), as in Lemma 2. 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.

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.

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.

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 3 by \(\sigma _K,\sigma _L\). Scalar extension and taking the exterior symbol commute:

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].

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 7.

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 7 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].

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.

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

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 9 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.

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.