Polarization and the exterior spinor model [fcap-001G]
✍️source

    A polarization turns Clifford generators into creation, contraction, and parity operators on an exterior algebra. The resulting Clifford action has two group restrictions and receives every orthogonal Lie action through the quadratic Clifford realization.

    Write \(S=\bigwedge _K W\) for the exterior carrier and \(\rho :\mathcal {C}\kern -2pt\ell (Q)\to \operatorname {End}(S)\) for its Clifford action. Let \(\mathfrak g\) be an external Lie algebra with an orthogonal action \(\theta :\mathfrak g\to \mathfrak {so}(V,Q)\). The diagram records the induced Lie action at the top and the Pin and Spin restrictions of \(\rho \) below.

    § [ca-0001]

    Definition 1. Polarization data and its carrier [chevalley1954algebraic, II.2.1--II.2.2, pp. 42--44] [fcap-001H]
    SpinPolarizationData
    L∃∀N

      Let \(K\) be a commutative ring, let \(V\) be a \(K\)-module, and let \(Q\) be a quadratic form. Polarization data consists of isotropic submodules \(W,W'\subseteq V\), an orthogonal remainder \(L\), and a linear equivalence \[(W\oplus W')\oplus L\simeq V.\] The polar form identifies \(W'\) with \(W^*\); the pairing is separating in both variables. A coordinate \(\ell :L\to K\) is injective and satisfies \(\ell (z)^2=Q(z)\). Thus \(L\) is an orthogonal remainder equipped with an injective coordinate. Over a field it is at most one-dimensional; it vanishes in the classical even split model. The carrier of the exterior spinor model is \[S=\bigwedge _K W.\]

      Chevalley treats complementary totally singular subspaces in the split, even-dimensional field case. Meinrenken uses the equivalent Lagrangian model \(V=F^*\oplus F\) [meinrenken2013clifford, Section 3.2.2, Proposition 3.5, pp. 56--57]. The packaged remainder and commutative-ring hypotheses are TauCeti's stated generalization.

      Definition 2. Creation, contraction, and the line operator [meinrenken2013clifford, Section 3.2.2, Proposition 3.5, p. 57] [fcap-001I]
      wedgecontractlineOperator
      L∃∀N

        For \(x\in W\), creation is exterior multiplication \[\varepsilon _x(s)=x\wedge s.\] For \(y\in W'\), contraction is the degree-\(-1\) operator \(\iota _y\) associated with the functional \(x\mapsto B_Q(x,y)\). Finally, if \(z\in L\), its operator is \[\lambda _z=\ell (z)\,\alpha ,\] where \(\alpha \) is parity: it is \(+1\) on even exterior degree and \(-1\) on odd exterior degree. Chevalley's formulas identify the first two operators as left Clifford multiplication on the minimal ideal model [chevalley1954algebraic, II.2.2, pp. 43--44].

        Lemma 3. The polarized Clifford relation [meinrenken2013clifford, Section 3.2.1, pp. 54--55] [fcap-001J]
        contract_wedgecliffordOperator_sq
        L∃∀N

          Creation and contraction satisfy \[\iota _y\varepsilon _x+\varepsilon _x\iota _y =B_Q(x,y)\operatorname {id}_S.\] Creation and contraction each square to zero. Parity anticommutes with both, while \(\lambda _z^2=Q(z)\operatorname {id}_S\). Consequently the operator \(c(v)\) assembled from the three polarization coordinates obeys \[c(v)^2=Q(v)\operatorname {id}_S.\] This is the quadratic form of the usual polarized anticommutation relation \(c(v)c(w)+c(w)c(v)=B_Q(v,w)\). Meinrenken states the latter as the defining condition for a Clifford module.

          Theorem 4. The exterior Clifford action [meinrenken2013clifford, Section 3.2.2, Proposition 3.5, p. 57] [fcap-001K]
          spinAction
          L∃∀N

            The square relation of Lemma 3 extends uniquely to an algebra homomorphism \[\rho :\mathcal {C}\kern -2pt\ell (Q)\longrightarrow \operatorname {End}_K(S).\] On the three summands it is determined by \[\rho (\iota (x))s=x\wedge s,\qquad \rho (\iota (y))s=\iota _y(s),\qquad \rho (\iota (z))s=\ell (z)\alpha (s).\] The corresponding formalized equations are TauCeti.spinAction_ι_wedge, TauCeti.spinAction_ι_contract, and TauCeti.spinAction_ι_lineOperator. Chevalley's split even-dimensional model has no remainder term; the third formula is TauCeti's odd-line extension of that construction.

            Theorem 5. Creation and contraction generate all endomorphisms [meinrenken2013clifford, Section 3.2.4, Theorem 3.3, pp. 59--60] [fcap-001L]
            creation_contraction_adjoin_eq_topspinAction_surjective
            L∃∀N

              Assume that \(W\) is finite and free over the commutative ring \(K\). The subalgebra of \(\operatorname {End}_K(\bigwedge W)\) generated by all creation operators and all contractions is the whole endomorphism algebra. Since the polar pairing identifies \(W'\) with \(W^*\), these generators lie in the image of the exterior Clifford action. Hence \[\rho :\mathcal {C}\kern -2pt\ell (Q)\twoheadrightarrow \operatorname {End}_K(\bigwedge W)\] is surjective.

              Meinrenken proves generation first in rank one by four matrix units and then by tensor decomposition. Over a split field he combines surjectivity with a dimension calculation to obtain an isomorphism and irreducibility. TauCeti formalizes the generation and surjectivity statements over a finite free module. This card does not claim that \(S\) is irreducible, or that \(\rho \) is injective.

              Definition 6. The Spin and Pin representations [meinrenken2013clifford, Section 3.2.1, pp. 55--56] [fcap-001M]
              spinReppinRep
              L∃∀N

                The groups \(\operatorname {Spin}(Q)\) and \(\operatorname {Pin}(Q)\) consist of units in the Clifford algebra. Restricting the action \(\rho \) of Theorem 4 along these two inclusions gives representations on the same exterior carrier: \[\operatorname {spinRep}:\operatorname {Spin}(Q)\longrightarrow \operatorname {Aut}_K(S), \qquad \operatorname {pinRep}:\operatorname {Pin}(Q)\longrightarrow \operatorname {Aut}_K(S).\] Meinrenken calls the restriction of a Clifford module to the Clifford group the spin representation. The definitions here require only the commutative ring, module, quadratic form, and polarization data already used for \(\rho \); no nondegeneracy or finite-dimensionality is added.

                Lemma 7. The restricted actions are the Clifford action [meinrenken2013clifford, Section 3.2.1, pp. 55--56] [fcap-001N]
                spinRep_applypinRep_apply
                L∃∀N

                  For every \(g\in \operatorname {Spin}(Q)\) and \(h\in \operatorname {Pin}(Q)\), the two representations act through their underlying Clifford units: \[\operatorname {spinRep}(g)=\rho (g),\qquad \operatorname {pinRep}(h)=\rho (h).\] Thus the group actions introduce no new formula on \(S\); they are the same Clifford action with a smaller domain. In particular, any equation proved for the action of the underlying Clifford element applies to its Spin or Pin restriction.

                  Example 8. The rank-one polarized model [meinrenken2013clifford, Section 3.2.4, Theorem 3.3, p. 59] [fcap-001P]

                    Let \(W=Ke\) and choose \(e'\in W'\) with \(B_Q(e,e')=1\). In the ordered basis \((1,e)\) of \(S=\bigwedge W\), creation and contraction are \[\varepsilon _e= \begin {pmatrix}0&0\\1&0\end {pmatrix}, \qquad \iota _{e'}= \begin {pmatrix}0&1\\0&0\end {pmatrix}.\] Both are nilpotent, and \[\varepsilon _e\iota _{e'}+\iota _{e'}\varepsilon _e=I_2.\] Together with their products they give the four matrix units of \(\operatorname {End}_K(S)\). This is the rank-one calculation in Meinrenken's generation proof and a specialization of the general relation in Lemma 3. The formalized ingredients are TauCeti.SpinPolarizationData.contract_wedge and TauCeti.ExteriorAlgebra.creation_contraction_adjoin_eq_top; neither declaration formalizes this displayed choice of basis.

                    Remark 9. Horizons beyond the exterior model [meinrenken2013clifford, Section 3.2.4, Theorem 3.3, pp. 59--60]; [kostant1997clifford, Section 2.4, Theorem 8, pp. 286--287]; [lawson2016spin, I.2, pp. 13--19] [fcap-0017]

                      The exterior action constructed above stops before several classical consequences in representation theory. Over a split field, irreducibility and the decomposition into two half-spin modules require further hypotheses and arguments; Meinrenken proves these results after establishing that the Clifford action is an isomorphism. The currently open TauCeti half-spin work is therefore not represented by a Lean marker here.

                      The generic mathematics of differentiating a smooth Lie-group homomorphism is developed in § [fcap-001Q]. What remains missing for the Spin cover is more specific: compatible Lie-group structures on TauCeti's abstract \(\operatorname {Spin}(V)\) and \(SO(V)\), followed by the identification of their specialized differential with the algebraic quadratic action above. The open TauCeti PR linked in Remark [fcap-001W] proposes only the generic Lie functor.

                      Highest weights, triality, and the Bott-periodic real table also belong to later layers. Kostant supplies the differential in the classical complex setting, and Lawson--Michelsohn treat the real Pin and Spin groups. None of these horizons follows merely from the algebraic restrictions \(\operatorname {spinRep}\) and \(\operatorname {pinRep}\).

                      References

                        Reference. Spin geometry (pms-38) [lawson2016spin]

                        • 2016
                        • H. Blaine Lawson, Marie-Louise Michelsohn
                        @book{lawson2016spin,
 title = {Spin Geometry (Pms-38)},
 author = {Lawson, H. Blaine and Michelsohn, Marie-Louise},
 date = {2016},
 volume = {38},
 publisher = {{Princeton university press}}
}

                        Reference. Clifford algebras and lie theory [meinrenken2013clifford]

                        • 2013
                        • Eckhard Meinrenken
                        @book{meinrenken2013clifford,
 title = {Clifford algebras and Lie theory},
 author = {Meinrenken, Eckhard},
 year = {2013},
 volume = {58},
 publisher = {Springer}
}

                        Reference. Clifford algebra analogue of the Hopf--Koszul--Samelson theorem [kostant1997clifford]

                        • 1997
                        • Bertram Kostant
                        @article{kostant1997clifford,
 title = {Clifford Algebra Analogue of the Hopf--Koszul--Samelson Theorem},
 author = {Kostant, Bertram},
 year = {1997},
 journal = {Advances in Mathematics},
 volume = {125},
 number = {2},
 pages = {275--350},
 doi = {10.1006/aima.1997.1602}
}

                        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

                          Spin-representation roadmap [fcap-0019]

                            This appendix follows the mathematical dependencies of the spin-representation roadmap of Tau Ceti. The filtered Clifford algebra first exposes its exterior shadow. Reflections then lead to the global Pin and Spin extensions, while bivectors provide the algebraic infinitesimal orthogonal action. The Lie functor records the separate differential bridge from smooth group homomorphisms. A polarization joins the algebraic group and Lie constructions in the exterior spinor model. The real-signature recurrence and classification form a parallel algebraic branch and do not depend on the spinor-module or double-cover join.

                            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.

                              § [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]
                                    filtrationGradedPieceEquivExteriorPowerfiltrationLeadingTerm_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]
                                      filtrationAssociatedGradedEquivExterior
                                      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]
                                        filtrationAssociatedGradedEquivExterior_apply_of_succ
                                        L∃∀N

                                          For \(u,v\in M\), write the Clifford product 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\). Hence the degree-two class of \(\iota (u)\iota (v)\) is \(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.

                                            Reflections and square-normalized Clifford lifts [fcap-0007]

                                              A nonisotropic vector acts on the generating space by a reflection through twisted Clifford conjugation. Normalizing such vectors gives elements of Pin, while determinant parity detects the even products that belong to Spin. The cards pass from local lifts to reflection generation, Pin surjectivity, and finally Spin surjectivity onto the special orthogonal group.

                                              § [ca-0001]

                                              Convention. Quadratic-form sign [lawson2016spin, I.1, (1.3)--(1.4), p. 8] [fcap-0008]

                                                Lawson and Michelsohn write \[v^2=-q(v)1, \qquad vw+wv=-2q(v,w),\] where \(2q(v,w)=q(v+w)-q(v)-q(w)\). Mathlib and TauCeti instead use a quadratic form \(Q\) with \[\iota (v)^2=Q(v)1.\] The conventions agree after setting \(Q=-q\). The orthogonal group and its reflections are unchanged by this global sign reversal. A vector with \(q(v)=1\) therefore has \(Q(v)=-1\) in the convention used below. Mathlib's generator-square rule CliffordAlgebra.ι_sq_scalar uses this \(Q\)-convention.

                                                Definition. Reflection in a nonisotropic vector [lawson2016spin, I.2, (2.12), p. 14] [fcap-0009]
                                                reflection
                                                L∃∀N

                                                  Let \(F\) be a field of characteristic different from \(2\), let \(Q\) be a quadratic form on an \(F\)-vector space \(V\), and write \[B_Q(x,y)=Q(x+y)-Q(x)-Q(y)\] for its polar form. If \(Q(v)\ne 0\), the reflection with normal vector \(v\) is \[\rho _v(w)=w-\frac {B_Q(v,w)}{Q(v)}v.\] It fixes \(v^\perp \) pointwise, sends \(v\) to \(-v\), and preserves \(Q\). Multiplying \(v\) by a nonzero scalar does not change \(\rho _v\).

                                                  Lemma. Twisted Clifford conjugation is a reflection [lawson2016spin, I.2, Proposition 2.2 and (2.8), p. 13; (2.11)--(2.12), p. 14] [fcap-000A]

                                                    Let \(\alpha \) denote the grading involution of \(\mathcal {C}\kern -2pt\ell (Q)\). For \(Q(v)\ne 0\), the Clifford generator \(\iota (v)\) is invertible with \[\iota (v)^{-1}=Q(v)^{-1}\iota (v).\] Its twisted adjoint action on a generator is the reflection in Definition [fcap-0009]: \[\alpha (\iota (v))\,\iota (w)\,\iota (v)^{-1}=\iota (\rho _v(w)).\]

                                                    Proof. 

                                                      The generator-square rule CliffordAlgebra.ι_sq_scalar and the anticommutator rule CliffordAlgebra.ι_mul_ι_add_swap give \[\iota (v)\iota (w)+\iota (w)\iota (v)=B_Q(v,w).\] Since \(\alpha (\iota (v))=-\iota (v)\) and \(\iota (v)^2=Q(v)\), substitution yields \[-\iota (v)\iota (w)\frac {\iota (v)}{Q(v)} =\iota (w)-\frac {B_Q(v,w)}{Q(v)}\iota (v) =\iota (\rho _v(w)).\] The ordinary adjoint differs by the leading minus sign; the twisted adjoint is the action that gives the reflection itself.

                                                      Lemma. Square-normalized Pin lift [lawson2016spin, I.2, Definition 2.3 and (2.26), pp. 14, 18] [fcap-000B]
                                                      reflection_mem_range_pinToOrthogonal_of_isSquare
                                                      L∃∀N

                                                        Lawson--Michelsohn make this product-and-scaling argument for a finite-dimensional quadratic vector space over a field. The statement below is TauCeti's extension to a quadratic module over a commutative ring. It assumes that \(2\) and \(Q(v)\) are invertible.

                                                        Let \(R\) be a commutative ring, let \(Q\) be a quadratic form on an \(R\)-module \(M\), and suppose \(2\) and \(Q(v)\) are invertible. If there is a scalar \(c\) such that \[c^2=-Q(v)^{-1},\] then \(Q(cv)=-1\). The normalized Clifford generator \(\iota (cv)\) belongs to the Pin group and its twisted adjoint action is \(\rho _v\), because \(\rho _{cv}=\rho _v\). Consequently \[\rho _v\in \operatorname {range}(\operatorname {pinToOrthogonal}).\] Equivalently, the required hypothesis is that \(-Q(v)^{-1}\) is a square. The conclusion is existential: it asserts that a Pin lift exists, not that a canonical square root has been chosen.

                                                        Theorem. Paired reflections have a product-square Spin lift [lawson2016spin, I.2, (2.24)--(2.26), p. 18] [fcap-000C]
                                                        reflection_mul_reflection_mem_range_spinToOrthogonal_of_isSquare
                                                        L∃∀N

                                                          The cited product formulas are stated for a finite-dimensional quadratic vector space over a field. TauCeti packages the same scaling and Clifford-product calculation over the commutative-ring and module hypotheses inherited from Lemma [fcap-000B].

                                                          Let \(R\), \(M\), and \(Q\) be as in Lemma [fcap-000B]. Suppose \(Q(v)\), \(Q(w)\), and \(2\) are invertible. If there is a scalar \(c\) such that \[c^2=Q(v)^{-1}Q(w)^{-1},\] then \[Q(cv)Q(w)=1.\] Set \(x=\iota (cv)\iota (w)\). The element \(x\) is a product of invertible Clifford generators, and \[x^{*}x =\iota (w)\iota (cv)^2\iota (w) =Q(cv)Q(w)=1.\] Thus \(x\) is a unitary element of the Lipschitz group. It has even degree, so it belongs to the Spin group. Its twisted adjoint action is the ordered product of reflections, and therefore \[\rho _v\rho _w\in \operatorname {range}(\operatorname {spinToOrthogonal}).\]

                                                          Proof. 

                                                            The displayed square identity gives \(Q(cv)Q(w)=c^2Q(v)Q(w)=1\). Each generator is a Clifford unit and lies in the Lipschitz group, while the star calculation above establishes the unitary condition. The twisted adjoint is multiplicative on Clifford units, and scalar rescaling does not change a reflection. Hence the action of \(x\) is \(\rho _{cv}\rho _w=\rho _v\rho _w\); its even degree supplies the remaining Spin condition.

                                                            Equations (2.24)--(2.26) give the product descriptions and scaling invariance used here. The product-square condition is sharper than asking for separate normalizations of \(v\) and \(w\): one scalar normalizes the product even when neither vector has been normalized separately.

                                                            Example. A Euclidean unit normal [lawson2016spin, I.2, (2.12), p. 14; (2.24)--(2.26), p. 18] [fcap-000D]

                                                              Let \(V=\mathbb {R}^n\) with Euclidean inner product and use the sign convention \[Q(x)=-\langle x,x\rangle .\] For a unit vector \(v\), one has \(Q(v)=-1\); thus \(c=1\) satisfies the square condition in Lemma [fcap-000B]. The Clifford generator \(\iota (v)\) is already Pin-normalized, and its action is the familiar hyperplane reflection \[\rho _v(w)=w-2\langle v,w\rangle v.\] For orthonormal \(v,w\), the even product \(\iota (v)\iota (w)\) lies in Spin and lifts the composition \(\rho _v\rho _w\). This is the Euclidean specialization of the general Pin and paired-Spin lifting statements in Lemma [fcap-000B] and Theorem [fcap-000C].

                                                              Remark. From individual lifts to generation [lawson2016spin, I.2, Proposition 2.2, Definition 2.3, and (2.24)--(2.26), pp. 13--18] [fcap-000E]

                                                                Lawson and Michelsohn supply the twisted-adjoint reflection formula, the definitions of Pin and Spin, the description by products of normalized vectors, and the square-root obstruction to normalization. The square-witness statements in Lemma [fcap-000B] and Theorem [fcap-000C] isolate the precise algebraic hypotheses under which one or two reflections lift.

                                                                An individual lift does not by itself show that all orthogonal transformations lift. That global conclusion requires finite dimension, nondegeneracy, and the Cartan--Dieudonne factorization developed next.

                                                                From reflection generation to Pin and Spin [fcap-000U]

                                                                  One reflection can enlarge the fixed subspace of an orthogonal transformation. Iterating this correction proves that reflections generate the orthogonal group. Once each reflection has a Pin lift, generation gives the Pin cover; determinant parity then restricts that cover to Spin over the special orthogonal group.

                                                                  Lemma. Fixed-subspace correction by reflections [cartan1981theory, Section 10, pp. 10--12] [fcap-000V]
                                                                  exists_mem_subgroup_mul_eqOn_sup_span_singleton_of_reflection_mem
                                                                  L∃∀N

                                                                    Cartan proves reflection factorization by an induction that enlarges the fixed subspace. The subgroup-valued statement below is a formalized TauCeti lemma extracted from that method. Cartan's one- or two-reflection correction is repackaged as an element of \(H\) acting trivially on \(W+Kx\).

                                                                    Let \(K\) be a field of characteristic different from \(2\), let \(Q\) be a quadratic form on a \(K\)-vector space \(V\), and let \(H\le O(V,Q)\) contain every reflection in a nonisotropic vector. Suppose \(g\in O(V,Q)\) fixes a subspace \(W\) pointwise and \(x\in W^{\perp }\) has \(Q(x)\ne 0\). Then there is an element \(r\in H\) such that \[rg\vert _{W+Kx}=\operatorname {id}.\] The correction leaves the previously fixed space untouched and fixes one additional nonisotropic direction. It is either one reflection or a product of two reflections.

                                                                    Proof. 

                                                                      Compare \(x\) with \(g(x)\). When \(g(x)-x\) is nonisotropic, reflection in that difference carries \(g(x)\) to \(x\); because the difference is orthogonal to \(W\), the reflection fixes \(W\). In the exceptional case \(g(x)+x\) is nonisotropic: reflection in this sum carries \(g(x)\) to \(-x\), and reflection in \(x\) supplies the second factor. Both factors fix \(W\), so their product gives the required correction.

                                                                      Lemma. Pin-range refinement of the correction [cartan1981theory, Section 10, pp. 10--12]; [lawson2016spin, I.2, (2.26) and Theorem 2.9, pp. 18--19] [fcap-0018]
                                                                      exists_mem_range_pinToOrthogonal_mul_eqOn_sup_span_singleton
                                                                      L∃∀N

                                                                        Under the hypotheses of Lemma [fcap-000V], suppose moreover that \(K\) is separably closed and take \(H\) to be the range of the Pin action. Over a separably closed field, TauCeti's fixed-sign square condition from Theorem [fcap-000X] holds, so every reflection factor used by the correction has a square-normalized Pin lift by Lemma [fcap-000B]. The correcting element \(r\) can therefore be chosen in \[\operatorname {range}(\operatorname {pinToOrthogonal}),\] and still satisfies \(rg\vert _{W+Kx}=\operatorname {id}\). The statement concerns the correcting element in the Pin-action range; in the exceptional case it is the image of a product of two Pin lifts, not the image of a single reflecting vector.

                                                                        Theorem. Cartan--Dieudonne generation [lawson2016spin, I.2, Theorem 2.7, p. 17] [fcap-000W]
                                                                        subgroup_eq_top_of_reflection_mem
                                                                        L∃∀N

                                                                          Let \(K\) be a field of characteristic different from \(2\), let \(V\) be finite-dimensional, and let \(Q\) be nondegenerate. Every orthogonal transformation is a product of reflections in nonisotropic vectors. Equivalently, if a subgroup \(H\le O(V,Q)\) contains every such reflection, then \[H=O(V,Q).\] This formulation asserts generation only; it records neither a sharp bound on the number of reflection factors nor a parity formula for such a factorization.

                                                                          Proof. 

                                                                            Begin with the zero fixed subspace, whose restricted polar form is nondegenerate. If the current nondegenerate fixed subspace is not all of \(V\), its orthogonal complement is nonzero and nondegenerate, hence contains a nonisotropic vector. The correction step of Lemma [fcap-000V] enlarges the fixed subspace by that orthogonal line and preserves nondegeneracy. Finite-dimensional induction eventually makes the corrected product the identity, expressing the original transformation as a product of reflections. Cartan gives this fixed-vector induction, including the isotropic-difference case, in [cartan1981theory, Section 10, pp. 10--12].

                                                                            Theorem. Surjectivity of the Pin action [lawson2016spin, I.2, Theorem 2.9, pp. 18--19] [fcap-000X]
                                                                            pinToOrthogonal_surjective_of_isSquarepinToOrthogonal_surjective
                                                                            L∃∀N

                                                                              Let \(K\), \(V\), and \(Q\) be as in Theorem [fcap-000W]. Suppose every scalar \(-Q(v)^{-1}\) attached to a nonisotropic vector is a square in \(K\). Then the twisted-adjoint homomorphism is surjective: \[\operatorname {pinToOrthogonal}:\operatorname {Pin}(V,Q)\twoheadrightarrow O(V,Q).\] Indeed, Lemma [fcap-000B] puts every reflection in its range, and Theorem [fcap-000W] says that those reflections generate the target. In particular the conclusion holds over a separably closed field.

                                                                              Lawson and Michelsohn ask whether a nonzero vector can be rescaled to quadratic length either \(+1\) or \(-1\); see (2.26) and the discussion preceding Theorem 2.9. Under the convention \(Q=-q\), TauCeti's hypothesis asks for the particular scalar \(-Q(v)^{-1}\) to be a square, so every reflecting vector is normalized to one fixed sign. This is a sufficient and generally stronger condition, not an equivalent reformulation of Lawson--Michelsohn's condition.

                                                                              Example. A planar rotation as two reflections [lawson2016spin, I.2, (2.24)--(2.26), p. 18] [fcap-000Y]

                                                                                In an oriented Euclidean plane, let \(u\) and \(v\) be unit normals whose directed angle is \(\frac {\theta }{2}\). Reflection in \(u^{\perp }\) followed by reflection in \(v^{\perp }\) is rotation through \(\theta \). With the convention \(Q=-\langle -,-\rangle \), both vectors have \(Q=-1\), and \[s=\iota (v)\iota (u)\in \operatorname {Spin}(V,Q)\] lifts that rotation. In an oriented orthonormal basis \(e_1,e_2\), the familiar rotor form is \[\pm s=\cos \left (\frac {\theta }{2}\right )+\sin \left (\frac {\theta }{2}\right )\,\iota (e_1)\iota (e_2),\] after choosing the central sign and the order convention for the two reflections. This is the two-dimensional specialization of the paired lift in Theorem [fcap-000C]; the half-angle appears because the Spin element acts by conjugation on vectors.

                                                                                Lemma. Determinant parity detects the even lift [lawson2016spin, I.2, Theorems 2.7 and 2.9, pp. 17--19] [fcap-001A]
                                                                                det_reflectionmem_even_of_det_pinToOrthogonal_eq_one
                                                                                L∃∀N

                                                                                  Let \(R\) be a commutative ring in which \(2\) is invertible, let \(M\) be a finite free \(R\)-module, and let \(Q\) be a quadratic form on \(M\). A reflection in a vector of invertible quadratic value has determinant \(-1\). Therefore a product of \(r\) such reflections has determinant \[(-1)^r.\] In particular, every product of an even number of reflections belongs to \(SO(M,Q)\).

                                                                                  Lawson--Michelsohn state this parity argument for quadratic vector spaces over a field. The finite-free commutative-ring statement above is the formalized extension: its determinant calculation uses freeness and finiteness, while invertibility of \(2\) identifies the fixed part of the grading involution with the even subalgebra.

                                                                                  The Clifford lift remembers this parity. If \(p\in \operatorname {Pin}(M,Q)\) and its orthogonal action has determinant \(1\), then \(p\) lies in the even Clifford subalgebra. Hence \(p\) is a Spin element. Thus any Pin lift of a special orthogonal transformation is automatically even.

                                                                                  Proof. 

                                                                                    Multiplicativity of the determinant gives the first assertion from \(\det (\rho _v)=-1\). For the second, the grading involution of a Lipschitz element is its determinant sign times that element. If the determinant is \(1\), the involution fixes the Pin element. Because \(2\) is invertible, the fixed submodule of the grading involution is precisely the even Clifford subalgebra.

                                                                                    Theorem. Surjectivity of the Spin action [lawson2016spin, I.2, Theorem 2.9, pp. 18--19] [fcap-001B]
                                                                                    spinToSpecialOrthogonal_surjective_of_isSquarespinToSpecialOrthogonal_surjective
                                                                                    L∃∀N

                                                                                      Let \(K\) be a field of characteristic different from \(2\), let \(V\) be finite-dimensional, and let \(Q\) be nondegenerate. Suppose that for every nonisotropic \(v\in V\), the scalar \(-Q(v)^{-1}\) is a square in \(K\). Then the twisted-adjoint action restricts to a surjection \[\operatorname {Spin}(V,Q)\twoheadrightarrow SO(V,Q).\] The underlying homomorphism is TauCeti.CliffordAlgebra.spinToSpecialOrthogonal, and its action on vectors is the usual Spin action by TauCeti.CliffordAlgebra.coe_spinToSpecialOrthogonal_apply.

                                                                                      Indeed, the square-normalization hypothesis and Cartan--Dieudonne generation give the Pin surjection of Theorem [fcap-000X]. It lifts an element of \(SO(V,Q)\) to Pin; the lift has determinant \(1\), so Lemma [fcap-001A] shows that it is even and therefore lies in Spin. The restriction square

                                                                                      commutes because both vertical maps are induced by the same twisted Clifford conjugation. Over a separably closed field the square condition is automatic, so nondegeneracy and finite dimension suffice. The general restriction principle from a surjective Pin action is TauCeti.CliffordAlgebra.spinToSpecialOrthogonal_surjective_of_pinToOrthogonal_surjective.

                                                                                      The square condition is TauCeti's fixed-sign sufficient hypothesis, stronger in general than Lawson--Michelsohn's option to normalize each vector to either sign; see Theorem [fcap-000X]. For a positive-definite real geometric form \(q\), the Clifford convention is \(Q=-q\); hence \(-Q(v)^{-1}>0\) for every nonzero \(v\), so the reflecting vectors can be normalized over \(\mathbb {R}\). This observation does not assert the square condition for arbitrary real signatures.

                                                                                      Lemma. The real Spin kernel is the scalar pair [gallier2014clifford, Section 1.8, Proposition 1.21, pp. 39--40] [fcap-001C]
                                                                                      zmodTwoMulEquivKerSpinToSpecialOrthogonal
                                                                                      L∃∀N

                                                                                        For a real quadratic space of signature \((p,q)\), the kernel of the Spin action is the scalar pair: \[(\mathbb Z/2\mathbb Z)_{\mathrm {mult}} \simeq \ker \bigl (\operatorname {Spin}(p,q)\longrightarrow SO(p,q)\bigr ).\] The nontrivial residue class maps to the scalar Clifford element \(-1\). Thus the two kernel elements are precisely \(1\) and \(-1\). This is the kernel used in Gallier's real double-cover theorem.

                                                                                        TauCeti proves the analogous algebraic statement over a field \(K\): \(V\) is nontrivial and finite-dimensional, \(Q\) is nondegenerate, and \(2\) is invertible in \(K\). Under exactly those hypotheses it constructs the displayed canonical multiplicative equivalence. This is a generalization of the cited real result, not an attribution of arbitrary-field kernel classification to Gallier.

                                                                                        Theorem. The algebraic Spin extension [meinrenken2013clifford, Definition 3.2, pp. 51--52] [fcap-001D]
                                                                                        spinDoubleCoverOfSurjectivespinDoubleCover
                                                                                        L∃∀N

                                                                                          Let \(K\) be a characteristic-zero field, let \(V\) be finite-dimensional, and let its bilinear form be nondegenerate. Meinrenken defines Spin as the even part of the norm-one Clifford group. Its kernel is the scalar pair. If the Spin action is surjective, these data form the group extension \[1\longrightarrow (\mathbb Z/2\mathbb Z)_{\mathrm {mult}} \longrightarrow \operatorname {Spin}(Q)\longrightarrow SO(Q)\longrightarrow 1.\] The left map sends the nontrivial class to \(-1\); the right map is the Spin action. TauCeti packages this generic construction from an explicit surjectivity proof. The group-extension constructor used in that package is GroupExtension.ofMulEquivKer.

                                                                                          Meinrenken warns that the map to \(SO(V)\) need not be surjective over a general field; it is surjective when every element of \(K\) has a square root, because lifts can then be rescaled to have norm one. TauCeti separates this issue explicitly. Its generic construction assumes a field, a nontrivial finite-dimensional module, invertible \(2\), a nondegenerate quadratic form, and a supplied surjectivity proof. Over a separably closed field, Theorem [fcap-001B] supplies that proof and yields the specialized extension.

                                                                                          Lemma. The real Pin kernel is the scalar pair [gallier2014clifford, Section 1.8, Proposition 1.21, pp. 39--40] [fcap-001E]
                                                                                          zmodTwoMulEquivKerPinToOrthogonal
                                                                                          L∃∀N

                                                                                            For a real quadratic space of signature \((p,q)\), the Pin action has the same two-element kernel: \[(\mathbb Z/2\mathbb Z)_{\mathrm {mult}} \simeq \ker \bigl (\operatorname {Pin}(p,q)\longrightarrow O(p,q)\bigr ).\] Its nontrivial generator is the image in Pin of the scalar Spin element \(-1\). The identification is obtained by comparing the Pin kernel with the Spin kernel, not by adding a second pair of central elements. Gallier's real double-cover proof uses exactly the quotient by \(\{\pm 1\}\).

                                                                                            TauCeti transports the Spin-kernel equivalence to Pin over a field \(K\) when the module is nontrivial and finite-dimensional, \(Q\) is nondegenerate, and \(2\) is invertible. These are the formal theorem's exact assumptions; the cited scholarly claim is the real case.

                                                                                            Theorem. The algebraic Pin extension [meinrenken2013clifford, Definition 3.2, pp. 51--52] [fcap-001F]
                                                                                            pinDoubleCoverOfSurjectivepinDoubleCover
                                                                                            L∃∀N

                                                                                              In Meinrenken's characteristic-zero, finite-dimensional, nondegenerate setting, Pin is the kernel of the norm on the Clifford group. Its scalar kernel and any proof that the Pin action is surjective determine the group extension \[1\longrightarrow (\mathbb Z/2\mathbb Z)_{\mathrm {mult}} \longrightarrow \operatorname {Pin}(Q)\longrightarrow O(Q)\longrightarrow 1.\] The inclusion sends the nontrivial class to the scalar \(-1\), and the projection is the Pin action. Meinrenken notes that surjectivity can fail over a general field and that square roots for all field elements suffice to normalize lifts. TauCeti's generic theorem instead assumes a field, a nontrivial finite-dimensional module, invertible \(2\), a nondegenerate quadratic form, and an explicit surjectivity proof. Its separably closed specialization obtains that proof from the formal Cartan--Dieudonne route.

                                                                                              Remark. Algebraic extension versus topological cover [fcap-000Z]

                                                                                                The extensions in Theorem [fcap-001D] and Theorem [fcap-001F] are exact sequences of abstract groups. They record a surjective homomorphism and its two-element kernel. No topology on the groups is used.

                                                                                                For real quadratic spaces of arbitrary signature, Gallier proves that the two maps \[\operatorname {Pin}(p,q)\longrightarrow O(p,q),\qquad \operatorname {Spin}(p,q)\longrightarrow SO(p,q)\] are topological double covers [gallier2014clifford, Section 1.8, Proposition 1.21, pp. 39--40].

                                                                                                Gallier then treats the compact groups: \(\operatorname {Spin}(n)\) is path-connected for \(n\geq 2\), and for \(n\geq 3\) it is simply connected and hence the universal cover of \(SO(n)\) [gallier2014clifford, Section 1.8, pp. 40--42]. These claims are not being extended here to arbitrary signature. Kostant identifies the differential of the complex Spin cover with the quadratic Clifford Lie algebra [kostant1997clifford, Section 2.4, Theorem 8, pp. 286--287]. Those conclusions require topological or Lie-theoretic structure not supplied by an abstract group extension. They are not asserted by the four cards above.

                                                                                                Bivectors and the orthogonal Lie algebra [fcap-000M]

                                                                                                  The second exterior power singled out by the PBW filtration has a second life inside the Clifford algebra. Its half-commutators are closed under the commutator bracket, and their action on generators is exactly the infinitesimal orthogonal action.

                                                                                                  § [ca-0001]

                                                                                                  Convention. Bivector normalizations [meinrenken2013clifford, Section 2.2.5, Proposition 2.5, p. 33] [fcap-000N]
                                                                                                  bivector_defbivector_lie_ι
                                                                                                  L∃∀N

                                                                                                    Meinrenken works throughout this chapter with finite-dimensional vector spaces over a characteristic-zero field. The cards below retain his normalization and formulas but follow TauCeti's extensions. Each card states the commutative-ring, module, invertible-\(2\), finite-dimensional, or nondegeneracy assumptions it needs.

                                                                                                    Meinrenken starts with a symmetric bilinear form \(B\) and the relation \[uv+vu=2B(u,v)1.\] For the associated quadratic form \(Q(v)=B(v,v)\), the polar form used here is \(B_Q=2B\).

                                                                                                    Meinrenken's quantization formula and the half-commutator agree: \[q(u\wedge v)=uv-B(u,v)1 =\frac 12(uv-vu)=:\beta (u,v).\] The induced action on a vector is \[[\beta (u,v),x] =B_Q(v,x)u-B_Q(u,x)v =2\bigl (B(v,x)u-B(u,x)v\bigr ).\] This is Meinrenken's formula \(-2\iota _{B(x,-)}(u\wedge v)\) and Kostant's formula \(-2\iota _x(u\wedge v)\) in the corresponding contraction convention [kostant1997clifford, Section 2.4, (12) and Theorem 8, pp. 283, 286]. The factor of two belongs to the passage from \(B\) to the unhalved polar form \(B_Q\); it is not an additional rescaling of \(\beta \).

                                                                                                    Definition. Clifford bivector [meinrenken2013clifford, Section 2.2.5, Proposition 2.5, p. 33] [fcap-000O]
                                                                                                    bivectorExteriorequivExterior_bivectorExterior
                                                                                                    L∃∀N

                                                                                                      For the formalized extension described in Convention [fcap-000N], let \(R\) be a commutative ring in which \(2\) is invertible, let \(M\) be an \(R\)-module, and let \(Q\) be a quadratic form on \(M\). The Clifford bivector of \(u,v\in M\) is \[\beta _Q(u,v)=\frac 12\bigl (\iota (u)\iota (v)-\iota (v)\iota (u)\bigr ).\] It is alternating in \(u\) and \(v\), so it induces a linear map \[\beta _Q:\bigwedge _R^2M\longrightarrow \mathcal {C}\kern -2pt\ell (Q).\] The exterior model is a left inverse on its image: \[\operatorname {equivExterior}_Q\bigl (\beta _Q(z)\bigr )=z \qquad (z\in \bigwedge _R^2M).\] Hence \(\beta _Q\) is injective.

                                                                                                      Lemma. A bivector acts by an infinitesimal rotation [meinrenken2013clifford, Section 2.2.10, Theorem 2.1, pp. 39--40] [fcap-000P]
                                                                                                      bivector_lie_ι
                                                                                                      L∃∀N

                                                                                                        For \(u,v,x\in M\), the commutator of the bivector with a Clifford generator is \[[\beta _Q(u,v),\iota (x)] =\iota \left (B_Q(v,x)u-B_Q(u,x)v\right ).\] The endomorphism \[A_{u\wedge v}(x)=B_Q(v,x)u-B_Q(u,x)v\] is skew-adjoint for \(B_Q\), since \[B_Q(A_{u\wedge v}x,y)+B_Q(x,A_{u\wedge v}y)=0.\] Thus commutation by a degree-two Clifford element preserves the generating module and realizes the elementary infinitesimal orthogonal transformation attached to \(u\wedge v\).

                                                                                                        Proof. 

                                                                                                          Expand the half-commutator and move \(\iota (x)\) past \(\iota (u)\) and \(\iota (v)\) using the Clifford relation. The cubic terms cancel; the two polar terms combine to the displayed generator. Symmetry of \(B_Q\) then makes the skew-adjointness equation cancel in pairs.

                                                                                                          Theorem. Exterior bivectors are the quadratic Clifford Lie algebra [meinrenken2013clifford, Section 2.2.10, Theorem 2.1, pp. 39--40] [fcap-000Q]
                                                                                                          bivectorExteriorEquivQuadraticLieSubalgebrabivectorLieEquiv
                                                                                                          L∃∀N

                                                                                                            Over the commutative ring and module of Definition [fcap-000O], let \(\mathfrak {cl}^{(2)}(Q)\) be the submodule of \(\mathcal {C}\kern -2pt\ell (Q)\) spanned by the elements \(\beta _Q(u,v)\). This is TauCeti's module-general extension of Meinrenken's characteristic-zero vector-space construction. The commutator formula of Lemma [fcap-000P], together with the Jacobi identity, shows that this submodule is closed under commutators. Transporting its bracket across \(\beta _Q\) gives a Lie algebra structure on \(\bigwedge _R^2M\) and a Lie equivalence \[\bigwedge _R^2M\simeq _{\mathrm {Lie}}\mathfrak {cl}^{(2)}(Q).\] On a decomposable bivector the equivalence is exactly \[u\wedge v\longmapsto \frac 12(uv-vu).\] No choice of basis enters this identification.

                                                                                                            Theorem. Quadratic elements realize the orthogonal Lie algebra [meinrenken2013clifford, Section 2.2.10, Proposition 2.12, p. 40] [fcap-000R]
                                                                                                            soEquivQuadraticsoEquivQuadratic_lie_ι
                                                                                                            L∃∀N

                                                                                                              Meinrenken states this realization over a characteristic-zero field. TauCeti proves the extension below over any field of characteristic different from \(2\). Let \(K\) be such a field, let \(V\) be finite-dimensional, and let \(Q\) be nondegenerate. Write \(\mathfrak {so}(V,B_Q)\) for the Lie algebra of endomorphisms skew-adjoint for the polar form. Then commutation on generators gives a Lie equivalence \[\mathfrak {so}(V,B_Q)\simeq _{\mathrm {Lie}}\mathfrak {cl}^{(2)}(Q).\] If \(A\in \mathfrak {so}(V,B_Q)\) corresponds to \(z_A\in \mathfrak {cl}^{(2)}(Q)\), then \[[z_A,\iota (x)]=\iota (Ax)\qquad (x\in V).\] Combining this equivalence with Theorem [fcap-000Q] gives the basis-free chain \[\bigwedge _K^2V\simeq _{\mathrm {Lie}}\mathfrak {so}(V,B_Q) \simeq _{\mathrm {Lie}}\mathfrak {cl}^{(2)}(Q).\] Kostant identifies the same degree-two subspace with \(\operatorname {Lie}(\operatorname {Spin}(V))\) and the first equivalence with the differential of the double cover [kostant1997clifford, Section 2.4, Theorem 8, pp. 286--287].

                                                                                                              Example. An elementary skew matrix [meinrenken2013clifford, Section 2.2.10, Proposition 2.12, p. 40] [fcap-000S]
                                                                                                              bivectorEquivSo_apply_ιMultibivectorEquivSo_apply_ιMulti_mulVec
                                                                                                              L∃∀N

                                                                                                                This coordinate example specializes TauCeti's extension of the characteristic-zero construction summarized in Convention [fcap-000N]. Take \(V=R^n\) with the standard sum-of-squares quadratic form, and let \(e_i,e_j\) be distinct coordinate vectors. Under the standard-coordinate realization, \[e_i\wedge e_j\longmapsto 2(E_{ij}-E_{ji}).\] Thus its action on \(x=(x_k)\) is \[x\longmapsto 2x_j e_i-2x_i e_j.\] The factor \(2\) is the polar-form normalization from Convention [fcap-000N]: for the sum-of-squares form, \(B_Q(x,y)=2\sum _kx_ky_k\). The displayed matrix is the standard-coordinate specialization of the basis-free isomorphism in Meinrenken's proposition. Dividing the skew matrix by two would correspond to using the associated bilinear form \(B_Q/2\) instead.

                                                                                                                Remark. Infinitesimal and global Clifford symmetry [fcap-000T]

                                                                                                                  The quadratic Clifford Lie algebra is the infinitesimal part of the same conjugation action that produces reflections. Kostant proves that \(\bigwedge ^2V=\operatorname {Lie}(\operatorname {Spin}(V))\), that its map to \(\mathfrak {so}(V)\) is the differential of \(\operatorname {Spin}(V)\to SO(V)\), and that its commutator action extends as the corresponding derivation of the exterior algebra [kostant1997clifford, Section 2.4, Theorem 8, pp. 286--287]. Chevalley obtains the same two-vector Lie algebra inside the Clifford group [chevalley1954algebraic, II.2.9, pp. 67--68].

                                                                                                                  The cards above identify the algebraic Lie layer. They do not construct Lie-group structures or identify a differential of a Lie-group covering map. The next chapter instead reaches the global orthogonal group by finite products of reflections.

                                                                                                                  Theorem. An orthogonal Lie action lifts to every Clifford module [kostant1997clifford, Section 3.1, pp. 294--295] [fcap-001O]
                                                                                                                  cliffordInducedRepcliffordInducedRep_apply
                                                                                                                  L∃∀N

                                                                                                                    Let \(K\) be a field in which \(2\) is invertible, let \(V\) be finite-dimensional, and let \(Q\) be nondegenerate. Suppose a \(K\)-Lie algebra \(L\) acts orthogonally on \(V\) through \[\theta :L\longrightarrow \mathfrak {so}(V,B_Q),\] and let \(\rho :\mathcal {C}\kern -2pt\ell (Q)\to \operatorname {End}_K(S)\) be any Clifford module. The equivalence of Theorem [fcap-000R] lifts \(\theta \) to quadratic Clifford elements; composing with \(\rho \) gives a Lie representation \[\rho _{\mathcal {C}\kern -2pt\ell }:L\longrightarrow \operatorname {End}_K(S),\qquad \rho _{\mathcal {C}\kern -2pt\ell }(y)=\rho \bigl (\operatorname {soEquivQuadratic}(\theta (y))\bigr ).\] Kostant constructs this lift for a complex reductive group representation and then lets its quadratic elements act on the spin module. The formalized statement isolates the algebraic mechanism over the stated field and for an arbitrary Clifford module; it does not assert that \(\theta \) is a differential of a group representation.

                                                                                                                    Differentiating smooth group homomorphisms [fcap-001Q]

                                                                                                                      The quadratic Clifford construction in the preceding section is algebraic. A different bridge starts from a smooth homomorphism of Lie groups and differentiates it at the identity. This produces the functor from Lie groups to Lie algebras and explains which part of the Spin-representation roadmap is generic differential geometry, before any Lie-group structure on the abstract Spin and special orthogonal groups has been supplied.

                                                                                                                      Definition. The differential of a smooth homomorphism [liu2016lie, Section 2.1, p. 9] [fcap-001R]

                                                                                                                        Let \(G\) and \(H\) be finite-dimensional real Lie groups, with identities \(e_G\) and \(e_H\), and let \(\phi :G\to H\) be a smooth group homomorphism. Their Lie algebras are the tangent spaces \[\mathfrak g=T_{e_G}G, \qquad \mathfrak h=T_{e_H}H.\] The differential of \(\phi \) at the identity is the linear map \[\operatorname {Lie}(\phi )=d\phi _{e_G}: \mathfrak g\longrightarrow \mathfrak h.\] No connectedness or simply-connectedness hypothesis is needed to define this map. Those hypotheses enter the converse problem of integrating a Lie-algebra homomorphism, not the differentiation of a given smooth homomorphism.

                                                                                                                        For \(X\in \mathfrak g\), let \(\widetilde X\) be its left-invariant vector field, \[\widetilde X_g=d(L_g)_{e_G}X.\] The homomorphism identity \(\phi \circ L_g=L_{\phi (g)}\circ \phi \) gives \[d\phi _g(\widetilde X_g) =\widetilde {\operatorname {Lie}(\phi )(X)}_{\phi (g)}.\] Thus differentiation at the identity and transport by left translation are two descriptions of the same infinitesimal map.

                                                                                                                        Lemma. The differential preserves the Lie bracket [liu2016lie, Section 2.1, p. 9] [fcap-001S]

                                                                                                                          In the setting of Definition [fcap-001R], the differential is a Lie-algebra homomorphism: \[\operatorname {Lie}(\phi )([X,Y]) =[\operatorname {Lie}(\phi )(X), \operatorname {Lie}(\phi )(Y)].\] Indeed, the left-invariant fields \(\widetilde X\) and \(\widetilde Y\) are \(\phi \)-related to the left-invariant fields determined by their images. Brackets of related vector fields are again related. Evaluating that relation at \(e_G\) gives the displayed identity.

                                                                                                                          This argument is local at the identity. In particular, bracket preservation does not require \(G\) to be connected or simply connected.

                                                                                                                          Theorem. The Lie functor [liu2016lie, Section 2.2, p. 10] [fcap-001T]

                                                                                                                            Differentiation at the identity is functorial. For smooth homomorphisms \(G\xrightarrow {\phi }H\xrightarrow {\psi }K\), the chain rule gives \[\operatorname {Lie}(\operatorname {id}_G) =\operatorname {id}_{\mathfrak g}, \qquad \operatorname {Lie}(\psi \circ \phi ) =\operatorname {Lie}(\psi )\circ \operatorname {Lie}(\phi ).\] Together with Lemma [fcap-001S], this defines a functor from Lie groups and smooth homomorphisms to Lie algebras and Lie-algebra homomorphisms.

                                                                                                                            The stronger correspondence between simply connected Lie groups and Lie algebras concerns existence and uniqueness in the reverse direction. It is not a hypothesis of these functor laws.

                                                                                                                            Theorem. Naturality of the exponential [liu2016lie, Section 2.4, pp. 12--13] [fcap-001U]

                                                                                                                              Let \(\phi :G\to H\) be a smooth Lie-group homomorphism. For every \(X\in \mathfrak g\), \[\phi (\exp _G X) =\exp _H\bigl (\operatorname {Lie}(\phi )(X)\bigr ).\] Equivalently, the square

                                                                                                                              commutes.

                                                                                                                              Proof. 

                                                                                                                                The curve \(t\mapsto \phi (\exp _G(tX))\) is a one-parameter subgroup of \(H\). Its tangent vector at \(t=0\) is \(\operatorname {Lie}(\phi )(X)\). The curve \(t\mapsto \exp _H(t\operatorname {Lie}(\phi )(X))\) has the same property and the same tangent vector. Uniqueness of the one-parameter subgroup with a given tangent vector identifies the curves; setting \(t=1\) proves the formula.

                                                                                                                                Example. Differentiating a matrix representation [liu2016lie, Sections 2.1 and 2.4, pp. 9, 12] [fcap-001V]

                                                                                                                                  Let \(V\) be a finite-dimensional real vector space and let \[\rho :G\longrightarrow \operatorname {GL}(V)\] be a smooth representation. Its differential is a Lie-algebra representation \[d\rho _{e_G}:\mathfrak g\longrightarrow \mathfrak {gl}(V).\] Naturality of the exponential becomes \[\rho (\exp _G X)=\exp \bigl (d\rho _{e_G}(X)\bigr ),\] where the exponential on the right is the ordinary matrix exponential. For example, for the determinant homomorphism \(\det :\operatorname {GL}_n(\mathbb R)\to \mathbb R^\times \), \[d(\det )_I(A)=\operatorname {tr}(A).\]

                                                                                                                                  Remark. Why explicit smoothness changes the roadmap [liu2016lie, Sections 2.1--2.4 and 2.8, pp. 9--13, 19--20]; [isaev2018theory, Section 3.1.2, pp. 106--107] [fcap-001W]

                                                                                                                                    The constructions in Definition [fcap-001R]--Example [fcap-001V] start with a smooth homomorphism. Their tangent map, bracket law, functor laws, and exponential naturality therefore do not require a theorem that upgrades a continuous homomorphism to a smooth one. The generic theorem does not invoke the closed-subgroup theorem; that theorem belongs to the later specialization to concrete matrix subgroups. This is the dependency split proposed in TauCetiRoadmap PR 224.

                                                                                                                                    The exponential input is separate from the tangent and bracket input. Likewise, the Baker--Campbell--Hausdorff calculation can first be made in a matrix or general-linear group; using it inside a particular closed matrix subgroup additionally requires the subgroup's Lie structure. Liu describes the local exponential and BCH coordinates, while Isaev--Rubakov give the matrix Campbell--Hausdorff calculation.

                                                                                                                                    The open TauCeti draft PR 3078 proposes the generic construction and its functor and exponential laws. It is not merged, so these cards carry no Lean markers. Even after that generic interface lands, the differential of \(\operatorname {Spin}(Q)\to SO(Q)\) still needs compatible Lie-group structures on the two abstract groups. The algebraic identification in Theorem [fcap-000R] does not by itself supply those structures.

                                                                                                                                    Polarization and the exterior spinor model [fcap-001G]
                                                                                                                                    ✍️source

                                                                                                                                      A polarization turns Clifford generators into creation, contraction, and parity operators on an exterior algebra. The resulting Clifford action has two group restrictions and receives every orthogonal Lie action through the quadratic Clifford realization.

                                                                                                                                      Write \(S=\bigwedge _K W\) for the exterior carrier and \(\rho :\mathcal {C}\kern -2pt\ell (Q)\to \operatorname {End}(S)\) for its Clifford action. Let \(\mathfrak g\) be an external Lie algebra with an orthogonal action \(\theta :\mathfrak g\to \mathfrak {so}(V,Q)\). The diagram records the induced Lie action at the top and the Pin and Spin restrictions of \(\rho \) below.

                                                                                                                                      § [ca-0001]

                                                                                                                                      Definition. Polarization data and its carrier [chevalley1954algebraic, II.2.1--II.2.2, pp. 42--44] [fcap-001H]
                                                                                                                                      SpinPolarizationData
                                                                                                                                      L∃∀N

                                                                                                                                        Let \(K\) be a commutative ring, let \(V\) be a \(K\)-module, and let \(Q\) be a quadratic form. Polarization data consists of isotropic submodules \(W,W'\subseteq V\), an orthogonal remainder \(L\), and a linear equivalence \[(W\oplus W')\oplus L\simeq V.\] The polar form identifies \(W'\) with \(W^*\); the pairing is separating in both variables. A coordinate \(\ell :L\to K\) is injective and satisfies \(\ell (z)^2=Q(z)\). Thus \(L\) is an orthogonal remainder equipped with an injective coordinate. Over a field it is at most one-dimensional; it vanishes in the classical even split model. The carrier of the exterior spinor model is \[S=\bigwedge _K W.\]

                                                                                                                                        Chevalley treats complementary totally singular subspaces in the split, even-dimensional field case. Meinrenken uses the equivalent Lagrangian model \(V=F^*\oplus F\) [meinrenken2013clifford, Section 3.2.2, Proposition 3.5, pp. 56--57]. The packaged remainder and commutative-ring hypotheses are TauCeti's stated generalization.

                                                                                                                                        Definition. Creation, contraction, and the line operator [meinrenken2013clifford, Section 3.2.2, Proposition 3.5, p. 57] [fcap-001I]
                                                                                                                                        wedgecontractlineOperator
                                                                                                                                        L∃∀N

                                                                                                                                          For \(x\in W\), creation is exterior multiplication \[\varepsilon _x(s)=x\wedge s.\] For \(y\in W'\), contraction is the degree-\(-1\) operator \(\iota _y\) associated with the functional \(x\mapsto B_Q(x,y)\). Finally, if \(z\in L\), its operator is \[\lambda _z=\ell (z)\,\alpha ,\] where \(\alpha \) is parity: it is \(+1\) on even exterior degree and \(-1\) on odd exterior degree. Chevalley's formulas identify the first two operators as left Clifford multiplication on the minimal ideal model [chevalley1954algebraic, II.2.2, pp. 43--44].

                                                                                                                                          Lemma. The polarized Clifford relation [meinrenken2013clifford, Section 3.2.1, pp. 54--55] [fcap-001J]
                                                                                                                                          contract_wedgecliffordOperator_sq
                                                                                                                                          L∃∀N

                                                                                                                                            Creation and contraction satisfy \[\iota _y\varepsilon _x+\varepsilon _x\iota _y =B_Q(x,y)\operatorname {id}_S.\] Creation and contraction each square to zero. Parity anticommutes with both, while \(\lambda _z^2=Q(z)\operatorname {id}_S\). Consequently the operator \(c(v)\) assembled from the three polarization coordinates obeys \[c(v)^2=Q(v)\operatorname {id}_S.\] This is the quadratic form of the usual polarized anticommutation relation \(c(v)c(w)+c(w)c(v)=B_Q(v,w)\). Meinrenken states the latter as the defining condition for a Clifford module.

                                                                                                                                            Theorem. The exterior Clifford action [meinrenken2013clifford, Section 3.2.2, Proposition 3.5, p. 57] [fcap-001K]
                                                                                                                                            spinAction
                                                                                                                                            L∃∀N

                                                                                                                                              The square relation of Lemma [fcap-001J] extends uniquely to an algebra homomorphism \[\rho :\mathcal {C}\kern -2pt\ell (Q)\longrightarrow \operatorname {End}_K(S).\] On the three summands it is determined by \[\rho (\iota (x))s=x\wedge s,\qquad \rho (\iota (y))s=\iota _y(s),\qquad \rho (\iota (z))s=\ell (z)\alpha (s).\] The corresponding formalized equations are TauCeti.spinAction_ι_wedge, TauCeti.spinAction_ι_contract, and TauCeti.spinAction_ι_lineOperator. Chevalley's split even-dimensional model has no remainder term; the third formula is TauCeti's odd-line extension of that construction.

                                                                                                                                              Theorem. Creation and contraction generate all endomorphisms [meinrenken2013clifford, Section 3.2.4, Theorem 3.3, pp. 59--60] [fcap-001L]
                                                                                                                                              creation_contraction_adjoin_eq_topspinAction_surjective
                                                                                                                                              L∃∀N

                                                                                                                                                Assume that \(W\) is finite and free over the commutative ring \(K\). The subalgebra of \(\operatorname {End}_K(\bigwedge W)\) generated by all creation operators and all contractions is the whole endomorphism algebra. Since the polar pairing identifies \(W'\) with \(W^*\), these generators lie in the image of the exterior Clifford action. Hence \[\rho :\mathcal {C}\kern -2pt\ell (Q)\twoheadrightarrow \operatorname {End}_K(\bigwedge W)\] is surjective.

                                                                                                                                                Meinrenken proves generation first in rank one by four matrix units and then by tensor decomposition. Over a split field he combines surjectivity with a dimension calculation to obtain an isomorphism and irreducibility. TauCeti formalizes the generation and surjectivity statements over a finite free module. This card does not claim that \(S\) is irreducible, or that \(\rho \) is injective.

                                                                                                                                                Definition. The Spin and Pin representations [meinrenken2013clifford, Section 3.2.1, pp. 55--56] [fcap-001M]
                                                                                                                                                spinReppinRep
                                                                                                                                                L∃∀N

                                                                                                                                                  The groups \(\operatorname {Spin}(Q)\) and \(\operatorname {Pin}(Q)\) consist of units in the Clifford algebra. Restricting the action \(\rho \) of Theorem [fcap-001K] along these two inclusions gives representations on the same exterior carrier: \[\operatorname {spinRep}:\operatorname {Spin}(Q)\longrightarrow \operatorname {Aut}_K(S), \qquad \operatorname {pinRep}:\operatorname {Pin}(Q)\longrightarrow \operatorname {Aut}_K(S).\] Meinrenken calls the restriction of a Clifford module to the Clifford group the spin representation. The definitions here require only the commutative ring, module, quadratic form, and polarization data already used for \(\rho \); no nondegeneracy or finite-dimensionality is added.

                                                                                                                                                  Lemma. The restricted actions are the Clifford action [meinrenken2013clifford, Section 3.2.1, pp. 55--56] [fcap-001N]
                                                                                                                                                  spinRep_applypinRep_apply
                                                                                                                                                  L∃∀N

                                                                                                                                                    For every \(g\in \operatorname {Spin}(Q)\) and \(h\in \operatorname {Pin}(Q)\), the two representations act through their underlying Clifford units: \[\operatorname {spinRep}(g)=\rho (g),\qquad \operatorname {pinRep}(h)=\rho (h).\] Thus the group actions introduce no new formula on \(S\); they are the same Clifford action with a smaller domain. In particular, any equation proved for the action of the underlying Clifford element applies to its Spin or Pin restriction.

                                                                                                                                                    Example. The rank-one polarized model [meinrenken2013clifford, Section 3.2.4, Theorem 3.3, p. 59] [fcap-001P]

                                                                                                                                                      Let \(W=Ke\) and choose \(e'\in W'\) with \(B_Q(e,e')=1\). In the ordered basis \((1,e)\) of \(S=\bigwedge W\), creation and contraction are \[\varepsilon _e= \begin {pmatrix}0&0\\1&0\end {pmatrix}, \qquad \iota _{e'}= \begin {pmatrix}0&1\\0&0\end {pmatrix}.\] Both are nilpotent, and \[\varepsilon _e\iota _{e'}+\iota _{e'}\varepsilon _e=I_2.\] Together with their products they give the four matrix units of \(\operatorname {End}_K(S)\). This is the rank-one calculation in Meinrenken's generation proof and a specialization of the general relation in Lemma [fcap-001J]. The formalized ingredients are TauCeti.SpinPolarizationData.contract_wedge and TauCeti.ExteriorAlgebra.creation_contraction_adjoin_eq_top; neither declaration formalizes this displayed choice of basis.

                                                                                                                                                      Remark. Horizons beyond the exterior model [meinrenken2013clifford, Section 3.2.4, Theorem 3.3, pp. 59--60]; [kostant1997clifford, Section 2.4, Theorem 8, pp. 286--287]; [lawson2016spin, I.2, pp. 13--19] [fcap-0017]

                                                                                                                                                        The exterior action constructed above stops before several classical consequences in representation theory. Over a split field, irreducibility and the decomposition into two half-spin modules require further hypotheses and arguments; Meinrenken proves these results after establishing that the Clifford action is an isomorphism. The currently open TauCeti half-spin work is therefore not represented by a Lean marker here.

                                                                                                                                                        The generic mathematics of differentiating a smooth Lie-group homomorphism is developed in § [fcap-001Q]. What remains missing for the Spin cover is more specific: compatible Lie-group structures on TauCeti's abstract \(\operatorname {Spin}(V)\) and \(SO(V)\), followed by the identification of their specialized differential with the algebraic quadratic action above. The open TauCeti PR linked in Remark [fcap-001W] proposes only the generic Lie functor.

                                                                                                                                                        Highest weights, triality, and the Bott-periodic real table also belong to later layers. Kostant supplies the differential in the classical complex setting, and Lawson--Michelsohn treat the real Pin and Spin groups. None of these horizons follows merely from the algebraic restrictions \(\operatorname {spinRep}\) and \(\operatorname {pinRep}\).

                                                                                                                                                        Hyperbolic recurrence and real signatures [fcap-0010]

                                                                                                                                                          A positive and a negative generator form a hyperbolic plane. Adjoining that plane tensors the Clifford algebra with two-by-two real matrices. Iteration removes the common part of a real signature, while a sign switch gives a complementary one-sided recurrence. These are algebraic steps toward the real classification; the real Pin and Spin groups follow a separate branch through the double-cover theory.

                                                                                                                                                          § [ca-0001]

                                                                                                                                                          Convention. Real signature and Clifford signs [chevalley1954algebraic, II.2.9, pp. 65--66] [fcap-0011]
                                                                                                                                                          realCliffordFormrealCliffordForm_apply
                                                                                                                                                          L∃∀N

                                                                                                                                                            For \(p,q\ge 0\), put \[Q_{p,q}(x)=\sum _{i<p}x_i^2-\sum _{p\le i<p+q}x_i^2\] on \(\mathbb {R}^{p+q}\), and write \(\mathcal {C}\kern -2pt\ell _{p,q}\) for \(\mathcal {C}\kern -2pt\ell (Q_{p,q})\). Thus the first \(p\) Clifford generators square to \(+1\), and the last \(q\) square to \(-1\). This agrees with Chevalley's convention for the quadratic form and with his positive/negative inertia indices.

                                                                                                                                                            Lawson and Michelsohn use the same signature \(q_{r,s}\) but impose \(v^2=-q_{r,s}(v)1\) [lawson2016spin, I.3, Proposition 3.1, p. 21]. Therefore the algebras are related by the exact index swap \[\mathcal {C}\kern -2pt\ell _{p,q}=\mathcal {C}\kern -2pt\ell ^{\mathrm {Lawson}}_{q,p}.\] The recurrence below adds one index of each sign, so it is invariant under this swap.

                                                                                                                                                            Definition. The hyperbolic plane [lawson2016spin, I.4, Theorem 4.1 and (4.3), pp. 25--26] [fcap-0012]
                                                                                                                                                            realCliffordForm_one_one_applyrealBottSplitIsometry
                                                                                                                                                            L∃∀N

                                                                                                                                                              The real hyperbolic plane is \[H=(\mathbb {R}^2,Q_{1,1}),\qquad Q_{1,1}(s,t)=s^2-t^2.\] Its coordinate generators \(e_+\) and \(e_-\) satisfy \[e_+^2=1,\qquad e_-^2=-1,\qquad e_+e_-=-e_-e_+.\] For every signature, separating the last positive and negative coordinates gives an isometry \[(\mathbb {R}^{p+q+2},Q_{p+1,q+1}) \simeq (\mathbb {R}^{p+q},Q_{p,q})\perp H.\] The coordinate order is fixed: the retained \(p\) positive and \(q\) negative axes form the first factor, and the last positive and last negative axes form \(H\).

                                                                                                                                                              Theorem. The hyperbolic matrix recurrence [lawson2016spin, I.4, Theorem 4.1, (4.3), pp. 25--26] [fcap-0013]
                                                                                                                                                              hyperbolicEquivTensorrealCliffordBottEquiv_ι
                                                                                                                                                              L∃∀N

                                                                                                                                                                For finite-dimensional quadratic spaces, Lawson--Michelsohn state the signature recurrence \[\mathcal {C}\kern -2pt\ell _{p+1,q+1}\simeq _{\mathbb {R}\text {-alg}} \mathcal {C}\kern -2pt\ell _{p,q}\otimes _{\mathbb {R}}M_2(\mathbb {R}).\] TauCeti extends the recurrence to any real quadratic module \((M,Q)\) and supplies an explicit formula on generators: \[\mathcal {C}\kern -2pt\ell (Q\perp Q_{1,1})\simeq \mathcal {C}\kern -2pt\ell (Q)\otimes _{\mathbb {R}}M_2(\mathbb {R}).\] With \[\sigma _x=\begin {pmatrix}0&1\\1&0\end {pmatrix},\] the equivalence sends a generator \((m,(s,t))\) to \[\iota _Q(m)\otimes \sigma _x +1\otimes \begin {pmatrix}s&t\\-t&-s\end {pmatrix}.\] The first summand squares to \(Q(m)\), the second to \(s^2-t^2\), and the two anticommute. The universal property therefore gives the forward algebra map. In the other direction, the original Clifford algebra and the matrix algebra act through commuting algebra maps on the hyperbolic Clifford algebra; their tensor lift is inverse to the forward map. The two composites are checked on Clifford generators and pure tensors, which is why TauCeti's extension needs no finite-dimensional hypothesis. Chevalley's split-matrix theorem and orthogonal-sum calculation supply the classical structural mechanism [chevalley1954algebraic, II.2.1 and II.2.5, pp. 42--46].

                                                                                                                                                                Writing the displayed generator formula as \(f\), its universal extension is summarized by the commuting diagram

                                                                                                                                                                Lemma. Finite hyperbolic reduction [chevalley1954algebraic, II.2.9, pp. 65--66] [fcap-0014]
                                                                                                                                                                realCliffordBottIterEquivrealCliffordSignatureReductionEquiv
                                                                                                                                                                L∃∀N

                                                                                                                                                                  Chevalley splits a finite-dimensional real quadratic space into hyperbolic planes and a definite remainder. TauCeti combines that classical reduction with iteration of Theorem [fcap-0013] and Kronecker equivalences to synthesize the explicit tensor and matrix packaging below. Iterating \(n\) times gives \[\mathcal {C}\kern -2pt\ell _{p+n,q+n}\simeq \mathcal {C}\kern -2pt\ell _{p,q}\otimes _{\mathbb {R}}M_{2^n}(\mathbb {R}).\] Taking \(n=\min (p,q)\) removes the common positive and negative part: \[\mathcal {C}\kern -2pt\ell _{p,q}\simeq \mathcal {C}\kern -2pt\ell _{p-n,q-n}\otimes _{\mathbb {R}}M_{2^n}(\mathbb {R}), \qquad n=\min (p,q).\] Thus if \(p\le q\), the residual algebra is \(\mathcal {C}\kern -2pt\ell _{0,q-p}\); if \(q\le p\), it is \(\mathcal {C}\kern -2pt\ell _{p-q,0}\). The matrix factors combine through the Kronecker equivalence \[M_{2^a}(\mathbb {R})\otimes M_{2^b}(\mathbb {R}) \simeq M_{2^{a+b}}(\mathbb {R}).\] Chevalley supplies the quadratic-space decomposition. The displayed \(M_{2^n}\) packaging and its named equivalences are TauCeti's formalized synthesis.

                                                                                                                                                                  Theorem. The signature-switch recurrence [lawson2016spin, I.4, Theorem 4.1 and (4.1), pp. 25--26] [fcap-001X]
                                                                                                                                                                  realCliffordSignatureSwitchRecurrenceEquiv
                                                                                                                                                                  L∃∀N

                                                                                                                                                                    With the TauCeti signature convention of Convention [fcap-0011], there is an algebra equivalence \[\mathcal {C}\kern -2pt\ell _{p+2,q}\simeq _{\mathbb R\text {-alg}} \mathcal {C}\kern -2pt\ell _{q,p}\otimes _{\mathbb R}M_2(\mathbb R).\] The construction first separates the last positive coordinate from \(Q_{p+2,q}\). Adjoining that positive line permits a Clifford sign switch; negating \(Q_{p+1,q}\) exchanges its positive and negative coordinate blocks. The resulting form is \(Q_{q+1,p+1}\), to which the hyperbolic recurrence of Theorem [fcap-0013] applies.

                                                                                                                                                                    The accompanying generator theorem SignatureSwitchRecurrenceEquiv_ι records this composition through the positive-coordinate splitter, the sign-switch isometry, and the generator formula for the hyperbolic equivalence. It fixes the equivalence on the canonical Clifford generators rather than asserting only that some algebra isomorphism exists.

                                                                                                                                                                    After converting between the two signature conventions, inverting Lawson--Michelsohn's equation (4.1), using \(\mathcal {C}\kern -2pt\ell ^{\mathrm {Lawson}}_{0,2}\cong M_2(\mathbb R)\), and swapping the indices yields the displayed algebra isomorphism. Their equation (4.3) is instead the mixed \((1,1)\) recurrence used in Theorem [fcap-0013]. Chevalley's split-matrix and orthogonal-sum constructions give the same structural ingredients [chevalley1954algebraic, II.2.1 and II.2.5, pp. 42--46]. The exact splitter composition and generator formula are additional data recorded by TauCeti.

                                                                                                                                                                    Remark. Why algebraic periodicity is a separate branch [chevalley1954algebraic, II.2.1, II.2.5, and II.2.9, pp. 42--46, 65--66]; [lawson2016spin, I.4, Theorems 4.1 and 4.3, pp. 25--29] [fcap-001Y]

                                                                                                                                                                      The recurrences in Theorem [fcap-0013], Lemma [fcap-0014], and Theorem [fcap-001X] use Clifford universal properties, orthogonal sums, tensor products, coordinate isometries, and the real base entries. They do not use the Spin representation, the structure theorem obtained from a spinor module, or the Pin and Spin double covers. This is the algebraic branch of Layer 7.

                                                                                                                                                                      The real groups \(\operatorname {Pin}(p,q)\) and \(\operatorname {Spin}(p,q)\) form a different branch. Their actions, kernels, and algebraic extensions specialize the group theory developed in § [fcap-0007], and therefore genuinely consume the Layer-2 Pin/Spin work. The distinction between these branches is the dependency correction proposed in TauCetiRoadmap PR 225. It changes the order in which the mathematics can be built; it does not turn the roadmap proposal itself into a formal theorem.

                                                                                                                                                                      Example. Four real Clifford base entries [lawson2016spin, I.4, Theorem 4.3 and Tables I--II, pp. 27--29] [fcap-0015]
                                                                                                                                                                      realCliffordOneZeroEquivProdrealCliffordZeroOneEquivComplexrealCliffordZeroTwoEquivQuaternionrealCliffordOneOneEquivMatrix
                                                                                                                                                                      L∃∀N

                                                                                                                                                                        With \(\mathcal {C}\kern -2pt\ell _{0,0}\simeq \mathbb {R}\) as the scalar anchor, the signature convention of Convention [fcap-0011] gives four nontrivial base entries: \[\begin {aligned} \mathcal {C}\kern -2pt\ell _{0,0}&\simeq \mathbb {R}, & \mathcal {C}\kern -2pt\ell _{1,0}&\simeq \mathbb {R}\times \mathbb {R}, & \mathcal {C}\kern -2pt\ell _{0,1}&\simeq \mathbb {C},\\ \mathcal {C}\kern -2pt\ell _{0,2}&\simeq \mathbb {H}, & \mathcal {C}\kern -2pt\ell _{1,1}&\simeq M_2(\mathbb {R}). \end {aligned}\] For \(\mathcal {C}\kern -2pt\ell _{0,2}\), the two negative generators map to the quaternion units \(i\) and \(j\); their product maps to \(k\). Thus they square to \(-1\) and anticommute, as required by the Clifford relations. The exact generator map is recorded by TauCeti.realCliffordZeroTwoEquivQuaternion_ι.

                                                                                                                                                                        For \(\mathcal {C}\kern -2pt\ell _{1,1}\), the positive and negative generators may be represented by \[e_+\longmapsto \begin {pmatrix}1&0\\0&-1\end {pmatrix}, \qquad e_-\longmapsto \begin {pmatrix}0&1\\-1&0\end {pmatrix}.\] Their squares are \(+I\) and \(-I\), and they anticommute. The last equivalence is also the case \(p=q=0\) of Theorem [fcap-0013]. The index swap in Convention [fcap-0011] explains why Lawson's one-generator table lists \(\mathbb {C}\) and \(\mathbb {R}\times \mathbb {R}\) in the opposite order.

                                                                                                                                                                        Remark. What the recurrence does not classify [fcap-0016]

                                                                                                                                                                          Hyperbolic reduction determines the matrix factor coming from matched positive and negative axes. It leaves a one-sided algebra \(\mathcal {C}\kern -2pt\ell _{r,0}\) or \(\mathcal {C}\kern -2pt\ell _{0,r}\). The signature-switch recurrence of Theorem [fcap-001X] provides a second move, and Example [fcap-0015] fixes the first real, complex, quaternionic, and matrix entries. These facts still have to be assembled into recurrences that close on each one-sided axis.

                                                                                                                                                                          A reviewed local candidate called SPINREP-050 establishes the quaternion recurrence \[\mathcal {C}\kern -2pt\ell _{p,q+2}\simeq \mathcal {C}\kern -2pt\ell _{q,p}\otimes _{\mathbb R}\mathbb H,\] and another local candidate, SPINREP-053, iterates the recurrence chain to \[\mathcal {C}\kern -2pt\ell _{p+8,q}\simeq \mathcal {C}\kern -2pt\ell _{p,q}\otimes _{\mathbb R}M_{16}(\mathbb R).\] Neither candidate is a merged TauCeti declaration or a public TauCeti pull request, so neither receives a Lean marker here.

                                                                                                                                                                          The residue-indexed mod-eight classification table remains unformalized. In particular, the mixed \((1,1)\) recurrence alone only removes matched axes; it cannot classify the one-sided remainder. Lawson--Michelsohn give the full classical periodicity and table in [lawson2016spin, I.4, Theorem 4.3 and Tables I--II, pp. 27--29].

                                                                                                                                                                          Related

                                                                                                                                                                            Notes on Clifford Algebras [ca-0001]
                                                                                                                                                                            📄PDF
                                                                                                                                                                            Readers may also check out Compendium on Spin groups.

                                                                                                                                                                            Preliminaries [ca-000N]

                                                                                                                                                                              This section introduces the algebraic environment of Clifford Algebra, covering vector spaces, groups, algebras, representations, modules, multilinear algebras, quadratic forms, filtrations and graded algebras.

                                                                                                                                                                              The material in this section should be familiar to the readers, but it is worth reading through it to become familiar with the notation and terminology that is used, as well as their counterparts in Lean, which usually require some additional treatment, both mathematically and technically (probably applicable to other formal proof verification systems).

                                                                                                                                                                              Details can be found in the references in corresponding section, or you may use the L∃∀N button to check the corresponding \(\textsf {Mathlib}\) document and Lean 4 source code.

                                                                                                                                                                              In this section, we follow [jadczyk2019notes], with supplements from [garling2011clifford][chen2016infinitely], and extensive modifications to match the counterparts in Lean's \(\textsf {Mathlib}\).

                                                                                                                                                                              basics: from groups to modules [ca-000P]

                                                                                                                                                                                Convention. definition style [ca-000O]

                                                                                                                                                                                  In this document, we unify the informal mathematical language for a definition to:

                                                                                                                                                                                  Let \(X\) be a concept \(X\).

                                                                                                                                                                                  A concept \(Z\) is a set/pair/triple/tuple \((Z, \mathtt {op}, ...)\), satisfying:

                                                                                                                                                                                  1. \(Z\) is a concept \(Y\) over \(X\) under op .
                                                                                                                                                                                  2. formula for all elements in \(Z\) ( property ).
                                                                                                                                                                                  3. for each element in concept \(X\), there exists element such that formula for all elements in concept \(Z\).
                                                                                                                                                                                  4. op is called op name, for all elements in \(Z\), we have
                                                                                                                                                                                    1. formula
                                                                                                                                                                                    2. formula
                                                                                                                                                                                    ( property ).

                                                                                                                                                                                  By default, \(X\) is a set, op is a binary operation on \(X\).

                                                                                                                                                                                  Definition. group [garling2011clifford, 1.1] [ca-000Q]
                                                                                                                                                                                  GroupAddGroup
                                                                                                                                                                                  L∃∀N

                                                                                                                                                                                    A group is a pair \((G, *)\), satisfying:

                                                                                                                                                                                    1. \((a * b) * c = a * (b * c)\) for all \(a, b, c \in G\) (associativity).
                                                                                                                                                                                    2. there exists \(1 \in G\) such that \[1 * a = a * 1 = a\] for all \(a \in G\).
                                                                                                                                                                                    3. for each \(a \in G\), there exists \(a^{-1} \in G\) such that \[a * a^{-1} = a^{-1} * a = 1\].

                                                                                                                                                                                    Remark.  [ca-000R]

                                                                                                                                                                                      It then follows that \(1\), the identity element, is unique, and that for each \(g \in G\) the inverse \(g^{-1}\) is unique. A group G is abelian, or commutative, if \(g * h = h * g\) for all \(g, h \in G\).

                                                                                                                                                                                      Notation. product [ca-000S]

                                                                                                                                                                                        In literatures, the binary operation of a group is usually called a product. It's denoted by juxtaposition \(g h\), and is understood to be a mapping \((g, h) \mapsto g * h\) from \(G \times G\) to \(G\).

                                                                                                                                                                                        Here we use an explicit symbol for the operation. It can be denoted multiplicatively as \(*\) in Group or additively as \(+\) in AddGroup, where the identity element will be denoted by \(1\) or \(0\), respectively.

                                                                                                                                                                                        Sometimes we use notations with subscripts (e.g. \(*_G\), \(1_G\)) to indicate where they are.

                                                                                                                                                                                        \(\textsf {Mathlib}\) encodes the mapping \(G \times G \to G\) as \(G \to G \to G\), it is understood to be \(G \to (G \to G)\), that sends \(g \in G\) to a mapping that sends \(h \in G\) to \(g * h \in G\).

                                                                                                                                                                                        Furthermore, a mathematical construct, e.g. a group, is represented by a "type", as Lean has a dependent type theory foundation, see [carneiro2019type] and [ullrich2023extensible, sec. 3.2].

                                                                                                                                                                                        Definition. monoid [ca-000T]
                                                                                                                                                                                        MonoidAddMonoid
                                                                                                                                                                                        L∃∀N

                                                                                                                                                                                          A monoid is a pair \((R, *)\), satisfying:

                                                                                                                                                                                          1. \((a * b) * c = a * (b * c)\) for all \(a, b, c \in R\) (associativity).
                                                                                                                                                                                          2. there exists an element \(1 \in R\) such that \(1 * a = a * 1 = a\) for all \(a \in R\)
                                                                                                                                                                                            3. i.e. \(1\) is the multiplicative identity (neutral element).

                                                                                                                                                                                          Definition. ring [jadczyk2019notes, 1.1] [ca-000U]
                                                                                                                                                                                          RingCommRingCommSemiring
                                                                                                                                                                                          L∃∀N

                                                                                                                                                                                            A ring is a triple \((R, +, *)\), satisfying:

                                                                                                                                                                                            1. \(R\) is a commutative group under \(+\).
                                                                                                                                                                                            2. \(R\) is a monoid under \(*\).
                                                                                                                                                                                            3. for all \(a, b, c \in R\), we have
                                                                                                                                                                                              1. \(a * (b + c) = a * b + a * c\)
                                                                                                                                                                                              2. \((a + b) * c = a * c + b * c\)
                                                                                                                                                                                              (left and right distributivity over \(+\)).

                                                                                                                                                                                            Remark.  [ca-000V]

                                                                                                                                                                                              In applications to Clifford algebras \(R\) will be always assumed to be commutative.

                                                                                                                                                                                              Definition. division ring [ca-000W]
                                                                                                                                                                                              DivisionRing
                                                                                                                                                                                              L∃∀N

                                                                                                                                                                                                A division ring is a ring \((R, +, *)\), satisfying:

                                                                                                                                                                                                1. \(R\) contains at least 2 elements.
                                                                                                                                                                                                2. for all \(a \neq 0\) in \(R\), there exists a multiplicative inverse \(a^{-1} \in R\) such that
                                                                                                                                                                                                  3. \[ a * a^{-1} = a^{-1} * a = 1 \]

                                                                                                                                                                                                Definition. module [jadczyk2019notes, 1.3] [ca-000X]
                                                                                                                                                                                                Module
                                                                                                                                                                                                L∃∀N

                                                                                                                                                                                                  Let \(R\) be a commutative ring. A module over \(R\), called an \(R\)-module, is a pair \((M, \bullet )\), satisfying:

                                                                                                                                                                                                  1. M is a group under \(+\).
                                                                                                                                                                                                  2. \(\bullet : R \to M \to M\) is called scalar multiplication, for every \(a, b \in R\), \(x, y \in M\), we have
                                                                                                                                                                                                    1. \(a \bullet (x + y) = a \bullet x + b \bullet y\)
                                                                                                                                                                                                    2. \((a + b) \bullet x = a \bullet x + b \bullet x\)
                                                                                                                                                                                                    3. \(a * (b \bullet x)=(a * b) \bullet x\)
                                                                                                                                                                                                    4. \(1_R \bullet x = x\)

                                                                                                                                                                                                  Remark.  [ca-000Y]

                                                                                                                                                                                                    The notation of scalar multiplication is generalized as heterogeneous scalar multiplication HMul in \(\textsf {Mathlib}\): \[ \bullet : \alpha \to \beta \to \gamma \] where \(\alpha \), \(\beta \), \(\gamma \) are different types.

                                                                                                                                                                                                    Definition. vector space [jadczyk2019notes, 1.5] [ca-000Z]
                                                                                                                                                                                                    Module
                                                                                                                                                                                                    L∃∀N

                                                                                                                                                                                                      If \(R\) is a division ring, then a module \(M\) over \(R\) is called a vector space.

                                                                                                                                                                                                      Remark.  [ca-0010]

                                                                                                                                                                                                        For generality, \(\textsf {Mathlib}\) uses Module throughout for vector spaces, particularly, for a vector space \(V\), it's usually declared as

                                                                                                                                                                                                        /-- Let $K$ be a division ring, a module $V$ over $K$ is a vector space where being a module requires $V$ to be a commutative group over $+$. -/ variable [DivisionRing K] [AddCommGroup V] [Module K V]

                                                                                                                                                                                                        For definitions/theorems about it, and most of them can be found under Mathlib.LinearAlgebra e.g. LinearIndependent.

                                                                                                                                                                                                        Definition. submodule [ca-0011]

                                                                                                                                                                                                          A submodule \(N\) of \(M\) is a module \(N\) such that every element of \(N\) is also an element of \(M\). If \(M\) is a vector space then \(N\) is called a subspace.

                                                                                                                                                                                                          Definition. dual module [ca-0012]
                                                                                                                                                                                                          Module.Dual
                                                                                                                                                                                                          L∃∀N

                                                                                                                                                                                                            The dual module \(M^* : M \to _{l[R]} R\) is the \(R\)-module of all linear maps from \(M\) to \(R\).

                                                                                                                                                                                                            algebras [ca-0013]

                                                                                                                                                                                                              Definition. ring homomorphism [chen2016infinitely, 4.5.1] [ca-0014]
                                                                                                                                                                                                              RingHomRingHomClassalgebraMap
                                                                                                                                                                                                              L∃∀N

                                                                                                                                                                                                                Let \((\alpha , +_\alpha , *_\alpha )\) and \((\beta , +_\beta , *_\beta )\) be rings. A ring homomorphism from \(\alpha \) to \(\beta \) is a map \(\mathit {1} : \alpha \to _{+*} \beta \) such that

                                                                                                                                                                                                                1. \(\mathit {1}(x +_{\alpha } y) = \mathit {1}(x) +_{\beta } \mathit {1}(y)\) for each \(x,y \in \alpha \).
                                                                                                                                                                                                                2. \(\mathit {1}(x *_{\alpha } y) = \mathit {1}(x) *_{\beta } \mathit {1}(y)\) for each \(x,y \in \alpha \).
                                                                                                                                                                                                                3. \(\mathit {1}(1_{\alpha }) = 1_{\beta }\).

                                                                                                                                                                                                                Definition. isomorphism, endomorphism, automorphism [ca-0015]

                                                                                                                                                                                                                  Isomorphism \(A \cong B\) is a bijective homomorphism \(\phi : A \to B\) (it follows that \(\phi ^{-1} : B \to A\) is also a homomorphism).

                                                                                                                                                                                                                  Endomorphism is a homomorphism from an object to itself, denoted \(\operatorname {End}(A)\).

                                                                                                                                                                                                                  Automorphism is an endomorphism which is also an isomorphism, denoted \(\operatorname {Aut}(A)\).

                                                                                                                                                                                                                  Definition. algebra [ca-0016]
                                                                                                                                                                                                                  Algebra
                                                                                                                                                                                                                  L∃∀N

                                                                                                                                                                                                                    Let \(R\) be a commutative ring. An algebra \(A\) over \(R\) is a pair \((A, \bullet )\), satisfying:

                                                                                                                                                                                                                    1. \(A\) is a ring under \(*\).
                                                                                                                                                                                                                    2. there exists a ring homomorphism from \(R\) to \(A\), denoted \(\mathit {1} : R \to _{+*} A\).
                                                                                                                                                                                                                    3. \(\bullet : R \to M \to M\) is a scalar multiplication
                                                                                                                                                                                                                    4. for every \(r \in R\), \(x \in A\), we have
                                                                                                                                                                                                                      1. \(r * x = x * r\) (commutativity between \(R\) and \(A\))
                                                                                                                                                                                                                      2. \(r \bullet x = r * x\) (definition of scalar multiplication)
                                                                                                                                                                                                                      where we omitted that the ring homomorphism \(\mathit {1}\) is applied to \(r\) before each multiplication.

                                                                                                                                                                                                                    Notation.  [ca-0017]

                                                                                                                                                                                                                      Following literatures, for \(r \in R\), usually we write \(\mathit {1}_A(r) : R \to _{+*} A\) as a product \(r \mathit {1}_A\) if not omitted, while they are written as a call to algebraMap _ _ r in \(\textsf {Mathlib}\), which is defined to be Algebra.toRingHom r.

                                                                                                                                                                                                                      Remark.  [ca-0018]

                                                                                                                                                                                                                        The definition above (adopted in \(\textsf {Mathlib}\)) is more general than the definition in literature (e.g. [jadczyk2019notes, 1.6]):

                                                                                                                                                                                                                        Let \(R\) be a commutative ring. An algebra \(A\) over \(R\) is a pair \((M, *)\), satisfying:

                                                                                                                                                                                                                        1. \(A\) is a module \(M\) over \(R\) under \(+\) and \(\bullet \).
                                                                                                                                                                                                                        2. \(A\) is a ring under \(*\).
                                                                                                                                                                                                                        3. For \(x, y \in A, a \in R\), we have
                                                                                                                                                                                                                          4. \[ a \bullet (x * y) = (a \bullet x) * y = x * (a \bullet y) \]

                                                                                                                                                                                                                        See Implementation notes in Algebra for details.

                                                                                                                                                                                                                        Remark.  [ca-0019]

                                                                                                                                                                                                                          What's simply called algebra is actually associative algebra with identity, a.k.a. associative unital algebra. See the red herring principle for more about such phenomenon for naming, particularly the example of (possibly) nonassociative algebra.

                                                                                                                                                                                                                          Definition. algebra homomorphism [ca-001A]
                                                                                                                                                                                                                          AlgHom
                                                                                                                                                                                                                          L∃∀N

                                                                                                                                                                                                                            Let \(A\) and \(B\) be \(R\)-algebras. \(\mathit {1}_A\) and \(\mathit {1}_B\) are ring homomorphisms from \(R\) to \(A\) and \(B\), respectively. A algebra homomorphism from \(A\) to \(B\) is a map \(f : \alpha \to _{a} \beta \) such that

                                                                                                                                                                                                                            1. \(f\) is a ring homomorphism
                                                                                                                                                                                                                            2. \(f(\mathit {1}_{A}(r)) = \mathit {1}_{B}(r)\) for each \(r \in R\)

                                                                                                                                                                                                                            Definition. ring quotient [ca-001B]
                                                                                                                                                                                                                            RingQuot
                                                                                                                                                                                                                            L∃∀N

                                                                                                                                                                                                                              Let \(R\) be a non-commutative ring, \(r\) an arbitrary equivalence relation on \(R\). The ring quotient of \(R\) by \(r\) is the quotient of \(R\) by the strengthen equivalence relation of \(r\) such that for all \(a, b, c\) in \(R\):

                                                                                                                                                                                                                              1. \(a + c \sim b + c\) if \(a \sim b\)
                                                                                                                                                                                                                              2. \(a * c \sim b * c\) if \(a \sim b\)
                                                                                                                                                                                                                              3. \(a * b \sim a * c\) if \(b \sim c\)
                                                                                                                                                                                                                              i.e. the equivalence relation is compatible with the ring operations \(+\) and \(*\).

                                                                                                                                                                                                                              Remark.  [ca-001C]

                                                                                                                                                                                                                                As ideals haven't been formalized for the non-commutative case, \(\textsf {Mathlib}\) uses RingQuot in places where the quotient of non-commutative rings by ideal is needed. The universal properties of the quotient are proven, and should be used instead of the definition that is subject to change.

                                                                                                                                                                                                                                Definition. free algebra [ca-001D]
                                                                                                                                                                                                                                FreeAlgebraFreeAlgebra.PreFreeAlgebra.Rel
                                                                                                                                                                                                                                L∃∀N

                                                                                                                                                                                                                                  Let \(X\) be an arbitrary set. An free \(R\)-algebra on \(X\) (or "generated by \(X\)"), named \(A\), is the ring quotient of the following inductively constructed set \(A_{\mathtt {pre}}\)

                                                                                                                                                                                                                                  1. for all \(x\) in \(X\), there exists a map \(X \to A_{\mathtt {pre}}\).
                                                                                                                                                                                                                                  2. for all \(r\) in \(R\), there exists a map \(R \to A_{\mathtt {pre}}\).
                                                                                                                                                                                                                                  3. for all \(a, b\) in \(A_{\mathtt {pre}}\), \(a + b\) is in \(A_{\mathtt {pre}}\).
                                                                                                                                                                                                                                  4. for all \(a, b\) in \(A_{\mathtt {pre}}\), \(a * b\) is in \(A_{\mathtt {pre}}\).
                                                                                                                                                                                                                                  by that equivalence relation that makes \(A\) an \(R\)-algebra, namely:
                                                                                                                                                                                                                                  1. there exists a ring homomorphism from \(R\) to \(A_{\mathtt {pre}}\), denoted \(R \to _{+*} A_{\mathtt {pre}}\).
                                                                                                                                                                                                                                  2. \(A\) is a commutative group under \(+\).
                                                                                                                                                                                                                                  3. \(A\) is a monoid under \(*\).
                                                                                                                                                                                                                                  4. left and right distributivity under \(*\) over \(+\).
                                                                                                                                                                                                                                  5. \(0 * a \sim a * 0 \sim 0\).
                                                                                                                                                                                                                                  6. for all \(a, b, c\) in \(A\), if \(a \sim b\), we have
                                                                                                                                                                                                                                    1. \(a + c \sim b + c\)
                                                                                                                                                                                                                                    2. \(c + a \sim c + b\)
                                                                                                                                                                                                                                    3. \(a * c \sim b * c\)
                                                                                                                                                                                                                                    4. \(c * a \sim c * b\)
                                                                                                                                                                                                                                    (compatibility with the ring operations \(+\) and \(*\))

                                                                                                                                                                                                                                  Remark.  [ca-001E]

                                                                                                                                                                                                                                    Similar to Remark [ca-0019], what we defined here is the free (associative, unital) \(R\)-algebra on \(X\), it can be denoted \(R\langle X \rangle \), expressing that it's freely generated by \(R\) and \(X\), where \(X\) is the set of generators.

                                                                                                                                                                                                                                    Definition. linear map [ca-001F]
                                                                                                                                                                                                                                    LinearMap
                                                                                                                                                                                                                                    L∃∀N

                                                                                                                                                                                                                                      Let \(R, S\) be rings, \(M\) an \(R\)-module, \(N\) an \(S\)-module. A linear map from \(M\) to \(N\) is a function \(f : M \to _{l} N\) over a ring homomorphism \(\sigma : R \to _{+*} S\), satisfying:

                                                                                                                                                                                                                                      1. \(f(x + y) = f(x) + f(y)\) for all \(x, y \in M\).
                                                                                                                                                                                                                                      2. \(f(r \bullet x) = \sigma (r) \bullet f(x)\) for all \(r \in R\), \(x \in M\).

                                                                                                                                                                                                                                      Remark. Lin [ca-001G]

                                                                                                                                                                                                                                        The set of all linear maps from \(M\) to \(M'\) is denoted \(\operatorname {Lin}(M, M')\), and \(\operatorname {Lin}(M)\) for mapping from \(M\) to itself. \(\operatorname {Lin}(M)\) is an endomorphism.

                                                                                                                                                                                                                                        Definition. tensor algebra [ca-001H]
                                                                                                                                                                                                                                        TensorAlgebra
                                                                                                                                                                                                                                        L∃∀N

                                                                                                                                                                                                                                          Let \(A\) be a free \(R\)-algebra generated by module \(M\), let \(\iota : M \to A\) denote the map from \(M\) to \(A\). An tensor algebra over \(M\) (or "of \(M\)") \(T\) is the ring quotient of the free \(R\)-algebra generated by \(M\), by the equivalence relation satisfying:

                                                                                                                                                                                                                                          1. for all \(a, b\) in \(M\), \(\iota (a + b) \sim \iota (a) + \iota (b)\).
                                                                                                                                                                                                                                          2. for all \(r\) in \(R\), \(a\) in \(M\), \(\iota (r \bullet a) \sim r * \iota (a)\).
                                                                                                                                                                                                                                          i.e. making the inclusion of \(M\) into an \(R\)-linear map.

                                                                                                                                                                                                                                          Remark.  [ca-001I]

                                                                                                                                                                                                                                            The definition above is equivalent to the following definition in literature (e.g. [jadczyk2019notes, 1.7]):

                                                                                                                                                                                                                                            Let \(M\) be a module over \(R\). An algebra \(T\) is called a tensor algebra over \(M\) (or "of \(M\)") if it satisfies the following universal properties:

                                                                                                                                                                                                                                            1. \(T\) is an algebra containing \(M\) as a submodule, and it is generated by \(M\),
                                                                                                                                                                                                                                            2. Every linear mapping \(\lambda \) of \(M\) into an algebra \(A\) over \(R\), can be extended to
                                                                                                                                                                                                                                              3. a homomorphism \(\theta \) of \(T\) into \(A\).

                                                                                                                                                                                                                                            Forms [ca-000L]

                                                                                                                                                                                                                                              Definition. bilinear form [ca-0003]
                                                                                                                                                                                                                                              BilinForm
                                                                                                                                                                                                                                              L∃∀N

                                                                                                                                                                                                                                                Let \(R\) be a ring, \(M\) an \(R\)-module.

                                                                                                                                                                                                                                                An bilinear form \(B\) over \(M\) is a map \(B : M \to M \to R\), satisfying:

                                                                                                                                                                                                                                                1. \( B(x + y, z) = B(x, z) +B(y, z) \)
                                                                                                                                                                                                                                                2. \( B(x, y + z) = B(x, y) +B(x, z) \)
                                                                                                                                                                                                                                                3. \( B(a \bullet x, y) = a * B(x, y)\)
                                                                                                                                                                                                                                                4. \( B(x, a \bullet y) = a * B(x, y)\)
                                                                                                                                                                                                                                                for all \(a \in R, x, y, z \in M\).

                                                                                                                                                                                                                                                Definition. quadratic form [jadczyk2019notes, 1.9] [ca-0004]
                                                                                                                                                                                                                                                QuadraticFormQuadraticForm.polar
                                                                                                                                                                                                                                                L∃∀N

                                                                                                                                                                                                                                                  Let \(R\) be a commutative ring, \(M\) a \(R\)-module.

                                                                                                                                                                                                                                                  An quadratic form \(Q\) over \(M\) is a map \(Q : M \to R\), satisfying:

                                                                                                                                                                                                                                                  1. \( Q(a \bullet x) = a * a * Q(x)\) for all \(a \in R, x \in M\).
                                                                                                                                                                                                                                                  2. there exists a companion bilinear form \(B : M \to M \to R\), such that \(Q(x + y) = Q(x) + Q(y) + B(x, y)\)

                                                                                                                                                                                                                                                  In [jadczyk2019notes], the bilinear form is denoted \(\Phi \), and called the polar form associated with the quadratic form \(Q\), or simply the polar form of \(Q\).

                                                                                                                                                                                                                                                  Remark.  [ca-0005]

                                                                                                                                                                                                                                                    This notion generalizes to commutative semirings using the approach in [izhakian2016supertropical].

                                                                                                                                                                                                                                                    Clifford Algebra [ca-000M]

                                                                                                                                                                                                                                                      Here we provide a detailed account of the formalization of Clifford Algebra [hestenes2012clifford] in the Lean 4 theorem prover and programming language [moura2021lean][moura2015lean][ullrich2023extensible] and using its Mathematical Library \(\textsf {Mathlib}\) [mathlib2020lean].

                                                                                                                                                                                                                                                      The primary references of the formalization are [wieser2022formalizing] and [wieser2024formalizing].

                                                                                                                                                                                                                                                      Definition [ca-000F]

                                                                                                                                                                                                                                                        Definition. Clifford algebra [wieser2022formalizing] [ca-0006]
                                                                                                                                                                                                                                                        CliffordAlgebraTensorAlgebra.toClifford
                                                                                                                                                                                                                                                        L∃∀N

                                                                                                                                                                                                                                                          Let \(M\) be a module over a commutative ring \(R\), equipped with a quadratic form \(Q: M \to R\).

                                                                                                                                                                                                                                                          Let \(\iota : M \to _{l[R]} T(M)\) be the canonical \(R\)-linear map for the tensor algebra \(T(M)\).

                                                                                                                                                                                                                                                          Let \(\mathit {1} : R \to _{+*} T(M)\) be the canonical map from \(R\) to \(T(M)\), as a ring homomorphism.

                                                                                                                                                                                                                                                          A Clifford algebra over \(Q\), denoted \(\mathcal {C}\kern -2pt\ell (Q)\), is the ring quotient of the tensor algebra \(T(M)\) by the equivalence relation satisfying \(\iota (m)^2 \sim \mathit {1}(Q(m))\) for all \(m \in M\).

                                                                                                                                                                                                                                                          The natural quotient map is denoted \(\pi : T(M) \to \mathcal {C}\kern -2pt\ell (Q)\) in some literatures, or \(\pi _\Phi \)/\(\pi _Q\) to emphasize the bilinear form \(\Phi \) or the quadratic form \(Q\), respectively.

                                                                                                                                                                                                                                                          Remark.  [ca-0007]

                                                                                                                                                                                                                                                            In literatures, \(M\) is often written \(V\), and the quotient is taken by the two-sided ideal \(I_Q\) generated from the set \(\{ v \otimes v - Q(v) \vert v \in V \}\). See also Clifford algebra [pr-spin].

                                                                                                                                                                                                                                                            As of writing, \(\textsf {Mathlib}\) does not have direct support for two-sided ideals, but it does support the equivalent operation of taking the ring quotient by a suitable closure of a relation like \(v \otimes v \sim Q(v)\).

                                                                                                                                                                                                                                                            Hence the definition above.

                                                                                                                                                                                                                                                            Remark.  [ca-0008]

                                                                                                                                                                                                                                                              This definition and what follows in \(\textsf {Mathlib}\) is initially presented in [wieser2022formalizing], some further developments are based on [grinberg2016clifford], and in turn based on [bourbaki2007algebra] which is in French and never translated to English.

                                                                                                                                                                                                                                                              The most informative English reference on [bourbaki2007algebra] is [jadczyk2019notes], which has an updated exposition in [jadczyk2023bundle].

                                                                                                                                                                                                                                                              Example. Clifford algebra over a vector space [ca-0009]

                                                                                                                                                                                                                                                                Let \(V\) be a vector space \(\mathbb R^n\) over \(\mathbb R\), equipped with a quadratic form \(Q\).

                                                                                                                                                                                                                                                                Since \(\mathbb R\) is a commutative ring and \(V\) is a module, the definition above applies.

                                                                                                                                                                                                                                                                Definition. Clifford map [wieser2022formalizing] [ca-000A]
                                                                                                                                                                                                                                                                CliffordAlgebra.ι
                                                                                                                                                                                                                                                                L∃∀N

                                                                                                                                                                                                                                                                  We denote the canonical \(R\)-linear map to the Clifford algebra \(\mathcal {C}\kern -2pt\ell (M)\) by \(\iota : M \to _{l[R]} \mathcal {C}\kern -2pt\ell (M)\).

                                                                                                                                                                                                                                                                  It's denoted \(i_\Phi \) or just \(i\) in some literatures.

                                                                                                                                                                                                                                                                  Definition. Clifford lift [wieser2022formalizing] [ca-000B]
                                                                                                                                                                                                                                                                  CliffordAlgebra.lift
                                                                                                                                                                                                                                                                  L∃∀N

                                                                                                                                                                                                                                                                    Given a linear map \(f : M \to _{l[R]} A\) into an \(R\)-algebra \(A\), satisfying \(f(m)^2 = Q(m)\) for all \(m \in M\), called is Clifford, the canonical lift of \(f\) is defined to be a algebra homomorphism from \(\mathcal {C}\kern -2pt\ell (Q)\) to \(A\), denoted \(\operatorname {lift} f : \mathcal {C}\kern -2pt\ell (Q) \to _{a} A\).

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

                                                                                                                                                                                                                                                                      Remark.  [ca-000D]

                                                                                                                                                                                                                                                                        The universal property of the Clifford algebras is now proven, and should be used instead of the definition that is subject to change.

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

                                                                                                                                                                                                                                                                          Operations [ca-000G]

                                                                                                                                                                                                                                                                            Convention.  [wieser2022formalizing] [ca-000H]

                                                                                                                                                                                                                                                                              Same as the previous section, let \(M\) be a module over a commutative ring \(R\), equipped with a quadratic form \(Q: M \to R\).

                                                                                                                                                                                                                                                                              We also use \(m\) or \(m_1, m_2, \dots \) to denote elements of \(M\), i.e. vectors, and \(x, y, z\) to denote elements of \(\mathcal {C}\kern -2pt\ell (Q)\).

                                                                                                                                                                                                                                                                              Definition. grade involution [wieser2022formalizing] [ca-000I]
                                                                                                                                                                                                                                                                              CliffordAlgebra.involute
                                                                                                                                                                                                                                                                              L∃∀N

                                                                                                                                                                                                                                                                                Grade involution, intuitively, is negating each basis vector.

                                                                                                                                                                                                                                                                                Formally, it's an algebra homomorphism \(\alpha : \mathcal {C}\kern -2pt\ell (Q) \to _{a} \mathcal {C}\kern -2pt\ell (Q)\), satisfying:

                                                                                                                                                                                                                                                                                1. \(\alpha \circ \alpha = \operatorname {id}\)
                                                                                                                                                                                                                                                                                2. \(\alpha (\iota (m)) = - \iota (m)\)

                                                                                                                                                                                                                                                                                for all \(m \in M\).

                                                                                                                                                                                                                                                                                That is, the following diagram commutes:

                                                                                                                                                                                                                                                                                It's called main involution \(\alpha \) or main automorphism in [jadczyk2019notes], the canonical automorphism in [gallier2008clifford].

                                                                                                                                                                                                                                                                                It's denoted \(\hat {m}\) in [lounesto2001clifford], \(\alpha (m)\) in [jadczyk2019notes], \(m^*\) in [chisolm2012geometric].

                                                                                                                                                                                                                                                                                Definition. grade reversion [wieser2022formalizing] [ca-000J]
                                                                                                                                                                                                                                                                                CliffordAlgebra.reverse
                                                                                                                                                                                                                                                                                L∃∀N

                                                                                                                                                                                                                                                                                  Grade reversion, intuitively, is reversing the multiplication order of basis vectors. Formally, it's an algebra homomorphism \(\tau : \mathcal {C}\kern -2pt\ell (Q) \to _{a} \mathcal {C}\kern -2pt\ell (Q)^{\mathtt {op}}\), satisfying:

                                                                                                                                                                                                                                                                                  1. \(\tau (m_1 m_2) = \tau (m_2) \tau (m_1)\)
                                                                                                                                                                                                                                                                                  2. \(\tau \circ \tau = \operatorname {id}\)
                                                                                                                                                                                                                                                                                  3. \(\tau (\iota (m)) = \iota (m)\)

                                                                                                                                                                                                                                                                                  That is, the following diagram commutes:

                                                                                                                                                                                                                                                                                  It's called anti-involution \(\tau \) in [jadczyk2019notes], the canonical anti-automorphism in [gallier2008clifford], also called transpose/transposition in some literature, following tensor algebra or matrix.

                                                                                                                                                                                                                                                                                  It's denoted \(\tilde {m}\) in [lounesto2001clifford], \(m^\tau \) in [jadczyk2019notes] (with variants like \(m^t\) or \(m^\top \) in other literatures), \(m^\dagger \) in [chisolm2012geometric].

                                                                                                                                                                                                                                                                                  Definition. Clifford conjugate [wieser2022formalizing] [ca-000K]
                                                                                                                                                                                                                                                                                  CliffordAlgebra.reverse
                                                                                                                                                                                                                                                                                  L∃∀N

                                                                                                                                                                                                                                                                                    Clifford conjugate is an algebra homomorphism \({*} : \mathcal {C}\kern -2pt\ell (Q) \to _{a} \mathcal {C}\kern -2pt\ell (Q)\), denoted \(x^{*}\) (or even \(x^\dagger \), \(x^v\) in some literatures), defined to be: \[ x^{*} = \operatorname {reverse}(\operatorname {involute}(x)) = \tau (\alpha (x)) \] for all \(x \in \mathcal {C}\kern -2pt\ell (Q)\), satisfying (as a \(*\)-ring):

                                                                                                                                                                                                                                                                                    1. \((x + y)^{*} = (x)^{*} + (y)^{*}\)
                                                                                                                                                                                                                                                                                    2. \((x y)^{*} = (y)^{*} (x)^{*}\)
                                                                                                                                                                                                                                                                                    3. \({*} \circ {*} = \operatorname {id}\)
                                                                                                                                                                                                                                                                                    4. \(1^{*} = 1\)
                                                                                                                                                                                                                                                                                    and (as a \(*\)-algebra): \[ (r x)^{*} = r' x^{*} \] for all \(r \in R\), \(x, y \in \mathcal {C}\kern -2pt\ell (Q)\) where \('\) is the involution of the commutative \(*\)-ring \(R\).

                                                                                                                                                                                                                                                                                    Note: In our current formalization in \(\textsf {Mathlib}\), the application of the involution on \(r\) is ignored, as there appears to be nothing in the literature that advocates doing this.

                                                                                                                                                                                                                                                                                    Clifford conjugate is denoted \(\bar {m}\) in [lounesto2001clifford] and most literatures, \(m^\ddagger \) in [chisolm2012geometric].