Theorem. Scalar extension preserves the Clifford and exterior constructions [fcap-003V]
✍️source
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]

      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]
              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]
                          ✍️source
                          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

                                            Lemma. Opposite Lorentz signatures share an even-algebra action dictionary [fcap-003Z]

                                              Keep the Pauli convention of Example [fcap-002L]: \(Q_{1,3}(v)=t^2-x_1^2-x_2^2-x_3^2\), \(A_j=e_0e_j\), and \(\Psi (A_j)=\sigma _j\). For \(Q_{3,1}(y)=y_0^2+y_1^2+y_2^2-y_3^2\), write \(f_0,\ldots ,f_3\) for the coordinate generators. The real linear bijection \[T(t,x_1,x_2,x_3)=(-x_2,x_1,-x_3,t)\] satisfies \(Q_{3,1}(Tv)=-Q_{1,3}(v)\). There is a real algebra equivalence \[E:\mathcal {C}\kern -2pt\ell ^+(Q_{1,3})\longrightarrow \mathcal {C}\kern -2pt\ell ^+(Q_{3,1}), \qquad E(vw)=-T(v)T(w).\] It preserves reversion and restricts to an equivalence of the actual Spin groups. Their vector actions satisfy \[T(svs^{-1})=E(s)T(v)E(s)^{-1}.\]

                                              For the construction, complexify and send \(v\mapsto iT(v)\). Its square is \(Q_{1,3}(v)\), so the Clifford universal property gives an algebra map. On an even word of length \(2k\) its value is \((-1)^kT(v_1)\cdots T(v_{2k})\), which is real. This defines \(E\) by scalar extension as in Theorem [fcap-003V]. The reverse construction sends \(w\mapsto iT^{-1}(w)\); the two composites negate generators and therefore fix every even word. Reversing an even word commutes with \(E\). The dimension-four carrier lemma Lemma [fcap-002J] now identifies the reverse-norm-one even units on both sides, so \(E\) and its inverse restrict to the stated actual groups. Applying the complex map to \(svs^{-1}\) and cancelling \(i\) proves the action identity. This is the sign-transfer mechanism used for compact forms in Proposition [fcap-0039], with the additional coordinate change \(T\).

                                              The algebraic construction is also the composite of sign scaling and the isometry \(T:(-Q_{1,3})\to Q_{3,1}\). TauCeti's general scaling formula at the unit \(-1\) TauCeti.CliffordAlgebra.evenEquivEvenSMul_ι, its reversion compatibility TauCeti.CliffordAlgebra.evenEquivEvenSMul_reverseEven, and the isometry formula CliffordAlgebra.evenEquivOfIsometry_ι provide these three component statements. The displayed \(T\) and its Spin-action dictionary are the explicit specialization proved here.

                                              Let \(\Phi :\mathcal {C}\kern -2pt\ell ^+(Q_{3,1})\to M_2(\mathbb C)\) be TauCeti's concrete matrix equivalence. Its bilinear-generator formula TauCeti.realCliffordThreeOneEvenEquivComplexMatrix_ι gives \[\begin {aligned} \Phi (f_0f_3)&=-\sigma _2,&\Phi (f_1f_3)&=\sigma _1,& \Phi (f_2f_3)&=-\sigma _3,\\ \Phi (f_0f_1)&=i\sigma _3,&\Phi (f_0f_2)&=i\sigma _1,& \Phi (f_1f_2)&=i\sigma _2. \end {aligned}\] Since \(T(e_0)=f_3\), \(T(e_1)=f_1\), \(T(e_2)=-f_0\), and \(T(e_3)=-f_2\), these formulas give \(\Phi (E(A_j))=\sigma _j\). The \(A_j\) generate the even algebra, hence \(\Phi \circ E=\Psi \). Also \(E(e_0e_1e_2e_3)=f_0f_1f_2f_3\), whose matrix is \(-i1\). Thus the Pauli group equivalence agrees, through \(E\), with TauCeti.realSpinThreeOneEquivSpecialLinear. This dictionary concerns the even algebras and their Spin actions; the full real Clifford algebras retain their different signature types.

                                              Theorem [ca-000C]Definition [ca-000J]Definition [spin-000O]

                                              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]

                                                Related

                                                  Definition. Exterior algebra [wieser2022formalizing] [ca-000E]
                                                  ExteriorAlgebra
                                                  L∃∀N

                                                    An Exterior algebra over \(M\) is the Clifford algebra \(\mathcal {C}\kern -2pt\ell (Q)\) where \(Q(m) = 0\) for all \(m \in M\).

                                                    Proposition. Spin lifts over a quadratic extension [fcap-003O]

                                                      Keep the quadratic-space hypotheses of Theorem [fcap-003N]. Let \(d\in K^\times \) be nonsquare, put \(L=K(\sqrt d)\), and let \(\sigma \) be its nontrivial \(K\)-automorphism. The square-class map has kernel \[\ker j=\{1,[d]_K\}.\] Consequently, for \(g\in SO(V,Q)\), \[g_L\text { has a Spin lift} \quad \Longleftrightarrow \quad \nu _Q(g)\in \{1,[d]_K\}.\] The trivial class already gives a lift over \(K\). If \(\nu _Q(g)=[d]_K\), the two lifts over \(L\) are exchanged by \(\sigma \); neither is the scalar extension of a \(K\)-defined Spin element.

                                                      Proof. 

                                                        Suppose \(a\in K^\times \) becomes a square in \(L\). Write \[a=(u+v\sqrt d)^2=u^2+dv^2+2uv\sqrt d, \qquad u,v\in K.\] The basis \(1,\sqrt d\) and characteristic different from two give \(uv=0\). If \(v=0\), then \(a=u^2\); if \(u=0\), then \(a=dv^2\). The nonzero remaining coefficient shows that \([a]_K\) is respectively \(1\) or \([d]_K\). Both classes become squares in \(L\), and they are distinct because \(d\) is nonsquare. This proves the kernel formula; Theorem [fcap-003N] gives the criterion for \(g_L\).

                                                        Now assume \(\nu _Q(g)=[d]_K\). By Proposition [fcap-002D], take a Lipschitz lift \(x\) of \(g\); determinant parity makes it even. Its reverse norm is \(db^2\) for some \(b\in K^\times \). Replacing \(x\) by \(x/b\) preserves its action and makes \(N_{\mathrm {rev}}(x)=d\). In the extended Clifford algebra set \[s=\frac {c(x)}{\sqrt d}.\] Scalar units are Lipschitz and even by Proposition [fcap-002D]. Thus \(s\) is even and Lipschitz, and \[N_{\mathrm {rev}}(s)=\frac {d}{(\sqrt d)^2}=1.\] The carrier criterion Remark [fcap-0028] places \(s\) in the actual \(\operatorname {Spin}(Q_L)\), and scalar normalization leaves its vector action equal to \(g_L\). Any other Spin lift differs from \(s\) by a scalar unit, by the Lipschitz action kernel over \(L\). Norm one forces that scalar's square to be one, so all lifts are precisely \(s\) and \(-s\).

                                                        The coefficient automorphism \(\sigma \) acts semilinearly on \(\mathcal {C}\kern -2pt\ell (Q_L)\): it fixes each extended generator and sends \(\sqrt d\) to \(-\sqrt d\). In particular it fixes \(c(x)\) and gives \[\sigma (s)=-s,\qquad \sigma (-s)=s.\] These elements are distinct because \(s\) is a unit and the characteristic is not two. Every Clifford element obtained by extending coefficients from \(K\) is fixed by \(\sigma \). Neither lift can therefore come from \(\operatorname {Spin}(Q)\), in agreement with its nontrivial spinor-norm obstruction.

                                                        For an explicit rational example, take \(K=\mathbb Q\) and \[Q(ae+bf)=a^2+2b^2,\qquad g=-\operatorname {Id}=r_e r_f.\] Here \(e^2=1\), \(f^2=2\), and \(ef=-fe\). Thus \(x=ef\) satisfies \[\operatorname {rev}(x)x=feef=2,\qquad x^2=efef=-2,\] and \(\nu _Q(g)=[2]_{\mathbb Q}\) is nontrivial. Over \(L=\mathbb Q(\sqrt 2)\), however, \[s=\frac {ef}{\sqrt 2},\qquad N_{\mathrm {rev}}(s)=1,\qquad s^2=-1.\] Its vector action is still \(-\operatorname {Id}\). The two Spin lifts \(s,-s\) are interchanged by conjugating \(\sqrt 2\); the rational orthogonal transformation acquires lifts without either lift becoming rational.

                                                        Theorem. Spinor norms commute with extension of scalars [fcap-003N]

                                                          Let \(L/K\) be an extension of fields of characteristic different from two. Let \(V\) be a positive-dimensional finite-dimensional \(K\)-space, and let \(Q\) be nondegenerate. Set \(V_L=L\otimes _K V\), with extended form \(Q_L\), and write \[j:K^{\times }/(K^\times )^2\longrightarrow L^{\times }/(L^\times )^2, \qquad j([a]_K)=[a]_L.\] For \(g\in O(V,Q)\), scalar extension gives \(g_L(a\otimes v)=a\otimes g(v)\). Then \[\nu _{Q_L}^O(g_L)=j\bigl (\nu _Q^O(g)\bigr ).\] In particular, for \(g\in SO(V,Q)\), \[\nu _{Q_L}(g_L)=j\bigl (\nu _Q(g)\bigr ),\] and \(g_L\) has a Spin lift exactly when \(j(\nu _Q(g))=1\).

                                                          Proof. 

                                                            A Gram matrix for the unhalved polar form \(B_Q\) has nonzero determinant. Its determinant remains nonzero under the field embedding, so \(Q_L\) is nondegenerate. For \(Q(v)\ne 0\), the reflection formula is \[r_v(x)=x-\frac {B_Q(x,v)}{Q(v)}v.\] Since \(Q_L(1\otimes v)=Q(v)\) and the polar form extends by \(L\)-bilinearity, this formula on pure tensors gives \((r_v)_L=r_{1\otimes v}\). Cartan--Dieudonne writes any orthogonal \(g\) as \(r_{v_1}\cdots r_{v_k}\). The reflection values from Proposition [fcap-002D] therefore give \[\begin {aligned} \nu _{Q_L}^O(g_L) &=\left [\prod _{i=1}^k Q_L(1\otimes v_i)\right ]_L\\ &=j\left (\left [\prod _{i=1}^k Q(v_i)\right ]_K\right ) =j\bigl (\nu _Q^O(g)\bigr ). \end {aligned}\] Determinants also extend, so restricting to \(SO\) proves the second identity. Apply the image/kernel theorem Theorem [fcap-0023] over \(L\) to obtain the lifting criterion.

                                                            The Clifford map \(c:\mathcal {C}\kern -2pt\ell (Q)\to \mathcal {C}\kern -2pt\ell (Q_L)\) sends \(\iota _Q(v)\) to \(\iota _{Q_L}(1\otimes v)\). It preserves parity, reversal and products, and carries each nonisotropic vector unit to a nonisotropic vector unit. Thus it restricts to a map of the actual Spin carriers, and their vector actions satisfy \[q_L(c(s))=(q_K(s))_L\qquad (s\in \operatorname {Spin}(Q)),\] where \(q_K\) and \(q_L\) denote the Spin projections. Indeed, apply \(c\) to the conjugation identity on every vector generator. A lift defined over \(K\) therefore remains a lift over \(L\); the next proposition explains how additional lifts can appear when \(j\) kills a nontrivial square class.

                                                            [chevalley1954algebraic, Section 2.7, pp. 60--61] describes the Clifford extension, compatibility with the main antiautomorphism, and the group/vector-action inclusions in even dimension. His main antiautomorphism is reversal. The reflection proof above gives the stated naturality in every positive dimension, using the reverse-norm convention of Proposition [fcap-002D].

                                                            TauCeti proves the orthogonal and special-orthogonal identities in CliffordAlgebra.orthogonalSpinorNorm_orthogonalGroupBaseChange and CliffordAlgebra.spinorNorm_specialOrthogonalGroupBaseChange under the field, finite-dimensionality, nondegeneracy and invertibility-of-two hypotheses. The commuting Spin-action square is CliffordAlgebra.spinToSpecialOrthogonal_baseChange; its more general input is a finite free module over a commutative ring with two invertible.

                                                            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. Transported exterior-basis coordinates [wieser2024formalizing, 9.3.5] [fcap-0003]

                                                                Let \(R\) be a commutative ring in which \(2\) is invertible, let \(M\) be an \(R\)-module, and choose a basis \(b\) indexed by a linearly ordered type. Write \(E_b(s)\) for the exterior-basis vector indexed by a finite subset \(s\). For a quadratic form \(Q\), the Mathlib linear equivalence CliffordAlgebra.equivExterior from \(\mathcal {C}\kern -2pt\ell (Q)\) to \(\bigwedge _R M\) gives a coordinate basis \[B_{Q,b}(s) = \operatorname {equivExterior}(Q)^{-1}(E_b(s)).\] This basis is transported through a linear equivalence. It does not say that the equivalence preserves multiplication or that Clifford multiplication becomes exterior multiplication. The basis-free construction is developed in [wieser2022formalizing].

                                                                The exterior equivalence is treated in [wieser2024formalizing, 9.3.5].

                                                                Two calculations anchor the choice. The empty subset maps to the scalar unit, \[B_{Q,b}(\varnothing ) = 1,\] and a singleton maps to the corresponding Clifford generator, \[B_{Q,b}(\{i\}) = \iota _Q(b(i)).\] These are module-level identities: they determine the first two coordinate types but do not determine multiplication of arbitrary coordinates.

                                                                For subsets with several elements, a coordinate formula additionally needs an ordering convention and its attendant signs. No such convention is implicit in the transported basis.

                                                                Theorem. Universal property [wieser2022formalizing] [ca-000C]
                                                                CliffordAlgebra.ι_comp_liftCliffordAlgebra.lift_unique
                                                                L∃∀N

                                                                  Given \(f : M \to _{l[R]} A\), which is Clifford, \(F = \operatorname {lift} f\) (denoted \(\bar {f}\) in some literatures), we have:

                                                                  1. \(F \circ \iota = f\), i.e. the following diagram commutes:

                                                                  2. \(\operatorname {lift}\) is unique, i.e. given \(G : \mathcal {C}\kern -2pt\ell (Q) \to _{a} A\), we have: \[ G \circ \iota = f \iff G = \operatorname {lift} f\]

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