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

                                            Theorem. Clifford algebras under scalar extension [fdip-000V]
                                            CliffordAlgebra.equivBaseChange
                                            L∃∀N

                                            • October 18, 2026

                                            Let \(R\) be a commutative ring in which \(2\) is a unit, \(M\) any \(R\)-module with quadratic form \(q\), and \(A\) any commutative \(R\)-algebra. Extend the symmetric half-polar form \[b(v,w)=\frac {q(v+w)-q(v)-q(w)}2\] to \(M_A=A\otimes _R M\), and let \(q_A\) be its diagonal. Thus \[q_A(a\otimes v)=a^2q(v),\] where \(q(v)\) on the right is mapped into \(A\). There is a canonical \(A\)-algebra isomorphism \[\begin {aligned} \beta _A:A\otimes _R\operatorname {Cl}_R(q) &\longrightarrow \operatorname {Cl}_A(q_A),\\ \beta _A(a\otimes \iota _q(v)) &=a\,\iota _{q_A}(1\otimes v). \end {aligned}\] No flatness, nondegeneracy, finite generation, or injectivity of \(R\to A\) is required. This extends the displayed field case of scalar extension to the declared commutative rings, using the same universal property.

                                            Proof. 

                                            • October 18, 2026

                                            The \(R\)-linear map \(v\mapsto \iota _{q_A}(1\otimes v)\) has square \(q(v)1\), so the universal property extends it to an \(R\)-algebra map out of \(\operatorname {Cl}_R(q)\). Central \(A\)-scalars then extend it to \(\beta _A\). The algebra structure on the tensor product uses \[(a\otimes c)(a'\otimes c')=aa'\otimes cc'.\] It is well-defined because the \(R\)-scalars are central.

                                            Conversely, the balanced bilinear assignment \((a,v)\mapsto a\otimes \iota _q(v)\) gives an \(A\)-linear map \[j:M_A\longrightarrow A\otimes _R\operatorname {Cl}_R(q).\] Write \(\iota =\iota _q\) and let \[\begin {aligned} B_q(v,w)&=q(v+w)\\ &\quad -q(v)-q(w)\\ &=2b(v,w) \end {aligned}\] be the full polar form. The defining square relation gives \[\iota (v)\iota (w)+\iota (w)\iota (v)=B_q(v,w)1.\] For an arbitrary finite sum \(x=\sum _i a_i\otimes v_i\), write \(w_i=\iota (v_i)\). Then \[\begin {aligned} j(x)^2 &=\sum _i a_i^2\otimes w_i^2\\ &+\sum _{i<j}a_i a_j\otimes (w_iw_j+w_jw_i)\\ &=\Bigl (\sum _i a_i^2q(v_i)\\ &\quad +\sum _{i<j}a_i a_j B_q(v_i,v_j)\Bigr )1\\ &=q_A(x)1. \end {aligned}\] Every tensor is such a finite sum; the cross terms are part of the square condition. Thus \(j\) extends to an \(A\)-algebra map in the opposite direction. Both composites fix scalars and vector generators. In the tensor-product algebra, \(a\otimes 1\) and \(1\otimes \iota (v)\) generate; in the other algebra, the vectors \(\iota _{q_A}(x)\) and scalars generate. The composites are therefore identities.

                                            Mathlib's marked equivalence has the reverse direction, \[\operatorname {Cl}_A(q_A) \simeq A\otimes _R\operatorname {Cl}_R(q).\] Its inverse is \(\beta _A\), and CliffordAlgebra.ofBaseChange_tmul_ι gives the displayed generator formula. QuadraticForm.baseChange constructs \(q_A\); its QuadraticForm.baseChange_tmul computes pure tensors. These declarations have exactly the commutative-ring and invertible-two hypotheses above. The marker concerns the generic algebra equivalence, not the arithmetic domain calculations or the sheaf multiplication below.

                                            Scalar extension is compatible with a further commutative algebra \(A\to B\). Identify \[\begin {aligned} B\otimes _A(A\otimes _R M)&\longrightarrow B\otimes _R M,\\ b\otimes (a\otimes v)&\longmapsto ba\otimes v. \end {aligned}\] The inverse inserts \(1\) in the middle tensor factor. Under this identification the direct and successive Clifford maps both send \(b\otimes (a\otimes \iota _q(v))\) to \(ba\,\iota _{q_B}(1\otimes v)\). These elements and scalars generate, proving equality of the algebra maps. TauCeti's QuadraticForm.baseChangeBaseChange uses the inverse identification, from direct to successive extension. With compatible \(R\)- and \(A\)-algebra structures on \(B\), its CliffordAlgebra.ofBaseChangeAux_baseChange states the same compatibility in that direction.

                                            For an \(R\)-linear form-preserving map \(P:M\to M\), put \(P_A(a\otimes v)=a\otimes Pv\). The two orders of applying \(\beta _A\) and the induced Clifford map both take \(a\otimes \iota _q(v)\) to \(a\,\iota _{q_A}(1\otimes Pv)\). Generation again proves equivariance. In particular the arithmetic half-turn and its \(C_2\) action commute with every allowed scalar extension.

                                            Apply this to \(C=\operatorname {Cl}_{R_q}(q)\) on the arithmetic base \(X_q\). Write \(\mathcal O_{X_q}\) for its structure sheaf: regular functions on \(D_{X_q}(g)\) form \((R_q)_g\). The associated module sheaf \(\widetilde C\) has \[\Gamma (D_{X_q}(g),\widetilde C) =C_g\simeq (R_q)_g\otimes _{R_q}C.\] Its restriction maps are the localization maps; compatible local sections glue uniquely. This construction and the standard-open formula are [stacks2017stacks, Section 26.5 and Lemma 26.5.4], Tag 01HR. Mathlib's AlgebraicGeometry.tilde, with its standard-open localized-module instance, supplies the underlying module sheaf. It does not by itself give the algebra structure.

                                            Multiplication and unit on a standard open are \[\frac {c}{g^m}\frac {d}{g^n} =\frac {cd}{g^{m+n}},\qquad 1=\frac 11.\] The denominators are central, so these operations are well-defined even though \(C\) need not be commutative. Restriction maps preserve them. On an arbitrary open, cover by standard opens and multiply the restrictions of two sections. The products agree on overlaps, so the module-sheaf axiom glues them uniquely; the same argument glues the unit. Associativity, additivity, the unit law and central \(\mathcal O_{X_q}\) action hold locally and hence globally. Thus \(\widetilde C\) is a sheaf of unital associative \(\mathcal O_{X_q}\)-algebras. No spectrum of the noncommutative algebra \(C\) is taken.

                                            The isomorphisms \(\beta _{(R_q)_g}\) identify these standard-open sections with \[\operatorname {Cl}_{(R_q)_g}(q_g).\] Scalar-tower compatibility makes the identifications commute with restrictions. This constructs the Clifford algebra sheaf of \(\mathcal O_{X_q}^4\) with matrix \(Q\). The half-turn acts on every localization by the same generator formula and commutes with restrictions, giving a \(C_2\) action on the sheaf. Restricting to \(X_{\mathrm {elim}}\) or \(X_{\mathrm {obs}}\) uses exactly these base-change maps.

                                            At the real specialization \(t=1\), put \(q_1(x)=x^TQ(1)x\) and let \(c_i=\iota _{q_1}(\delta _i)\) with the coordinate notation of the configuration Clifford algebra. Then \[c_i^2=3\,1,\qquad c_ic_j+c_jc_i=2Q(1)_{ij}\,1.\] The map \(\beta _{\mathbb R}\) identifies these relations with \(\mathbb R\otimes _{R_q}C\); direct evaluation or evaluation through either localization gives the same algebra and action. This evaluation is not injective: it kills the nonzero element \(t-1\) of \(R_q\). The isomorphism requires no injectivity. The effective rank-two form has its own Clifford algebra on \(X_{\mathrm {elim}}\); it is separate from this rank-4 construction.

                                            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]

                                              Definition. Rational diagonal subgroups [fcap-004K]

                                                Let \(Q\) be a nondegenerate quadratic form on a finite-dimensional rational space \(V\), and let \(U\) be a compatible compact-open reference tuple. For \(G=O,SO,\operatorname {Spin}\), write \(G(Q)\) for the rational group, \(g_p\) for the scalar extension of \(g\in G(Q)\) to \(\mathbb Q_p\), and \(g_\infty \) for its extension to \(\mathbb R\). Spin always means the actual vector-generated even reverse-norm-one carrier. The rational diagonal homomorphisms are \[\begin {aligned} \delta _f^G:G(Q)&\longrightarrow G_f(U), &g&\longmapsto (g_p)_p,\\ \delta _{\mathbb A}^G:G(Q)&\longrightarrow G_{\mathbb A}(U), &g&\longmapsto (g_\infty ,(g_p)_p),\\ \delta _R^G:G(Q)&\longrightarrow G_f^R(U), &g&\longmapsto (g_p)_{p\notin R}, \end {aligned}\] where \(R\) is any set of rational primes. The targets are the finite, full and away groups of Definition [fcap-004F], Definition [fcap-004H] and Definition [fcap-004G]. Their images are the corresponding rational diagonal subgroups.

                                                For O and Spin, the tuple axioms put each rational point in its reference subgroup at all but finitely many primes. For SO the same assertion follows from \(U_p^{SO}=i_p^{-1}(U_p^O)\), because determinant commutes with scalar extension. Thus the finite tuples are restricted. Deleting coordinates preserves this property, and the real factor imposes no reference condition. Scalar extension preserves products and identities, proving the homomorphism assertions.

                                                For the hyperbolic form \(Q(x,y)=xy\), use the standard-basis references. The matrix \(g=\operatorname {diag}(2,1/2)\) gives a rational SO diagonal. Its finite components are integral except at \(2\), as computed in Proposition [fcap-004D]. The real component is the same rational matrix viewed over \(\mathbb R\). Deleting the \(2\)-coordinate puts its away image in the product of the remaining reference subgroups.

                                                The finite and full diagonals are injective. The away diagonal is injective whenever at least one prime lies outside \(R\); in particular this holds for finite \(R\). If every prime is removed, its target is the singleton group, so the away map is injective only when \(G(Q)\) is itself trivial.

                                                Proof. 

                                                  Scalar extension to any one retained completion detects a rational O or SO element: in a rational basis, equality of the extended matrices implies equality of every rational entry, because the field map is injective. For Spin, the Clifford scalar-extension isomorphism of Theorem [fcap-003V] identifies its underlying Clifford map with \[\mathcal {C}\kern -2pt\ell _{\mathbb Q}(Q)\longrightarrow L\otimes _{\mathbb Q}\mathcal {C}\kern -2pt\ell _{\mathbb Q}(Q), \qquad c\longmapsto 1\otimes c,\] where \(L=\mathbb R\) or \(\mathbb Q_p\). This map is injective: the extension of a rational vector-space basis is an \(L\)-basis, so zero extended coefficients force every original coefficient to vanish. Restricting to the actual Spin carrier preserves injectivity. Equality of diagonal tuples therefore implies equality at one completion and hence equality of their rational arguments. The finite product retains, for example, the prime \(2\); the full product also retains the real place. The away argument requires the stated nonempty complement. The empty product is a singleton.

                                                  The diagonals commute with the component maps \(\operatorname {Spin}\to SO\to O\) of Proposition [fcap-004J]. At each place this is the scalar-extension action identity of Theorem [fcap-003N]; for SO to O it is the equality of underlying matrices. The full-to-finite projection and coordinate restriction satisfy \[\pi _f\delta _{\mathbb A}^G=\delta _f^G, \qquad r_R\delta _f^G=\delta _R^G.\] These are equalities of homomorphisms, with no topology assigned to \(G(Q)\). If the rational domain is given the discrete topology, the maps are continuous; injectivity alone does not make a map a topological embedding.

                                                  The rational-point diagonal in classical affine full adelic points is discussed in [conrad2011adelic, Example 2.3, p. 3]. Here restricted membership follows directly from the chosen tuple axioms. TauCeti constructs the finite diagonals in TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicOrthogonalDiagonal, TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalDiagonal and TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDiagonal. The full orthogonal construction is TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicOrthogonalDiagonal; the away injectivity condition is explicit in TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpecialOrthogonalDiagonal_injective. The Spin scalar-extension input is CliffordAlgebra.spinGroupBaseChange_injective, whose faithful, flat scalar-extension hypotheses hold for these fields. The SO and Spin full and away maps use the same construction.

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