Proposition. Eichler transvections have additive Spin lifts [fcap-002M]

✍️sourceAGENTDRAFTED

Let \(K\) be a field in which \(2\) is invertible, let \(V\) be a \(K\)-space, and let \(Q\) be nondegenerate. Write \(B_Q\) for the unhalved polar form and \(\widehat v=\iota _Q(v)\) for a Clifford generator. Suppose \[Q(u)=0,\qquad B_Q(u,w)=0.\] The Eichler transvection and its Clifford lift are \[\begin {aligned} E_{u,w}(x) &=x+B_Q(x,u)w-B_Q(x,w)u-Q(w)B_Q(x,u)u,\\ L_{u,w}&=1+\widehat w\widehat u. \end {aligned}\] Then \(L_{u,w}\in \operatorname {Spin}(Q)\), its Spin action is \(E_{u,w}\), and \[L_{u,w}^{-1}=\operatorname {rev}(L_{u,w})=1-\widehat w\widehat u.\] The formal transformation formula already makes sense over a commutative ring and module, without nondegeneracy or invertible \(2\) QuadraticMap.transvection_apply QuadraticMap.transvection_mem_specialOrthogonalGroup. The actual Spin lift uses the field, invertible-two, and nondegeneracy hypotheses stated above CliffordAlgebra.coe_spinTransvection CliffordAlgebra.coe_spinToSpecialOrthogonal_spinTransvection.

Indeed, put \(N=\widehat w\widehat u\). The Clifford relations give \[\begin {gathered} N^2=0,\qquad \operatorname {rev}(N)=-N,\\ N\widehat x-\widehat xN =B_Q(x,u)\widehat w-B_Q(x,w)\widehat u,\\ N\widehat xN=Q(w)B_Q(x,u)\widehat u. \end {gathered}\] Thus expansion of \((1+N)\widehat x(1-N)\) gives exactly the displayed formula, including its negative quadratic term, and proves reverse norm one. Actual membership in the vector-generated carrier is a separate point. If \(Q(w)\ne 0\), the explicit factorization is \[1+\widehat w\widehat u =\widehat {\frac {w}{Q(w)}}\, \widehat {\bigl (w+Q(w)u\bigr )},\] and the two quadratic values multiply to \(1\). If \(Q(w)=0\) and \(w\notin Ku\), nondegeneracy supplies \(x\perp u\) with \(b=B_Q(w,x)\ne 0\). For \[a=x+\frac {b-Q(x)}{b}w\] one has \(Q(a)=b\), \(Q(w+a)=2b\), and \(L_{u,w}=L_{u,w+a}L_{u,-a}\), reducing to the nonisotropic case. If \(w\in Ku\), the lift is \(1\). This is the algebraic carrier argument behind the linked formal construction; it needs no finite-dimensionality.

For \(w,w'\in u^\perp \), the cross term \((\widehat w\widehat u)(\widehat {w'}\widehat u)\) vanishes. Hence \[L_{u,w+w'}=L_{u,w}L_{u,w'},\qquad L_{u,-w}=L_{u,w}^{-1},\qquad L_{u,w+cu}=L_{u,w}.\] The same equations hold after projection to the Eichler transformations. Thus the lifts form a homomorphism \[u^{\perp }/Ku\longrightarrow \operatorname {Spin}(Q)\] which commutes with the projection to \(SO(Q)\); when \(u\ne 0\), it is injective CliffordAlgebra.spinTransvection_add CliffordAlgebra.spinTransvection_add_smul CliffordAlgebra.spinToSpecialOrthogonal_comp_spinTransvectionHom CliffordAlgebra.spinTransvectionHom_injective. The domain is \(u^{\perp }/Ku\), not all of \(V/Ku\); for \(u=0\) the family is trivial. If \(V\) is additionally finite-dimensional, these transformations have trivial spinor norm, as predicted by Theorem [fcap-0023] CliffordAlgebra.spinorNorm_transvection.

Chevalley treats the common totally singular case \(Q(u)=Q(w)=B_Q(u,w)=0\): his finite exponential is \(1+\widehat w\widehat u\) and his conjugation formula is the displayed action with its quadratic term zero [chevalley1954algebraic, III.1.7, pp. 73--74]. This passage does not state the arbitrary-\(Q(w)\) formula. Meinrenken's quantization of the bivector \(w\wedge u\) is \(\widehat w\widehat u\); his commutator theorem and exponential Spin comparison recover the full formula over finite-dimensional nondegenerate real or complex spaces [meinrenken2013clifford, Section 2.2.10, Theorem 2.1 and Proposition 2.12, pp. 39--40] [meinrenken2013clifford, Proposition 3.2, pp. 53--54]. Here his symmetric form is the half-polar form \(B_M=b_Q=B_Q/2\). Since \(N^2=0\), both the Clifford and vector exponentials truncate, and the written polynomial calculation fixes the normalization and extends the formula to the stated general field. No claim that every Spin element is one exponential is made.