Cartan proves reflection factorization by an induction that enlarges the fixed subspace. TauCeti formalizes the correction as a list of at most two anisotropic reflections whose product with \(g\) fixes \(W+Kx\) pointwise TauCeti.QuadraticMap.exists_reflectionOrthogonal_list_prod_mul_eqOn_sup_span_singleton. The statement below repackages that list-valued result: when \(H\) contains every reflection, closure under products places the correcting element in \(H\).

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.

Under the hypotheses of Lemma 1, 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 4 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.

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.

Let \(K\), \(V\), and \(Q\) be as in Theorem 3. 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 3 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.

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.

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.

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 CliffordAlgebra.spinToSpecialOrthogonal, and its action on vectors is the usual Spin action by CliffordAlgebra.coe_spinToSpecialOrthogonal_apply.

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

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

Let \(K\) be a field of characteristic different from two, let \(V\) be a positive-dimensional finite-dimensional \(K\)-space, and let \(Q\) be nondegenerate. Write \(\Gamma (Q)\) for the vector-generated Lipschitz group, and \(\tau _Q:\Gamma (Q)\to O(V,Q)\) for its twisted action. For \(x\in \Gamma (Q)\), let \(N_{\mathrm {rev}}(x)\in K^{\times }\) be the unique scalar unit satisfying \(\operatorname {rev}(x)x=N_{\mathrm {rev}}(x)\,1\). Set \(\mathcal {S}_K=K^{\times }/(K^{\times })^2\). The top row is exact, and the square commutes:

If \(Q(v)\) is nonzero, then \[N_{\mathrm {rev}}(\widehat v)=Q(v),\qquad \nu _Q^O(r_v)=[Q(v)]\] CliffordAlgebra.cliffordNorm_unitι CliffordAlgebra.orthogonalSpinorNorm_reflectionOrthogonal. Consequently, for an even product \(x=\widehat v_1\cdots \widehat v_{2k}\) of nonisotropic vector lifts, \[\tau _Q(x)=r_{v_1}\cdots r_{v_{2k}}\in SO(V,Q),\qquad \nu _Q(r_{v_1}\cdots r_{v_{2k}}) =\left [\prod _{i=1}^{2k}Q(v_i)\right ].\] Multiplying a lift by \(c\in K^\times \) changes its reverse norm by \(c^2\), so the square class is independent of the chosen lift. [chevalley1954algebraic, II.3.5--6, pp. 52--53] gives these vector and paired-product values. The scalar exact sequence, reflection factorization, and the same square-scaling law appear in [meinrenken2013clifford, Theorem 3.1, pp. 50--51]. Chevalley's quotient statement assumes positive dimension; Meinrenken works with a finite-dimensional characteristic-zero nondegenerate bilinear space.

If \(e:(V,Q)\simeq (V',Q')\) is an isometry equivalence, then conjugation transport preserves both norms: for \(g\in O(V,Q)\) and \(h\in SO(V,Q)\), \[\nu _{Q'}^O(ege^{-1})=\nu _Q^O(g),\qquad \nu _{Q'}(ehe^{-1})=\nu _Q(h).\] It therefore carries \(\ker \nu _Q\) onto \(\ker \nu _{Q'}\) QuadraticMap.IsometryEquiv.orthogonalSpinorNorm_orthogonalGroupCongr QuadraticMap.IsometryEquiv.spinorNorm_specialOrthogonalGroupCongr kernel-transport source. The induced kernel equivalence also commutes with Spin transport Spin-transport source. These are isometry-equivalence statements; they do not assert scalar-extension or orthogonal-product naturality. This is the norm-square companion to the vector-action square in Proposition 21.

Let \(K\) be a field in which \(2\) is invertible, \(V\) a finite-dimensional \(K\)-space, and \(Q\) a nondegenerate quadratic form. The Clifford norm of a Lipschitz lift, taken modulo squares, descends to \(\nu _Q^O:O(V,Q)\to K^{\times }/(K^\times )^2\) CliffordAlgebra.orthogonalSpinorNorm_lipschitzToOrthogonal. Its restriction to \(SO(V,Q)\) is the spinor norm \(\nu _Q:SO(V,Q)\to K^\times / (K^\times )^2\) CliffordAlgebra.spinorNorm. Then \[\operatorname {im}\bigl (\operatorname {Spin}(V,Q)\to SO(V,Q)\bigr ) =\ker \nu _Q.\] Thus a special orthogonal transformation has a Spin lift exactly when its spinor-norm class is trivial.

[chevalley1954algebraic, II.3.5--6, pp. 52--53] defines the reversal norm and describes the reduced orthogonal image by square classes of products \(Q(u)Q(v)\). His ordinary Clifford action and reversal norm compare with TauCeti's twisted action on even lifts: grading fixes such lifts, so the two actions agree, and reverse and star norms coincide Remark [fcap-0028]. For a single nonisotropic reflection, the descended orthogonal spinor norm is \[\nu _Q^O(r_v)=[Q(v)]\] CliffordAlgebra.orthogonalSpinorNorm_reflectionOrthogonal. This agrees with Chevalley's reverse norm. TauCeti's star norm on the odd vector lift has class \([-Q(v)]\); it is a different norm. The extra minus sign cancels on an even product, where the reverse and star norms agree.

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

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

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

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

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

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

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_transvectionLiftHom CliffordAlgebra.transvectionLiftHom_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 9 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.

Let \(K\) be a field in which \(2\) is invertible and take the three-dimensional quadratic space \[Q(au+bv+cz)=ab+c^2.\] Thus \(u,v\) are null, \(B_Q(u,v)=1\), \(Q(z)=1\), and \(z\) is orthogonal to their hyperbolic plane. For \(w=tz\), the preceding lift and action become \[\begin {gathered} L_t=1+t\widehat z\widehat u =\widehat z\,\widehat {(z+tu)},\\ E_t(u)=u,\qquad E_t(z)=z-2tu,\qquad E_t(v)=v+tz-t^2u. \end {gathered}\] Both factors in the displayed product have quadratic value \(1\). Hence the pair criterion puts \(L_t\) directly in the actual Spin group, including at \(t=0\) CliffordAlgebra.ι_mul_ι_mem_spinGroup_of_norm_mul_norm_eq_one. In coordinates \((a,c,b)\) the transformation is \[E_t= \begin {pmatrix} 1&-2t&-t^2\\ 0&1&t\\ 0&0&1 \end {pmatrix}.\] Substitution gives \(Q(E_t x)=Q(x)\), while multiplication gives \(E_sE_t=E_{s+t}\) and \(L_sL_t=L_{s+t}\). At \(t=1/2\), \[z\longmapsto z-u,\qquad v\longmapsto v+\frac 12z-\frac 14u,\] and composing this map with itself gives \(z\mapsto z-2u\) and \(v\mapsto v+z-u\). For \(t\ne 0\), the vector action has \((E_t-1)^2v=-2t^2u\) and \((E_t-1)^3=0\), although the Clifford increment satisfies \((L_t-1)^2=0\). Over \(\mathbb R\), this is the null frame inside the split model of Example [fcap-002I]; over every stated field it is a concrete element of the spinor-norm kernel in Theorem 9.

There is also a precise radical comparison. On the degenerate real form \[Q_{\mathrm {PGA}}(ar+xe+yf)=x^2+y^2\] the line \(\mathbb Rr\) is radical. With \(u=r\) and \(w=te\), the same ring-level transvection formula gives \[\begin {gathered} L_t=1+t\widehat e\widehat r =\widehat e\,\widehat {(e+tr)},\\ E_t(r)=r,\qquad E_t(e)=e-2tr,\qquad E_t(f)=f. \end {gathered}\] The nondegenerate packaged Spin-transvection theorem does not apply here. Nevertheless this particular lift still belongs to the vector-generated Spin carrier, because both displayed factors have quadratic value \(1\); the pair criterion itself needs no nondegeneracy. The quadratic action term vanishes because \(B_Q(r,-)=0\), and now \((E_t-1)^2=0\). This retains the original degenerate Clifford algebra rather than replacing it by the radical quotient of Remark [fcap-002C]. It does not identify the shear with a particular PGA point translation, motor parameter, dual encoding, or orientation convention.

On \(\mathbb R^2\), let \(Q(a,b)=a^2-b^2\), \(e_+=(1,0)\), and \(e_-=(0,1)\). The corresponding reflections are \[r_{e_+}=\operatorname {diag}(-1,1),\qquad r_{e_-}=\operatorname {diag}(1,-1),\] so \(g=r_{e_+}r_{e_-}=-I\) lies in \(SO(Q)\). Its spinor norm is \[\nu _Q(g)=[Q(e_+)Q(e_-)]=[-1]\ne [1].\] With the two norm conventions of Remark [fcap-0028], the even Clifford lift \(x=\widehat e_+\widehat e_-\) has \[N_{\mathrm {rev}}(x)=N_*(x)=-1.\] For every \(c\in \mathbb R^\times \), the scalar multiple \(cx\) has norm \(-c^2\), which cannot equal \(1\). More generally, any two Lipschitz lifts of \(g\) differ by a scalar by Proposition 8, so no lift can be normalized into the norm-one Spin carrier. Equivalently, the image theorem in Theorem 9 excludes a Spin lift because \(\nu _Q(g)\) is nontrivial.

This is the mixed-sign counterpart to the successful square normalizations in Lemma [fcap-000B] and Theorem [fcap-000C]. Meinrenken notes that over \(\mathbb R\) one sometimes uses the weaker carrier condition \(N(x)=\pm 1\); under that different convention this \(x\) passes the norm test [meinrenken2013clifford, Remark 3.2, p. 52]. TauCeti's Spin group uses the norm-one carrier, so the two conventions must not be identified.

Let \(Q\) be a positive-dimensional finite-dimensional nondegenerate real quadratic form. Distinguish the orthogonal norm \(\nu _Q^O\) on \(O(Q)\) from its restriction \(\nu _Q\) to \(SO(Q)\). Since \(\mathbb R^{\times }/(\mathbb R^\times )^2=\{[1],[-1]\}\), their images and the Spin image are: \[\begin {array}{c|c|c|c} \text {case}&\operatorname {im}\nu _Q^O& \operatorname {im}\nu _Q&\text {Spin image}\\ \hline \text {positive definite}&\{[1]\}&\{[1]\}&SO(Q)\\ \text {negative definite}&\{[1],[-1]\}&\{[1]\}&SO(Q)\\ \text {indefinite}&\{[1],[-1]\}&\{[1],[-1]\}&\ker \nu _Q \end {array}\] For a positive form, every reflected value is a square, so the orthogonal norm is trivial CliffordAlgebra.orthogonalSpinorNorm_eq_one_of_posDef. For a negative form, the orthogonal norm is the determinant square class and is therefore trivial on \(SO(Q)\) CliffordAlgebra.orthogonalSpinorNorm_eq_orthogonalDetSquareClass_of_negDef CliffordAlgebra.spinorNorm_eq_one_of_negDef. In the indefinite case, one positive and one negative reflection give a determinant-one element of norm \([-1]\), so \(\nu _Q\) is onto CliffordAlgebra.spinorNorm_surjective_of_indefinite. Thus the final kernel has index two. The Spin-image column follows from Theorem 9; the table does not identify this kernel with a topological component.

Rank zero is separate: \(SO(Q)\) is trivial, and the image/kernel theorem uses its subsingleton branch rather than the positive-dimensional scalar row. In rank one, \(SO(Q)\) and its spinor norm are trivial. For any nonzero \(v\), the image of \(\nu _Q^O\) is generated by \([Q(v)]\), and it is trivial exactly when \(Q(v)\) is a square CliffordAlgebra.spinorNorm_eq_one_of_finrank_le_one CliffordAlgebra.orthogonalSpinorNorm_range_eq_zpowers_of_finrank_eq_one CliffordAlgebra.orthogonalSpinorNorm_eq_one_iff_isSquare_apply_of_finrank_eq_one. An indefinite real form has rank at least two. Degenerate or semidefinite PGA forms lie outside every row of this nondegenerate table.

Let \(V\) be a finite-dimensional real vector space with \(\dim V\geq 2\), and let \(Q\) be positive definite. If \(Q(x)=Q(y)=c>0\), then some \(s\in \operatorname {Spin}(Q)\) satisfies \[\operatorname {spinVectorAction}_Q(s,x)=y.\] In particular, Spin acts transitively on the unit level \(Q(v)=1\). This is a statement about the algebraic vector action; no topology or compactness is needed.

Cartan's anisotropic-normal reflection has determinant \(-1\) [cartan1981theory, Section 9, pp. 9--10]. His even-reflection correction appears in [cartan1981theory, Section 10, p. 10]. The following two-case calculation gives the sphere orbit explicitly.

The formal surjectivity theorem uses positive \(Q\) directly: every nonzero value \(Q(v)\) has a real square root, making the spinor norm trivial on \(SO(Q)\) CliffordAlgebra.orthogonalSpinorNorm_eq_one_of_posDef. This is a separate route from the fixed-sign sufficient hypothesis in Theorem 7.

For a real quadratic space of signature \((p,q)\) with \(p+q>0\), 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.

Let \(K\) be a characteristic-zero field, let \(V\) be nonzero and 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 7 supplies that proof and yields the specialized extension.

For a real quadratic space of signature \((p,q)\) with \(p+q>0\), 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.

In Meinrenken's characteristic-zero, nonzero, 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.

Let \(R\) be a commutative ring, let \(M_1,M_2\) be \(R\)-modules with quadratic forms \(Q_1,Q_2\), and let \(f:M_1\to M_2\) be an \(R\)-linear map satisfying \[Q_2(f(m))=Q_1(m).\] The Clifford universal property gives an algebra homomorphism \(\operatorname {Cl}(f):\mathcal {C}\kern -2pt\ell (Q_1)\to \mathcal {C}\kern -2pt\ell (Q_2)\) characterized on generators by \[\operatorname {Cl}(f)(\iota _{Q_1}(m))=\iota _{Q_2}(f(m))\] CliffordAlgebra.map_apply_ι. It preserves the Spin carrier and therefore restricts to a group homomorphism \(\operatorname {Spin}(f):\operatorname {Spin}(Q_1)\to \operatorname {Spin}(Q_2)\) QuadraticMap.Isometry.spinGroupMap. Concretely, the Clifford map preserves Lipschitz membership QuadraticMap.Isometry.map_mem_lipschitzGroup, evenness CliffordAlgebra.map_mem_even, and Clifford conjugation CliffordAlgebra.map_star; these are the carrier conditions separated in Remark [fcap-0028]. Neither construction requires \(f\) to have an inverse.

Now suppose that \(2\) is invertible in \(R\). If \(a_i\) denotes the Spin vector action on \(M_i\), then \[a_2\bigl (\operatorname {Spin}(f)(s),f(m)\bigr ) =f\bigl (a_1(s,m)\bigr ).\] This identity says that the square with horizontal maps \(a_1,a_2\) and vertical maps \(\operatorname {Spin}(f)\times f,f\) commutes. It is the vector-action naturality equation, with no finite-dimensionality or nondegeneracy hypothesis. If \(f\) is instead an isometry equivalence, it induces a Spin equivalence QuadraticMap.IsometryEquiv.spinGroupEquiv, and the same square packages as naturality of the Spin-to-special-orthogonal homomorphism source theorem.

A changed Gram matrix shows why the target form is part of the data. Over \(\mathbb Q\), set \(Q_1(x,y)=x^2+y^2\) and \(T(x,y)=(2x,y)\). Keeping the same form on the target does not give an isometry: at \(e_1\), \[Q_1(Te_1)=4\ne 1=Q_1(e_1).\] Correspondingly, the source generator \(\iota _{Q_1}(e_1)\) squares to \(1\), while its proposed image \(\iota _{Q_1}(2e_1)\) squares to \(4\); that assignment cannot define the claimed Clifford map.

For the transported target form \(Q_2(x,y)=x^2/4+y^2\), one has \(Q_2(Tv)=Q_1(v)\). In column coordinates, \[G_1=I,\qquad G_2=(T^{-1})^\top G_1T^{-1} =\begin {pmatrix}1/4&0\\0&1\end {pmatrix},\qquad T^\top G_2T=G_1.\] Now \(\iota _{Q_2}(2e_1)^2=Q_2(2e_1)=1\), so the generator relation is preserved. Thus an arbitrary basis scaling is not a fixed-form isometry; it becomes an isometry only after the domain and target forms are related in the correct direction. This differs from the module equivalence \(T_Q:\mathcal {C}\kern -2pt\ell (Q)\simeq \bigwedge M\) in Lemma [fcap-0004], which is not an algebra map.

Meinrenken derives \(\operatorname {Cl}(f)\) from the same universal property for a bilinear-form-preserving linear map [meinrenken2013clifford, Section 2.2.2, Proposition 2.2, p. 29]. Chevalley's tensor-quotient construction gives the corresponding extension from generator images whose squares are \(Q(x)\) [chevalley1954algebraic, II.1.1, pp. 38--39]. In Meinrenken's convention \(Q(v)=B(v,v)\), so his \(B\) is the half-polar form \(b_Q\) of Convention [fcap-0027]. These sources work over finite-dimensional vector spaces over fields; Meinrenken assumes characteristic different from two. The formal action square above has the commutative-ring hypotheses stated here. This card makes no claim about scalar extension, orthogonal sums, or composition of extension maps.

Here a local field \(K\) of characteristic different from \(2\) means \(\mathbb R\) or \(\mathbb C\) with its usual topology, or a complete discretely valued field with finite residue field and \(\operatorname {char}K\ne 2\), with its valuation topology. The last case includes finite extensions of \(\mathbb Q_2\): the characteristic restriction is on \(K\), not its residue field. This uses the nonarchimedean definition in [lam2005quadratic, VI.2, Definition 2.1 and the discussion, pp. 151--152], with the two archimedean fields included explicitly.

For a finite-dimensional \(K\)-vector space \(W\), its canonical topology is the topology transported from \(K^d\) by any basis, where \(d=\dim _K W\). It is independent of the basis: a change of coordinates and its inverse have entries that are finite linear combinations, hence are continuous. In dimension zero this gives the one-point topology. Every linear map between such spaces is continuous by the same argument.

More generally, the canonical topology on the local points of an affine algebraic set is the subspace topology in any finite coordinate presentation. Explicitly, let \(X(K)\) consist of the points \(x\in K^m\) satisfying the finite polynomial equations \[\begin {gathered} f_i(x)=0\\ (i=1,\ldots ,r). \end {gathered}\] Give \(X(K)\) the topology inherited from \(K^m\). Changing the finite algebraic presentation expresses each new coordinate as a polynomial in the old ones and conversely. Both coordinate maps are continuous, so this topology is independent of the presentation. This is the concrete affine construction in [conrad2011adelic, Proposition 2.1 and its proof, p. 2]. It also shows directly that polynomial maps on local points are continuous.

Let \(A\) be a finite-dimensional unital \(K\)-algebra, with its canonical vector-space topology. Its multiplication is continuous because its coordinates are bilinear polynomials. On the group of units \(A^\times \), the affine-point construction first gives the inverse-graph topology: \[\begin {gathered} A^\times \longrightarrow A\times A,\\ x\longmapsto (x,x^{-1}). \end {gathered}\] This identifies the units with the solution set of \(xy=yx=1\). The inverse coordinate matters in the general topological-ring construction; see [conrad2011adelic, opening of Section 3, pp. 3--4].

Over the local fields specified above, this is also the subspace topology from \(A\). Indeed, write \(L_x\) for the matrix of left multiplication by \(x\). Its entries depend linearly on \(x\), and for a unit \(x\), \[\begin {gathered} x^{-1}=L_x^{-1}(1),\\ L_x^{-1}=\frac {\operatorname {adj}(L_x)}{\det L_x}. \end {gathered}\] Polynomial continuity and continuity of reciprocal on \(K^\times \) show that inversion is continuous on the subspace \(A^\times \subseteq A\). Thus the inverse-graph map is continuous for that subspace topology; projection to the first coordinate is its continuous inverse. For the zero algebra the unit group is a singleton and the same topology agreement is immediate.

For a quadratic form \(Q\) on a finite-dimensional \(V\), apply this construction to the Clifford algebra \(A=\mathcal {C}\kern -2pt\ell (Q)\) and to \(\operatorname {End}_K(V)\). The orthogonal and special orthogonal groups inherit the matrix topology from \(\operatorname {End}_K(V)\). The actual vector-generated Lipschitz, Pin, and Spin carriers inherit the subspace topology from \(\mathcal {C}\kern -2pt\ell (Q)^\times \), equivalently from \(\mathcal {C}\kern -2pt\ell (Q)\). These topologies depend on the field topology and the algebraic carriers, without a choice of positive-definite norm or a replacement of the actual carriers by normalizer-defined groups. The star-unitary Pin convention and its even Spin restriction are used here; Remark [fcap-0028] compares the star and reverse norms.

The coordinate topology on \(W\) is also its module topology: it is the finest topology making addition and scalar multiplication continuous. The coordinate topology has these properties; for any other such topology, the basis map \(K^d\to W\), a finite sum of scalar multiples of fixed basis vectors, is continuous. This proves the claimed maximality. Mathlib's moduleTopology defines that intrinsic topology, and TauCeti's CliffordAlgebra.instTopologicalSpaceCliffordAlgebra uses it for \(\mathcal {C}\kern -2pt\ell (Q)\). The agreement with local coordinates follows from the finite-dimensional argument above; the declaration itself is defined over a general topological commutative ring.

Let \(K\) be a local field of characteristic different from two in the sense of Definition 22, and let \(Q\) be a nondegenerate quadratic form on a finite-dimensional \(K\)-space \(V\). Give all spaces and carriers the canonical topologies of that definition. Then \(O(Q)\) and \(SO(Q)\) are closed in \(\operatorname {End}_K(V)\), and the actual vector-generated \(\operatorname {Spin}(Q)\) is closed in \(A=\mathcal {C}\kern -2pt\ell (Q)\). These are locally compact Hausdorff topological groups. Their actions on \(V\) and the projection \(\rho :\operatorname {Spin}(Q)\to SO(Q)\) are continuous.

Assume first that \(n=\dim _K V>0\). Write \(\widehat v=\iota _Q(v)\), \(\alpha \) for the grading involution, and \(\operatorname {rev}\) for reversion. The vector-generated Lipschitz group has the following closed description inside \(A^\times \): \[\begin {gathered} \Gamma (Q)=\{x\in A^\times :\tau _x(V)\subseteq V\},\\ \tau _x(\widehat v)=\alpha (x)\widehat v x^{-1}. \end {gathered}\] Here and below \(V\) is identified with its embedded vector subspace. We verify this description so that the generated carrier is retained. If \(w=\alpha (x)\widehat v x^{-1}\in V\), applying \(\alpha \) also gives \(w=x\widehat v\alpha (x)^{-1}\). Multiplying the two expressions yields \(w^2=Q(v)1\). Thus \(\tau _x\) preserves \(Q\); nondegeneracy makes it injective, hence an isometry of \(V\). By Proposition 8, choose a vector product \(y\in \Gamma (Q)\) with this action. For \(z=y^{-1}x\), \[\alpha (z)\widehat v=\widehat v z\qquad (v\in V).\] In an orthogonal basis \(e_1,\ldots ,e_n\), expand \(z\) in the Clifford monomials \(e_I\). For a fixed \(j\), the displayed equation is automatic on monomials with \(j\notin I\); on those with \(j\in I\), its two sides have opposite signs. The nonzero factors \(2Q(e_j)\) and linear independence force all their coefficients to vanish. Doing this for every \(j\) leaves only a scalar \(z=c1\), with \(c\ne 0\). For any \(Q(v)\ne 0\), \[c1=\widehat v\,\widehat {\left (\frac {c}{Q(v)}v\right )}.\] So \(c1\), and hence \(x\), belongs to \(\Gamma (Q)\). The reverse inclusion holds because each vector unit acts as a reflection. This also explains the general-field carrier argument behind the real case in Proposition [fcap-0037].

The actual Spin carrier is therefore \[\begin {gathered} \operatorname {Spin}(Q)=\{x\in A^{\mathrm {even}}:\\ \operatorname {rev}(x)x=1,\\ x\widehat v\operatorname {rev}(x)\in V\quad (v\in V)\}. \end {gathered}\] In finite dimension this left inverse is two-sided: \(L_{\operatorname {rev}(x)}L_x=1\) makes \(L_x\) invertible and gives \(x\operatorname {rev}(x)=1\). The preceding description now puts \(x\) in \(\Gamma (Q)\); evenness and reverse norm one are exactly the Spin conditions of Remark [fcap-0028]. Conversely every Spin element satisfies these equations. This is the norm-one convention: the star and reverse norms agree on even elements.

Every finite-dimensional linear subspace of \(A\) is closed: extend a basis and set the complementary coordinates equal to zero. Evenness and membership in \(V\) are consequently closed conditions. Reversion is linear, and multiplication is polynomial. It suffices to impose vector preservation on a basis of \(V\), so the displayed Spin carrier is a finite intersection of closed polynomial conditions in \(A\). The same argument, with continuous inversion on \(A^\times \), proves that \(\Gamma (Q)\) is closed in \(A^\times \).

Choose a basis of \(V\) and let \(G\) be the nonsingular Gram matrix of the half-polar form \(b_Q\) from Convention [fcap-0027]. Then \[\begin {aligned} O(Q)&=\{g:g^{\mathsf T}Gg=G\},\\ SO(Q)&=\{g\in O(Q):\det g=1\}. \end {aligned}\] The first equation already forces \(g\) invertible by taking determinants. These polynomial equations prove closedness in the whole matrix space. Matrix inversion, Clifford inversion and multiplication are continuous by Definition 22; their restrictions give the topological group operations. Finite-dimensional spaces over \(K\) are locally compact Hausdorff, so the closed carriers have those properties.

The joint action \((x,v)\mapsto \alpha (x)\widehat v x^{-1}\) is continuous by the same coordinate operations. Its values lie in the closed vector subspace, whose inverse identification with \(V\) is linear and continuous. Evaluating on a basis proves continuity of \(\tau :\Gamma (Q)\to O(Q)\) in matrix coordinates. Restricting to Spin removes \(\alpha \), and even determinant parity from Lemma 6 places its image in \(SO(Q)\), proving continuity of \(\rho \). The joint matrix actions of \(O(Q)\) and \(SO(Q)\) are polynomial as well.

If \(V=0\), its only vector has zero quadratic value. There are no invertible vector generators, so \(\Gamma (Q)=\operatorname {Spin}(Q)=\{1\}\); both orthogonal groups are also trivial. All conclusions follow for these one-point carriers. The positive-dimensional normalizer description must not be used here: every Clifford unit preserves the zero vector space.

TauCeti proves closedness and local compactness for the actual carrier in CliffordAlgebra.isClosed_spinGroup and CliffordAlgebra.locallyCompactSpace_spinGroup. The continuous projection is TauCeti.CliffordAlgebra.continuous_spinToSpecialOrthogonal. These declarations use canonical module and subgroup topologies; the first two allow Hausdorff topological fields, with local compactness added for the second. The projection itself needs neither nondegeneracy nor local compactness. The argument above supplies their coordinate specialization.

Let \(K\), \(V\), \(Q\) and their topologies be as in Lemma 23. The continuous surjection \(\tau :\Gamma (Q)\to O(Q)\) is open and is a quotient map. Give \(\mathcal S_K=K^{\times }/(K^{\times })^2\) its quotient topology. It is discrete, and the two spinor norms of Proposition 8, \[\begin {aligned} \nu _Q^O &: O(Q)\longrightarrow \mathcal S_K,\\ \nu _Q &: SO(Q)\longrightarrow \mathcal S_K, \end {aligned}\] are continuous and locally constant. In particular, \(\rho (\operatorname {Spin}(Q))=\ker \nu _Q\) is an open subgroup of \(SO(Q)\). This says that sufficiently small changes of an isometry preserve its square-class obstruction to a Spin lift.

TauCeti's CliffordAlgebra.isOpenMap_lipschitzToOrthogonal uses a Hausdorff, locally compact, \(\sigma \)-compact topological field. Its CliffordAlgebra.continuous_cliffordNorm uses a complete nontrivially normed field. Finally, CliffordAlgebra.continuous_orthogonalSpinorNorm, CliffordAlgebra.continuous_spinorNorm and CliffordAlgebra.isOpen_range_spinToSpecialOrthogonal assume a locally compact nontrivially normed field and explicitly require open squares. Each declaration assumes finite dimension and invertible two, with nondegeneracy for the action and spinor-norm conclusions. The local fields here satisfy those hypotheses, and the cited local square theorem discharges the extra open-squares condition.

Let \(K\) be a local field of characteristic different from two as in Definition 22, and let \(Q\) be a nondegenerate quadratic form on a finite-dimensional \(K\)-space \(V\). Use the canonical topologies of Definition 22. A continuous map is called proper here if the inverse image of every compact set is compact. The form \(Q\) is anisotropic if \(Q(v)=0\) implies \(v=0\); otherwise it is isotropic. This includes the zero-dimensional form as anisotropic, as in [lam2005quadratic, I.3, Definition 3.1, p. 9].

The Spin projection \(\rho :\operatorname {Spin}(Q)\to SO(Q)\) is proper, and \[\begin {gathered} \operatorname {Spin}(Q)\text { is compact}\\ \Longleftrightarrow \quad Q\text { is anisotropic}. \end {gathered}\] Anisotropy also makes \(O(Q)\) compact. The proofs below deduce these claims from the closed carriers and open Clifford quotient of Lemma 23 and Proposition 24, using the scalar-kernel and reverse-norm identities of Proposition 8. Thus compactness depends on the quadratic form, even when the projection has finite kernel.

TauCeti formalizes properness and the compactness criterion in CliffordAlgebra.isProperMap_spinToSpecialOrthogonal and CliffordAlgebra.isCompact_spinGroup_iff. Their hypotheses are a weakly locally compact nontrivially normed field, finite dimension, invertible two and nondegeneracy. The supporting TauCeti.QuadraticMap.isCompact_orthogonalGroup assumes anisotropy and finite dimension over the same kind of field, without a separate nondegeneracy or characteristic condition. These statements use the canonical module and subgroup topologies; on the locally compact Hausdorff targets here, formal properness agrees with the compact-preimage condition used above.

Over \(\mathbb Q_3\), with \(|3|_3=1/3\), consider \[\begin {aligned} Q_+(x,y)&=x^2+y^2,\\ Q_-(x,y)&=x^2-y^2. \end {aligned}\] Both forms are nondegenerate. In the canonical topologies, \(\operatorname {Spin}(Q_+)\) is compact and \(\operatorname {Spin}(Q_-)\) is not. This is a concrete application of Theorem 25. The local-field convention is Definition 22; the \(p\)-adic fields and their residue fields are included in [lam2005quadratic, VI.2, Definition 2.1 and discussion, pp. 151--152]. The calculations below establish the contrast directly.

If \(x^2+y^2=0\) and \(y=0\), then \(x=0\). If \(y\ne 0\), set \(z=x/y\); then \(z^2=-1\). Its 3-adic valuation is zero, so \(z\) is a unit in \(\mathbb Z_3\). Reduction modulo \(3\) would give a square root of \(-1=2\) in \(\mathbb F_3\). But the two nonzero residues both square to \(1\). Hence no such \(z\) exists, and \(Q_+\) is anisotropic. Its Spin group is compact by Theorem 25. The nonsquare input is also Padic.not_isSquare_neg_one_of_mod_four_eq_three at \(p=3\); TauCeti.anisotropic_binary_one_one_iff identifies anisotropy of \(\langle 1,1\rangle \) with this nonsquare condition over any field. These support the calculation, rather than asserting a formalization of every displayed lift below.

For \(Q_-\), take \[\begin {gathered} u=(1,1),\\ v=(1/4,-1/4). \end {gathered}\] They satisfy \(Q_-(u)=Q_-(v)=0\) and \(B_{Q_-}(u,v)=1\), in the unhalved convention of Convention [fcap-0027]. They form a basis, and \(Q_-(au+bv)=ab\). Thus \(Q_-\) is a split hyperbolic plane, agreeing with [lam2005quadratic, I.3, Theorem 3.2, p. 9].

There is an explicit unbounded family in the Spin image. In the ordered basis \((u,v)\), let \(h_t=\operatorname {diag}(t,t^{-1})\), where \(t\in \mathbb Q_3^\times \). Write \(\widehat w=\iota _{Q_-}(w)\). Both \(tu+t^{-1}v\) and \(u+v\) have quadratic value one, so \[s_t=\widehat {(tu+t^{-1}v)}\,\widehat {(u+v)}\] lies in the actual vector-generated Spin group by Theorem [fcap-000C] and the reverse-norm convention in Remark [fcap-0028]. The reflection formula gives the following matrices in \((u,v)\): \[\begin {gathered} r_{tu+t^{-1}v}=\begin {pmatrix}0&-t^2\\-t^{-2}&0\end {pmatrix},\\ r_{u+v}=\begin {pmatrix}0&-1\\-1&0\end {pmatrix},\\ \rho (s_t)=r_{tu+t^{-1}v}r_{u+v},\\ \rho (s_t)=\begin {pmatrix}t^2&0\\0&t^{-2}\end {pmatrix}=h_t^2. \end {gathered}\] The product order is that of the two Clifford factors. Thus these are actual normalized lifts, not only abstract square-class witnesses.

Set \(t=3^{-r}\) for \(r\geq 1\). The first matrix entry has \(|t^2|_3=3^{2r}\), which is unbounded. The continuous image of a compact Spin group would have bounded matrix entries, proving that \(\operatorname {Spin}(Q_-)\) is not compact. In particular, binary noncompactness already follows from this torus family, without an orthogonal complement in which to construct transvections.

Let \(K\) be a nonarchimedean local field of characteristic different from two, as in Definition 22, and let \(Q\) be a nondegenerate form on a finite-dimensional \(K\)-space. Use the reverse-norm convention of Proposition 8: \(\nu _Q^O\) is the spinor norm on \(O(Q)\), and \(\nu _Q\) is its restriction to \(SO(Q)\). Write \[\begin {gathered} S=K^{\times }/(K^{\times })^2,\\ I_Q=[SO(Q):\rho (\operatorname {Spin}(Q))]. \end {gathered}\] The kernel theorem Theorem 9 gives \(I_Q=|\operatorname {im}\nu _Q|\). Thus the index of the Spin image in \(SO(Q)\) measures the size of the spinor-norm image, not its index in \(S\).

For the anisotropic form \(Q_+=\langle 1,1\rangle \) over \(\mathbb Q_3\) from Example 26, both spinor-norm images are the square classes of norms from \(\mathbb Q_3(\sqrt {-1})\). They form the same index-two subgroup of \(S\). Since \(|S|=4\), the Spin index is \(I_{Q_+}=2\). The square-class count is [lam2005quadratic, VI.2, Theorem 2.22, p. 162]; the norm-image calculation follows from the general binary formulas below.

Suppose \(Q=\langle a,b\rangle \) is anisotropic, with \(a,b\in K^\times \), and put \(d=-b/a\). Then \(d\) is nonsquare and \(E=K(\sqrt d)\) is a quadratic field. Its field norm is \[N_{E/K}(x+y\sqrt d)=x^2-dy^2.\] The norm subgroup \(N=N_{E/K}(E^\times )\) contains \((K^\times )^2\), since \(N_{E/K}(c)=c^2\) for \(c\in K^\times \). Let \(H=N/(K^\times )^2\subseteq S\). Then \[\begin {gathered} \operatorname {im}\nu _Q=H,\\ \operatorname {im}\nu _Q^O=H\cup [a]H,\\ [S:H]=2,\\ I_Q=|H|=|S|/2. \end {gathered}\] In particular, \(\nu _Q^O\) is surjective exactly when \(a\notin N\). If \(a\in N\), both images are \(H\). If \(Q\) is split binary instead, both images are \(S\) and \(I_Q=|S|\).

The lower-dimensional boundary, with \(0\) denoting the form on the zero space, is \[\begin {array}{c|c|c} Q&\operatorname {im}\nu _Q&\operatorname {im}\nu _Q^O\\ \hline 0&\{1\}&\{1\}\\ \langle a\rangle &\{1\}&\langle [a]\rangle \end {array}\] In both rows \(SO(Q)\) is trivial and \(I_Q=1\). In rank one, \(O(Q)=\{1,-1\}\), and \(-1\) is reflection in the basis vector of value \(a\); its norm is \([a]\). These statements agree with CliffordAlgebra.spinorNorm_eq_one_of_finrank_le_one and CliffordAlgebra.orthogonalSpinorNorm_range_eq_zpowers_of_finrank_eq_one.

The two binary image formulas are CliffordAlgebra.range_spinorNorm_of_equivalent_binary and CliffordAlgebra.range_orthogonalSpinorNorm_of_equivalent_binary. They use the parameter \(-ab=a^2d\), which gives the same quadratic extension and norm subgroup. The local index and orthogonal surjectivity criterion are CliffordAlgebra.index_range_spinorNorm_of_finrank_eq_two_of_anisotropic and CliffordAlgebra.orthogonalSpinorNorm_surjective_iff_not_mem_quadraticNormSubgroup_of_anisotropic_binary. The image formulas require finite dimension, nondegeneracy and invertible two over a field; the index-two conclusion additionally uses the stated local-field and anisotropy hypotheses.

Let \(K\) be a nonarchimedean local field of characteristic different from two, as in Definition 22. Let \(Q\) be nondegenerate on a finite-dimensional \(K\)-space \(V\) with \(\dim _K V\geq 3\). Use \(S=K^{\times }/(K^{\times })^2\), \(\nu _Q\), \(\nu _Q^O\) and \(I_Q\) as in Proposition 27. Every element of \(S\) is the spinor norm of a product of two reflections. Consequently, \[\begin {gathered} \operatorname {im}\nu _Q=\operatorname {im}\nu _Q^O=S,\\ I_Q=|S|. \end {gathered}\] This holds for anisotropic ternary and quaternary forms as well as isotropic forms. The input is the local isotropy theorem: every nondegenerate form of dimension at least five is isotropic [lam2005quadratic, VI.2, Theorem 2.12, pp. 158--159].

Let \(k\) be the residue field, put \(q_0=|k|\), and normalize the additive valuation \(v_K:K^\times \to \mathbb Z\) to be surjective. Set \(e=v_K(2)\). The square-class count is \[|S|=4q_0^e\] by [lam2005quadratic, VI.2, Theorem 2.22, p. 162]. Here \(e=0\) in odd residue characteristic. Over \(\mathbb Q_2\), \(q_0=2\) and \(e=1\), so \(|S|=8\); see also [lam2005quadratic, VI.2, Corollary 2.24(1), p. 163]. Combining this count with Proposition 27 gives the following Spin indices; the middle column means odd residue characteristic. \[\begin {array}{c|c|c} Q&\text {odd}&\mathbb Q_2\\ \hline \text {anis. binary}&2&4\\ \text {split binary}&4&8\\ \dim Q\geq 3&4&8 \end {array}\] The rank-zero and rank-one indices remain one. The characteristic restriction is on \(K\); residue characteristic two is included.

For a concrete dyadic contrast, \(x^2+y^2\) is anisotropic over \(\mathbb Q_2\): a nontrivial zero would make \(-1\) a square, but a 2-adic unit square is \(1\) modulo \(8\), whereas \(-1\) is \(7\) modulo \(8\) by the cited Corollary 2.24(1). Its Spin image therefore has index four, although its spinor-norm image has index two in \(S\). For the nondegenerate ternary form \(Q(x,y,z)=xy+z^2\), vectors \((1,c,0)\) and \((1,1,0)\) have values \(c\) and \(1\). Their reflection product realizes \([c]\) for every \(c\in \mathbb Q_2^\times \), and the Spin image has index eight.

The two-reflection assertion and its surjectivity consequence are TauCeti.QuadraticMap.exists_reflectionPairSpecialOrthogonal_spinorNorm_eq and TauCeti.QuadraticMap.spinorNorm_surjective_of_three_le_finrank. The count is TauCeti.natCard_squareClassGroup, and the resulting Spin index is TauCeti.QuadraticMap.index_range_spinToSpecialOrthogonal_of_three_le_finrank. The reflection and index statements assume finite dimension, nondegeneracy, invertible two and dimension at least three over a nonarchimedean local field. The square-class count needs only that field setting and \(2\ne 0\).

On the rational hyperbolic plane with basis \(u,v\), put \(q(au+bv)=ab\). Its unhalved polar form has matrix \(\left (\begin {smallmatrix}0&1\\1&0\end {smallmatrix}\right )\), so it is nondegenerate over both \(\mathbb {Q}\) and \(\mathbb {Q}_7\). We construct a rational special orthogonal transformation with no rational Spin lift, then exhibit its lift over \(\mathbb {Q}_7\). This specializes the scalar-extension criterion of Theorem 10.

For \(c\ne 0\), write \(r_c=r_{u+cv}\). The reflection formula \(r_z(w)=w-B_q(w,z)z/q(z)\) gives, in the ordered basis \(u,v\), \[\begin {gathered} r_c=\begin {pmatrix}0&-c^{-1}\\-c&0\end {pmatrix},\\ g=r_2r_1=\begin {pmatrix}1/2&0\\0&2\end {pmatrix}. \end {gathered}\] Thus \(g\) preserves \(q\) and has determinant one. Since \(q(u+2v)=2\) and \(q(u+v)=1\), its spinor norm is \[\nu _q(g)=[2]_{\mathbb {Q}}\] by Proposition 8. This class is nontrivial: if \((a/b)^2=2\) for coprime integers \(a,b\) with \(b\ne 0\), then \(a^2=2b^2\) first makes \(a\) even and then makes \(b\) even, a contradiction. The image/kernel theorem Theorem 9 therefore rules out a rational Spin lift of \(g\).

In \(\mathbb {Z}_7\), take \(f(T)=T^2-2\). We have \(f(3)=7\) and \(f'(3)=6\), a unit. Hensel's lemma [lam2005quadratic, VI.2, Theorem 2.18, p. 161] gives \[\begin {gathered} \alpha \in \mathbb {Z}_7,\qquad \alpha ^2=2,\\ \alpha \equiv 3\pmod {7}. \end {gathered}\] Indeed, in the theorem use the ideal \(7\mathbb {Z}_7\) and \(e=f'(3)=6\): since \(e\) is a unit, \(f(3)\in e^2(7\mathbb {Z}_7)\). In Mathlib's norm formulation hensels_lemma, the same input satisfies \(|f(3)|_7=1/7<1=|f'(3)|_7^2\). In particular \(\alpha \ne 0\) and \([2]_{\mathbb {Q}_7}=1\).

Identify \(\mathbb {Q}_7\otimes _{\mathbb {Q}}V\) with the hyperbolic plane over \(\mathbb {Q}_7\), and denote the extended form and transformation by \(q_7,g_7\). Put \(\mathcal {S}_K=K^{\times }/(K^{\times })^2\). The square in Theorem 10 becomes

Suppress the Clifford inclusion symbols and use \(u^2=v^2=0\), \(uv+vu=1\) in \(\mathcal {C}\kern -2pt\ell (q_7)\). Set \(p=uv\) and \(x=(u+2v)(u+v)\). Then \[\begin {gathered} p^2=u(vu)v,\\ u(vu)v=u(1-uv)v=p,\\ x=uv+2vu=2-p,\\ \operatorname {rev}(x)=(u+v)(u+2v),\\ \operatorname {rev}(x)=1+p,\\ \operatorname {rev}(x)x=(1+p)(2-p),\\ (1+p)(2-p)=2. \end {gathered}\] Define \[s=\frac {x}{\alpha } =\left (\frac {u+2v}{\alpha }\right )(u+v).\] Both displayed vector factors have quadratic value one. They are Clifford units in the vector-generated Lipschitz carrier; their even product has reverse norm \(2/\alpha ^2=1\). On an even element the star and reverse norms agree by Remark [fcap-0028]. Thus \(s\) lies in the actual \(\operatorname {Spin}(q_7)\), by the product-square construction Theorem [fcap-000C]. Rescaling a nonisotropic vector leaves its reflection unchanged, so the Spin action of \(s\) is \[r_{(u+2v)/\alpha }\,r_{u+v}=r_2r_1=g_7.\] This is the normalized-pair construction CliffordAlgebra.spinReflectionPair and its action CliffordAlgebra.spinToOrthogonal_spinReflectionPair: the constructor assumes both quadratic values are one, and the action identity also assumes that two is invertible. These declarations certify the general pair construction; the arithmetic specialization above is proved here.

The extension \(\mathbb {Q}\subset \mathbb {Q}_7\) has killed this particular square-class obstruction. The quadratic-extension example Proposition 11 exhibits the same class becoming trivial over \(\mathbb {Q}(\sqrt {2})\) for a different quadratic form. Here the Hensel root and the displayed Clifford product give a lift at the single completion \(\mathbb {Q}_7\).

Let \(V\) be a finite-dimensional rational vector space and let \(Q\) be nondegenerate. For each rational prime \(p\), put \(V_p=\mathbb Q_p\otimes _{\mathbb Q}V\) and let \(Q_p\) be the extended form. Write \[\begin {gathered} O_p=O(Q_p),\\ SO_p=SO(Q_p),\\ \operatorname {Spin}_p=\operatorname {Spin}(Q_p),\\ \operatorname {Spin}_p\xrightarrow {\rho _p}SO_p\xrightarrow {i_p}O_p. \end {gathered}\] Here \(i_p\) is inclusion and \(\rho _p\) is the vector action. Spin is the actual vector-generated even norm-one carrier of Remark [fcap-0028], with the canonical local topology of Definition 22. The actions are continuous by Lemma 23. For a rational orthogonal or Spin point \(x\), write \(x_p\) for its scalar extension; the action compatibility is Theorem 10.

A compatible compact-open reference tuple for \(Q\) consists of subgroups \[U_p^O\leq O_p,\qquad U_p^{\operatorname {Spin}}\leq \operatorname {Spin}_p\] at every prime, subject to the following requirements.

1. Each subgroup is compact and open in its ambient local group.
2. The reference groups respect the vector action: \[i_p\rho _p(U_p^{\operatorname {Spin}})\subseteq U_p^O.\]
3. For each \(g\in O(Q)\), there is a finite set \(S_O(g)\) of primes such that \(g_p\in U_p^O\) whenever \(p\notin S_O(g)\).
4. For each \(s\in \operatorname {Spin}(Q)\), there is a finite set \(S_{\operatorname {Spin}}(s)\) such that \(s_p\in U_p^{\operatorname {Spin}}\) whenever \(p\notin S_{\operatorname {Spin}}(s)\).

The exceptional sets may depend on the rational point. The special orthogonal reference subgroup is determined by these data: \[U_p^{SO}=i_p^{-1}(U_p^O).\] Thus an element of \(SO_p\) belongs to \(U_p^{SO}\) exactly when its underlying orthogonal transformation belongs to \(U_p^O\), and \(\rho _p\) restricts to \(U_p^{\operatorname {Spin}}\to U_p^{SO}\).

The subgroup \(U_p^{SO}\) is open by continuity of \(i_p\). It is compact because \(i_p\) is the closed embedding cut out by \(\det =1\), as in Lemma 23: its image inside \(U_p^O\) is closed in that compact set. If \(g\in SO(Q)\), determinant commutes with scalar extension, so the rational orthogonal membership condition gives \(g_p\in U_p^{SO}\) outside \(S_O(i(g))\), where \(i:SO(Q)\to O(Q)\) is inclusion. No further special orthogonal family or exceptional-set axiom is needed.

For an affine finite-type scheme over a discrete valuation ring, its integral points are open and closed in its fraction-field points, as in [conrad2011adelic, Example 2.3, p. 3]. The paired orthogonal and Spin data above additionally impose compatibility and rational membership. TauCeti packages those exact fields in TauCeti.QuadraticMap.OrthogonalCompactOpens and defines the derived subgroup in TauCeti.QuadraticMap.OrthogonalCompactOpens.specialOrthogonal. Its compactness is TauCeti.QuadraticMap.OrthogonalCompactOpens.isCompact_specialOrthogonal. The formal structure allows arbitrary rational quadratic forms; the nondegenerate setting here supplies the existence construction in Proposition 31.

Let \(Q\) be a nondegenerate quadratic form on a finite-dimensional rational space \(V\), with basis \(b=(b_1,\ldots ,b_n)\). Use the local groups and maps of Definition 30. Let \(\mathbb Z_p\subseteq \mathbb Q_p\) be the ring of \(p\)-adic integers, and put \[\begin {gathered} b_{i,p}=1\otimes b_i,\\ L_p=\sum _{i=1}^n\mathbb Z_p b_{i,p},\\ H_p=\{g\in O_p:gL_p=L_p\}. \end {gathered}\] Then the choices \[\begin {gathered} U_p^O=H_p,\\ U_p^{\operatorname {Spin}}=(i_p\rho _p)^{-1}(H_p),\\ U_p^{SO}=i_p^{-1}(H_p) \end {gathered}\] form a compatible compact-open reference tuple. The Spin condition is integrality of its orthogonal action in both directions; it imposes no separate Clifford-coordinate integral model.

For example, in the hyperbolic plane \(Q(x,y)=xy\) with its standard rational basis, \(g=\operatorname {diag}(2,1/2)\) preserves \(Q\) and has determinant one. Both \(g\) and \(g^{-1}\) have integral entries at every prime except \(2\); thus \(S_O(g)=\{2\}\) works, and \(g_2\notin H_2\). This is the rational instance of the torus in Example 26, and makes the point-dependent denominator condition explicit.

The matrix proof is a direct calculation using the local affine topology of [conrad2011adelic, Proposition 2.1 and its proof, p. 2]; the compact Spin preimage is the deduction from Theorem 25 above. TauCeti's TauCeti.QuadraticMap.isCompact_integralOrthogonalSubgroup also permits degenerate local forms, whereas TauCeti.CliffordAlgebra.isCompact_integralSpinSubgroup requires nondegeneracy. The complete tuple is constructed in TauCeti.QuadraticMap.OrthogonalCompactOpens.integral for a nondegenerate rational quadratic form and a finite rational basis. These references concern the chosen subgroups; they assert no surjectivity of the restricted Spin action onto the orthogonal reference.

Let \(Q\) be nondegenerate on a finite-dimensional rational space \(V\). The compatible compact-open reference tuples constructed from any two rational bases in Proposition 31 agree at all but finitely many primes, in each of their O, SO and Spin families.

There is also a finite shrinking operation. Given any compatible tuple \(U\), choose open subgroups \(W_p\leq O_p\) and a finite set \(F\) such that \(U_p^O\subseteq W_p\) for \(p\notin F\). Then \[\begin {gathered} \widetilde U_p^O=U_p^O\cap W_p,\\ \widetilde U_p^{\operatorname {Spin}} =U_p^{\operatorname {Spin}}\cap (i_p\rho _p)^{-1}(W_p),\\ \widetilde U_p^{SO}=i_p^{-1}(\widetilde U_p^O) \end {gathered}\] is another compatible tuple, contained in \(U\) at every prime and equal to it outside \(F\). In particular one may take \(W_p=O_p\) outside a chosen finite set. The maps \(i_p\) and \(\rho _p\) are those of Definition 30.

For a concrete basis change in positive dimension, replace \(b_1\) by \(2b_1\) and leave the other basis vectors fixed. The two change matrices have diagonal entries \(2\) and \(1/2\), respectively, with all other diagonal entries \(1\). Thus \(F_b=\{2\}\) suffices. The two lattices agree at every odd prime, while at \(2\) the new lattice is strictly smaller. This does not assert that their orthogonal stabilizers must differ at \(2\).

These are deductions from the lattice construction in Proposition 31 and the continuous local action, using the coordinate topology of [conrad2011adelic, Proposition 2.1, p. 2]. The basis comparison is formalized by TauCeti.QuadraticMap.eventually_integralOrthogonalSubgroup_baseChange_eq, which also permits degenerate forms. The compatible shrinking construction is TauCeti.QuadraticMap.OrthogonalCompactOpens.infOpenSubgroup. Neither construction requires a lift of an arbitrary integral orthogonal point to Spin.

Let \(G_p\) be a Hausdorff locally compact topological group at each rational prime, and choose a compact open subgroup \(U_p\leq G_p\). The restricted product relative to \(U=(U_p)\) is \[G_f(U)=\prod _p'(G_p,U_p).\] It consists of the tuples \((g_p)\in \prod _pG_p\) for which \(g_p\in U_p\) at all but finitely many primes. For a finite set \(S\) of primes its principal stage is \[G_S(U)=\prod _{p\in S}G_p\times \prod _{p\notin S}U_p,\] regarded as a subset of \(G_f(U)\) and given the product topology. The restricted-product topology declares \(A\subseteq G_f(U)\) open exactly when \(A\cap G_S(U)\) is open in every principal stage. Multiplication and inversion are coordinatewise. The product reference subgroup is \[K(U)=\prod _pU_p=G_{\varnothing }(U).\]

For example, take the hyperbolic plane \(Q(x,y)=xy\) and the references from its standard rational basis in Proposition 31. The tuple whose \(2\)-component is \(\operatorname {diag}(2,1/2)\) and whose other components are identities belongs to \(G_{\{2\}}(U)\) for \(G_p=O_p\), but not to \(K(U)\). The finite exceptional set permits a nonintegral component without discarding the restrictions at all other primes.

With this topology, \(G_f(U)\) is a Hausdorff locally compact topological group, each \(G_S(U)\) is an open subspace with precisely its product topology, and \(K(U)\) is compact and open. Every coordinate evaluation \((g_q)\mapsto g_p\) is continuous.

For a compatible compact-open reference tuple, apply this construction to the three local families to define the finite adelic orthogonal, special orthogonal and Spin groups: \[\begin {gathered} O_f(U)=\prod _p'(O_p,U_p^O),\\ SO_f(U)=\prod _p'(SO_p,U_p^{SO}),\\ \operatorname {Spin}_f(U)=\prod _p'(\operatorname {Spin}_p,U_p^{\operatorname {Spin}}). \end {gathered}\] The local topological groups are supplied by Lemma 23. The construction applies to the derived SO references as well as to the chosen O and Spin references. In dimension zero all three restricted products are singleton groups. Here the notation retains the chosen tuple; an arbitrary compatible tuple has not been identified with the integral points of an affine scheme.

Finite changes of references leave the ambient group and its topology unchanged. More precisely, suppose \(U'_p=U_p\) outside a finite set \(F\). A tuple restricted for one family is restricted for the other after adjoining \(F\) to its exceptions. The identity in every coordinate is thus a group isomorphism \(G_f(U)\to G_f(U')\). On a stage it factors as \[G_S(U)\longrightarrow G_{S\cup F}(U')\longrightarrow G_f(U').\] The first map is continuous: outside \(S\cup F\) the reference factors coincide, and at the finitely many remaining factors it is either the identity on \(G_p\) or the inclusion \(U_p\hookrightarrow G_p\). Stagewise continuity gives continuity on the union. Interchanging \(U\) and \(U'\) proves continuity of the inverse. Consequently the changes in Proposition 32 identify the finite adelic topological groups by the coordinate identity.

This identity need not send \(K(U)\) onto \(K(U')\). If, for example, \(U'_{p_0}\) is a proper subgroup of \(U_{p_0}\), choose \(u\in U_{p_0}\setminus U'_{p_0}\). The tuple with component \(u\) at \(p_0\) and identities elsewhere belongs to \(K(U)\) but not to \(K(U')\). Thus the ambient topology and the chosen compact open subgroup are separate data. Continuity of all coordinate evaluations also shows that the restricted-product topology is at least as fine as the topology inherited from \(\prod _pG_p\).

The classical affine adelic construction uses finite stages and open transition maps in [conrad2011adelic, Theorem 3.6, pp. 6-8]; compactness of integral points and the resulting locally compact topology occur in [conrad2011adelic, Corollary 3.7 and Section 4 opening, p. 9]. The argument above proves the construction directly for the chosen compact-open group references. Mathlib's RestrictedProduct.isOpenEmbedding_inclusion_principal and RestrictedProduct.locallyCompactSpace_of_group support the stage and local compactness assertions. TauCeti's TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicOrthogonal, TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonal and TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpin define the three specializations. The coordinate identity and its continuity are TauCeti.restrictedProductCongr and TauCeti.continuous_restrictedProductCongr.

Use the Hausdorff locally compact groups \(G_p\) and compact open references \(U_p\) of Definition 33. For any set \(R\) of rational primes, the away restricted product is \[G_f^R(U)=\prod _{p\notin R}'(G_p,U_p).\] Its tuples have only finitely many exceptions to \(g_p\in U_p\) among the primes outside \(R\). Its topology is defined by the same principal-stage construction, now indexed by finite sets \(T\subseteq \{p:p\notin R\}\): \[G_T^R(U)=\prod _{p\in T}G_p\times \prod _{p\notin R\cup T}U_p.\] The proof in Definition 33 applies to this index set too. Thus \(G_f^R(U)\) is a Hausdorff locally compact topological group, and each displayed stage is open with its product topology.

Deleting the coordinates in \(R\) defines a continuous group homomorphism \[\begin {aligned} r_R:G_f(U)&\longrightarrow G_f^R(U),\\ (g_p)_p&\longmapsto (g_p)_{p\notin R}. \end {aligned}\] Indeed, a finite exceptional set \(S\) restricts to \(S\setminus R\), so the map is well defined. On the open stage \(G_S(U)\) it is the product-coordinate restriction \(G_S(U)\to G_{S\setminus R}^R(U)\), followed by the continuous stage inclusion. These restrictions are continuous, and the stages cover the source, proving continuity of \(r_R\). Coordinatewise operations prove the homomorphism assertion.

For \(R=\varnothing \), the away group and restriction are \(G_f(U)\) and its identity map. If \(R\) is the set of all primes, the complement is empty, so the away group is the one-point group and restriction is its unique incoming homomorphism. No finiteness of \(R\) is needed for the definition or for continuity.

If \(R\) is finite, separating its coordinates gives the finite-prime splitting, a topological group isomorphism \[\begin {aligned} d_R:G_f(U)&\longrightarrow \Bigl (\prod _{p\in R}G_p\Bigr )\times G_f^R(U),\\ (g_p)_p&\longmapsto \bigl ((g_p)_{p\in R},r_R(g)\bigr ). \end {aligned}\] The target carries the product topology. In particular the removed prime factors are unrestricted. For the hyperbolic-plane tuple in Definition 33, choosing \(R=\{2\}\) gives \(d_R(g)=(\operatorname {diag}(2,1/2),1)\). Reinserting that component recovers the tuple, even though its \(2\)-component is outside \(U_2\).

If \(R\) is infinite, the removed coordinates must retain their own restricted-product condition. An unrestricted family on \(R\) can have infinitely many components outside \(U_p\); reinserting it would not define a point of \(G_f(U)\). Thus the finite-prime formula does not extend by simply allowing infinite \(R\). The appropriate removed-coordinate factor is \(\prod _{p\in R}'(G_p,U_p)\). At the level of tuples this and the away factor split the finite exceptional set into two finite sets; conversely their union is finite. The resulting group isomorphism is also a homeomorphism: on each open product of two principal stages, reinsertion is a product rearrangement into the stage indexed by their union; restriction is continuous on every source stage. This also covers the empty and all-prime boundaries.

For a compatible compact-open reference tuple, the same construction defines \(O_f^R(U)\), \(SO_f^R(U)\) and \(\operatorname {Spin}_f^R(U)\) by taking the local families \(O_p\), \(SO_p\) and \(\operatorname {Spin}_p\) and their respective reference subgroups. The finite-prime splitting is a direct consequence of the stage topology; the classical affine adelic finite-stage decomposition is [conrad2011adelic, Theorem 3.6, equation (3.6.1), pp. 6-8].

TauCeti's TauCeti.RestrictedProductGroupAway defines the arbitrary-set carrier, and TauCeti.restrictAway with TauCeti.continuous_restrictAway supplies restriction. The finite-set splitting and its two continuity directions are TauCeti.awayDecomposition, TauCeti.continuous_awayDecomposition and TauCeti.continuous_awayDecomposition_symm. Its forward continuity does not need open references; inverse continuity assumes openness on the away coordinates, which our compact-open tuple supplies. The three specialized carriers are TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicOrthogonal, TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpecialOrthogonal and TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpin.

Let \(Q\) be a nondegenerate quadratic form on a finite-dimensional rational vector space \(V\), and choose a compatible compact-open reference tuple. Extend scalars to \(V_\infty =\mathbb R\otimes _{\mathbb Q}V\), with quadratic form \(Q_\infty \). Write \(O_\infty \), \(SO_\infty \) and \(\operatorname {Spin}_\infty \) for its real groups with the canonical topologies of Definition 22. In particular \(\operatorname {Spin}_\infty \) uses the actual vector-generated, even, reverse-norm-one carrier of Lemma 23.

The full adelic orthogonal, special orthogonal and Spin groups relative to the chosen references are \[\begin {aligned} O_{\mathbb A}(U)&=O_\infty \times O_f(U),\\ SO_{\mathbb A}(U)&=SO_\infty \times SO_f(U),\\ \operatorname {Spin}_{\mathbb A}(U)&=\operatorname {Spin}_\infty \times \operatorname {Spin}_f(U). \end {aligned}\] The finite factors are those of Definition 33. In each case take the ordinary product topology and coordinatewise group operations. There is no reference-subgroup condition at the real place: its factor is unrestricted. More generally write \(G_{\mathbb A}(U)=G_\infty \times G_f(U)\) for any of these three constructions. They are Hausdorff locally compact topological groups.

Indeed, Lemma 23 gives those properties for the real factor, and Definition 33 gives them for the finite factor. Multiplication and inversion are continuous in each component, hence in the product topology. Products of separating neighborhoods give the Hausdorff property. At each point choose compact neighborhoods in the two factors; their product is a compact neighborhood, proving local compactness. The finite-coordinate projection is the continuous group homomorphism \[\begin {aligned} \pi _f:G_{\mathbb A}(U)&\longrightarrow G_f(U),\\ (g_\infty ,g_f)&\longmapsto g_f. \end {aligned}\] Continuity is the defining property of the product topology, and the homomorphism identity follows from coordinatewise multiplication.

For example, take the hyperbolic plane \(Q(x,y)=xy\). For \(t>0\), the real matrix \(h_t=\operatorname {diag}(t,t^{-1})\) preserves \(Q\) and has determinant one. Thus \((h_t,1)\) is a point of \(SO_{\mathbb A}(U)\) for every \(t>0\), with identity at every finite prime. The nonidentity matrices \(h_t\) approach the identity as \(t\to 1\), exhibiting a nondiscrete real factor.

Let \(K(U)=\prod _pU_p\) be the compact open reference subgroup of the finite factor. The subgroup \(\{1\}\times K(U)\) of the full group is compact, but is not open when \(G_\infty \) is nondiscrete. Compactness follows from compactness of both factors. If the subgroup were open, its inverse image under the continuous map \(g\mapsto (g,1)\) would make \(\{1\}\) open in \(G_\infty \). Translations would then make every singleton open, contradicting nondiscreteness. Instead, for each open identity neighborhood \(W_\infty \subseteq G_\infty \), the set \(W_\infty \times K(U)\) is an open identity neighborhood in the full group. A compact real identity neighborhood \(C_\infty \) gives the compact identity neighborhood \(C_\infty \times K(U)\), without asserting that it is open. In dimension zero all three real and finite groups are singletons, so the nondiscreteness qualification is essential.

The unrestricted archimedean factors and the finite-place conditions occur together in the classical affine adelic stage formula of [conrad2011adelic, Theorem 3.6, equation (3.6.1), pp. 6-8]. Here the product construction is explicit for the chosen group references; it makes no additional identification with integral points of an affine scheme. TauCeti's TauCeti.RestrictedProductGroupWithFactor is the general carrier with an extra unrestricted factor. The three specializations are TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicOrthogonal, TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpecialOrthogonal and TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpin. The corresponding continuous finite projections are TauCeti.QuadraticMap.OrthogonalCompactOpens.continuous_fullAdelicOrthogonalToFinite, TauCeti.QuadraticMap.OrthogonalCompactOpens.continuous_fullAdelicSpecialOrthogonalToFinite and TauCeti.QuadraticMap.OrthogonalCompactOpens.continuous_fullAdelicSpinToFinite.

Use the hyperbolic plane \(Q(x,y)=xy\) and the integral orthogonal references of the example in Definition 33. Enumerate the rational primes without repetition as \(p_1,p_2,\ldots \). Define \(x_n\in O_f(U)\) by \[(x_n)_p=\begin {cases} \operatorname {diag}(p_n,p_n^{-1})&p=p_n,\\ 1&p\ne p_n. \end {cases}\] The exceptional diagonal matrix preserves \(xy\), and every other component is the identity. Thus \(x_n\) belongs to the principal stage \(O_{\{p_n\}}(U)\).

For each fixed prime \(p\), the coordinate \((x_n)_p\) is the identity for all but at most one \(n\). Hence \(x_n\to 1\) in the topology inherited from the unrestricted product \(\prod _pO_p\). Explicitly, a basic product neighborhood of the identity restricts only a finite set \(F\) of coordinates. Once the moving prime has passed every prime in \(F\), all those coordinates equal the identity, so the tuple belongs to that neighborhood.

In contrast, \(x_n\notin K(U)=\prod _pU_p^O\) for every \(n\): the entry \(p_n^{-1}\) is not in \(\mathbb Z_{p_n}\), so its matrix does not preserve the standard integral lattice. Since \(K(U)\) is an open identity neighborhood in the restricted-product topology, the sequence does not converge to the identity there. Coordinate continuity in Definition 33 gives one topology inclusion; this sequence proves that the restricted-product topology is strictly finer in this example.

For the classical open-stage topology, see [conrad2011adelic, Section 4 opening, p. 9] and its finite-stage formula in Theorem 3.6. The calculation above isolates what that topology detects: the nonintegral coordinate keeps moving, although every fixed coordinate eventually becomes the identity.

Let \(Q\) be a nondegenerate quadratic form on a rational vector space of finite dimension \(n\), with a compatible reference tuple \(U\) as in Definition 30. Let \(R\) be any set of primes. The local maps \(\rho _p:\operatorname {Spin}_p\to SO_p\) and \(i_p:SO_p\hookrightarrow O_p\) induce continuous group homomorphisms \[\begin {gathered} \operatorname {Spin}_f(U)\xrightarrow {\rho _f}SO_f(U)\xrightarrow {i_f}O_f(U),\\ \operatorname {Spin}_f^R(U)\xrightarrow {\rho ^R}SO_f^R(U)\xrightarrow {i^R}O_f^R(U),\\ \operatorname {Spin}_{\mathbb A}(U)\xrightarrow {\rho _{\mathbb A}} SO_{\mathbb A}(U)\xrightarrow {i_{\mathbb A}}O_{\mathbb A}(U). \end {gathered}\] The groups are defined in Definition 33, Definition 34 and Definition 35. Each \(i\) is injective, with image exactly the orthogonal tuples of determinant one at every retained place, including the real place for the full group. These maps commute with forgetting the real component and with deleting the primes in \(R\).

If \(n>0\), their Spin projection kernels are, as groups, \[\begin {aligned} \ker \rho _f&\cong \prod _p\{1,-1\},\\ \ker \rho ^R&\cong \prod _{p\notin R}\{1,-1\},\\ \ker \rho _{\mathbb A}&\cong \{1,-1\}\times \prod _p\{1,-1\}. \end {aligned}\] Every sign family occurs, with an independent real sign in the full case. These are algebraic identifications. If \(n=0\), all the groups and kernels above are singletons. If \(R\) contains every prime, the away groups and the empty sign product are singletons even when \(n>0\).

Proof. 

First consider continuous homomorphisms \(f_p:G_p\to H_p\) between the local groups of two restricted products, with \(f_p(U_p)\subseteq U'_p\) for every prime. If \(g\) has exceptional set \(S\), the tuple \((f_p(g_p))_p\) has exceptional set contained in \(S\). Thus coordinatewise application defines a homomorphism \(f:G_f(U)\to H_f(U')\). On each principal stage it factors through \[G_S(U)\longrightarrow H_S(U')\longrightarrow H_f(U').\] For \(p\in S\) use \(f_p\); outside \(S\) use its continuous restriction \(U_p\to U'_p\), with the subgroup topologies. The resulting product map is continuous. The second map is the continuous stage inclusion. Since the source stages form an open cover, \(f\) is continuous on the whole restricted product. The same proof on the index set \(\{p:p\notin R\}\) gives the arbitrary-away construction.

Compatibility of \(U\) says exactly that \(\rho _p\) preserves the Spin and SO references, while \(U_p^{SO}=i_p^{-1}(U_p^O)\) says that \(i_p\) preserves the SO and O references. Their local continuity is Lemma 23, so the preceding argument gives the finite and away maps. For the full maps take the product with the actual continuous real maps \(\rho _\infty \) and \(i_\infty \) from that same local result. Products of continuous homomorphisms are continuous homomorphisms. In particular \[\rho _{\mathbb A}(s_\infty ,s_f) =(\rho _\infty (s_\infty ),\rho _f(s_f)).\]

Each local \(i_p\) is injective, so equality of images determines every coordinate and proves injectivity of \(i_f\) and \(i^R\). The real inclusion gives injectivity for \(i_{\mathbb A}\) too. Their images have determinant one at every place by definition. Conversely, let an orthogonal restricted tuple \(g\) have determinant one everywhere. Each \(g_p\) has a unique preimage \(h_p\in SO_p\). If \(S\) is an exceptional set for \(g\), then for \(p\notin S\), \[g_p\in U_p^O\quad \Longrightarrow \quad h_p\in i_p^{-1}(U_p^O)=U_p^{SO}.\] Thus \(h\) is restricted and maps to \(g\). Restricting the argument to \(p\notin R\) proves the away image criterion. In the full case, the real determinant-one condition supplies the unique real SO preimage as well. If no prime remains, the away criterion is vacuous and both sides are singleton groups.

Write \(\pi _f^{\operatorname {Spin}}\) and \(\pi _f^{SO}\) for the projections that forget the real component. The square

commutes because either path sends \((s_\infty ,(s_p)_p)\) to \((\rho _p(s_p))_p\). Replacing Spin and SO by SO and O gives the same square for \(i\), since both paths retain \((i_p(h_p))_p\). Deleting \(R\) commutes with each map for the same reason: both orders give \(\rho _p(s_p)\) or \(i_p(h_p)\) at every \(p\notin R\). This also proves the full-to-away identities by composition.

Suppose now that \(n>0\). The scalar-kernel theorem of Lemma 17, applied over \(\mathbb Q_p\) and \(\mathbb R\), says that the local Spin projection kernel consists of the two scalar elements \(1,-1\). Scalar extension preserves dimension and nondegeneracy. An existing restricted Spin element therefore lies in the kernel exactly when each retained coordinate is a scalar sign; in the full case the real component must also be a sign.

It remains to show that arbitrary choices of signs really are restricted. Apply the rational membership axiom of Definition 30 to the single rational Spin element \(-1\), which exists by Lemma 17. Scalar extension carries it to the local scalar \(-1\): the Clifford algebra map preserves \(1\) and negation, as in Theorem 10. There is consequently one finite set \(F\) such that \(-1\in U_p^{\operatorname {Spin}}\) for every \(p\notin F\). Also \(1\in U_p^{\operatorname {Spin}}\) at every prime. Every family \((\varepsilon _p)_p\in \prod _p\{1,-1\}\) is therefore restricted, with its exceptional set contained in this same \(F\), independently of the choices of signs. It lies in the projection kernel by the local scalar-kernel theorem.

Sending a sign family to its scalar tuple is injective because \(1\ne -1\) over these characteristic-zero fields, and is surjective onto the kernel by the existing-element criterion. It respects multiplication coordinatewise, proving the finite group isomorphism. Restricting the family and \(F\) to the complement of \(R\) gives the away isomorphism, including an empty complement. The real scalar sign is unrestricted and independent, giving the full product. Finally, if \(n=0\), Lemma [fcap-003H] identifies the actual generated Spin carrier with the identity subgroup; the orthogonal and special orthogonal groups are also trivial. Scalar extension and products preserve these singleton descriptions, so no extra scalar \(-1\) is introduced in that case.

For example, in positive dimension choose \(\varepsilon _2=-1\) and \(\varepsilon _p=1\) at every other prime. This is a kernel element distinct from both constant sign families. In the full group either real sign can accompany it. These projection kernels are different from the kernel of the spinor norm in Theorem 9: the present maps start in Spin and record its scalar ambiguity.

The classical finite-stage functoriality is described in [conrad2011adelic, Theorem 3.6 and the paragraph following its proof, pp. 6-8]. The real scalar-kernel prototype appears in [gallier2014clifford, Section 1.8, Proposition 1.21, pp. 39-40]. Gallier's Definition 1.6 uses norm \(\pm 1\); the local input here is the norm-one field theorem in Lemma 17. In particular this argument makes no claim that the Spin projections are surjective.

The generic construction and its continuity are supported by TauCeti.restrictedProductMapOfForall and TauCeti.continuous_restrictedProductMapOfForall. The specialized continuity results are TauCeti.QuadraticMap.OrthogonalCompactOpens.continuous_finiteAdelicSpinToSpecialOrthogonal, TauCeti.QuadraticMap.OrthogonalCompactOpens.continuous_awayAdelicSpinToSpecialOrthogonal and TauCeti.QuadraticMap.OrthogonalCompactOpens.continuous_fullAdelicSpinToSpecialOrthogonal. For SO inclusion, the image criteria are TauCeti.QuadraticMap.OrthogonalCompactOpens.mem_range_finiteAdelicSpecialOrthogonalToOrthogonal_iff, TauCeti.QuadraticMap.OrthogonalCompactOpens.mem_range_awayAdelicSpecialOrthogonalToOrthogonal_iff and TauCeti.QuadraticMap.OrthogonalCompactOpens.mem_range_fullAdelicSpecialOrthogonalToOrthogonal_iff.

The displayed square is TauCeti.QuadraticMap.OrthogonalCompactOpens.fullAdelicSpecialOrthogonalToFinite_comp_fullAdelicSpinToSpecialOrthogonal; deletion compatibility is TauCeti.QuadraticMap.OrthogonalCompactOpens.awayAdelicSpinToSpecialOrthogonal_comp_restrictAway. The existing-element kernel criteria are TauCeti.QuadraticMap.OrthogonalCompactOpens.mem_ker_finiteAdelicSpinToSpecialOrthogonal_iff, TauCeti.QuadraticMap.OrthogonalCompactOpens.mem_ker_awayAdelicSpinToSpecialOrthogonal_iff and TauCeti.QuadraticMap.OrthogonalCompactOpens.mem_ker_fullAdelicSpinToSpecialOrthogonal_iff. They support the coordinate criteria; the proof that every sign family occurs is the additional rational \(-1\) argument above.

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

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

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

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

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

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

Let \(Q\) be nondegenerate on a finite-dimensional rational space \(V\), choose a compatible compact-open reference tuple \(U\), and fix a rational basis \(b\). Let \(L_p\) be its \(\mathbb Z_p\)-span and \(H_p=\{g\in O_p:gL_p=L_p\}\) as in Proposition 31. Assume the eventual lattice containment \[U_p^O\subseteq H_p\quad \text {for all but finitely many primes }p.\] Then each rational diagonal subgroup \[\delta _{\mathbb A}^O(O(Q)),\qquad \delta _{\mathbb A}^{SO}(SO(Q)),\qquad \delta _{\mathbb A}^{\operatorname {Spin}}(\operatorname {Spin}(Q))\] is discrete in its full adelic group. In particular this holds for the integral tuple of Proposition 31, its rational-basis changes and its finite shrinkings from Proposition 32.

The separation has two independent parts: finite-place integrality forces rational matrix entries to be integers, and the real bound then forces the identity matrix. The finite projection discards the second condition. With the rational groups given the discrete topology, injectivity and the proved discrete images make these full diagonals topological embeddings; this argument asserts no such property for the finite diagonals.

[conrad2011adelic, Example 2.3, p. 3] proves discreteness for rational points in classical affine full adelic points. The proof above supplies the chosen-tuple version under its explicit containment hypothesis, using Lemma 17 for the Spin scalar kernel. The exact O and SO criteria are TauCeti.QuadraticMap.OrthogonalCompactOpens.discreteTopology_range_fullAdelicOrthogonalDiagonal_of_eventually_integral and TauCeti.QuadraticMap.OrthogonalCompactOpens.discreteTopology_range_fullAdelicSpecialOrthogonalDiagonal_of_eventually_integral; these two formal statements even allow degenerate forms. TauCeti's TauCeti.QuadraticMap.OrthogonalCompactOpens.discreteTopology_range_fullAdelicSpinDiagonal proves the Spin conclusion for every nondegenerate compatible tuple, using a separate eventual-containment theorem. The explicit containment assumption is retained here to expose the neighborhood argument.

Let \(Q\) be nondegenerate on a rational vector space \(V\) of finite dimension \(d\geq 3\), and suppose that \(Q\) is isotropic. For every compatible compact-open reference tuple \(U\), the finite rational diagonal subgroup \(\delta _f^{SO}(SO(Q))\) is not discrete in \(SO_f(U)\). A sequence of nonidentity rational Eichler transvections converges to the identity while staying in one fixed principal stage.

In the explicit matrix of Example 13, take \(t=n!\). Its off-diagonal entries tend to zero at every finite prime, whereas the real entry \(t\) grows without bound. This exhibits what is lost on forgetting the real factor in Proposition 39. In dimension two, \(u^\perp =\mathbb Q u\), so the required parameter does not exist. No assertion about anisotropic forms or universal finite-diagonal nondiscreteness follows.

The transvection input is the general-field calculation in Proposition 12; its totally singular special case is [chevalley1954algebraic, III.1.7 and formula (1), pp. 73-74]. Chevalley's displayed formula assumes both parameters lie in a totally singular subspace; the proof here uses the already established arbitrary-\(Q(w)\) formula. The finite-stage topology is grounded in [conrad2011adelic, Theorem 3.6, pp. 6-8]. The factorial argument above is a deduction from these inputs. Its convergence statement is also TauCeti.QuadraticMap.OrthogonalCompactOpens.tendsto_finiteAdelicSpecialOrthogonalDiagonal_transvection_factorial; that statement needs the two polar identities but not the extra nondegeneracy and dimension assumptions used to obtain a nontrivial sequence.

Let \(Q\) be nondegenerate on a finite-dimensional rational space \(V\), and choose a compatible compact-open reference tuple \(U\). To collect the local spinor obstructions of one restricted SO tuple, the target must retain the images of its chosen reference subgroups. For each prime \(p\), put \[C_p=\mathbb Q_p^{\times }/(\mathbb Q_p^{\times })^2,\qquad \theta _p=\nu _{Q_p}:SO_p\longrightarrow C_p,\] using the reverse-norm spinor norm of Theorem 9, with multiplicative notation. Give \(C_p\) its quotient topology. Define the spinor-norm reference image and the finite adelic square-class target by \[I_p=\theta _p(U_p^{SO}),\qquad C_f(U)=\prod _p'(C_p,I_p).\] The restricted-product notation and topology are those of Definition 33; explicitly \((c_p)_p\in C_f(U)\) means \(c_p\in I_p\) for all but finitely many \(p\).

Each \(C_p\) is discrete, including at \(p=2\). Indeed, Proposition 24 proves that the square subgroup is open, using [lam2005quadratic, VI.2, Theorem 2.19 and Corollary 2.20, p. 161]. Every coset is then open, so every singleton in the quotient is open. The same local result proves that \(\theta _p\) is continuous. Since \(U_p^{SO}\) is compact, its image \(I_p\) is compact. A compact discrete set is finite: its open singleton cover has a finite subcover. Thus \(I_p\) is a finite open subgroup of \(C_p\), and the restricted product has the compact-open references required by Definition 33.

The finite adelic spinor norm is the continuous homomorphism \[\begin {aligned} \Theta :SO_f(U)&\longrightarrow C_f(U),\\ (g_p)_p&\longmapsto (\theta _p(g_p))_p. \end {aligned}\] For if \(g_p\in U_p^{SO}\) outside a finite set \(S\), then \(\theta _p(g_p)\in I_p\) outside that same set. This proves restricted membership, and the local homomorphism laws give the global homomorphism law. Continuity is the component-map argument of Proposition 37: on each principal stage the map is the product of the continuous maps \(SO_p\to C_p\) for \(p\in S\) and their restrictions \(U_p^{SO}\to I_p\) elsewhere, followed by the continuous target-stage inclusion. The open stages cover the domain.

For example, a tuple equal to \(g\in U_\ell ^{SO}\) at one prime \(\ell \) and to the identity elsewhere maps to the tuple with \(\theta _\ell (g)\in I_\ell \) at \(\ell \) and identity elsewhere. It therefore lies in the target's product reference \(\prod _p I_p\). This describes the actual reference condition without replacing \(I_p\) by the square classes of local units or asserting that it is all of \(C_p\).

If \(\dim V=0\) or \(1\), every local \(SO_p\) is trivial. In dimension one a linear automorphism is scalar multiplication, and its determinant-one condition forces that scalar to be one; dimension zero has only the identity. Therefore every \(I_p=\{1\}\) and \(\Theta \) is the trivial homomorphism. The ambient square-class groups \(C_p\) need not be trivial. No surjectivity of \(\Theta \) is asserted in any dimension.

This construction combines the local square theorem with the finite-stage functoriality described in [conrad2011adelic, Theorem 3.6 and the following paragraph, pp. 6-8]. The actual-image choice is TauCeti.QuadraticMap.OrthogonalCompactOpens.localSpinorNormImage, and its openness is TauCeti.QuadraticMap.OrthogonalCompactOpens.isOpen_localSpinorNormImage. The target and continuous map are TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSquareClasses and TauCeti.QuadraticMap.OrthogonalCompactOpens.continuous_adelicSpinorNorm. These use the same chosen references and nondegeneracy assumption. The low-rank image statement is TauCeti.QuadraticMap.OrthogonalCompactOpens.localSpinorNormImage_eq_bot_of_finrank_le_one. The compactness and finiteness of the images are the continuous-image argument given above, not a separate square-class count.

Let \(Q\) be nondegenerate on a finite-dimensional rational space \(V\), and let \(U\) be a compatible compact-open reference tuple. Use the finite adelic spinor norm \(\Theta :SO_f(U)\to C_f(U)\), with its actual reference images \(I_p=\theta _p(U_p^{SO})\). Its kernel, called the adelic spinor kernel, is \[\ker \Theta =\{g\in SO_f(U):\theta _p(g_p)=1\text { for every prime }p\}.\] Give this subgroup the subspace topology from \(SO_f(U)\). The continuous Spin projection \(\rho _f\) of Proposition 37 corestricts to a continuous homomorphism \[\bar \rho _f:\operatorname {Spin}_f(U)\longrightarrow \ker \Theta , \qquad (s_p)_p\longmapsto (\rho _p(s_p))_p.\] The formula retains exactly the same coordinates as \(\rho _f\).

The triangle records the factorization, with \(j\) the subgroup inclusion and no surjectivity assigned to either Spin arrow.

For a rational proper isometry \(g\in SO(V,Q)\), write \(\delta _f^{SO}(g)=(g_p)_p\) for its rational diagonal, and put \[j_p:\mathbb Q^{\times }/(\mathbb Q^{\times })^2\longrightarrow C_p, \qquad [a]_{\mathbb Q}\longmapsto [a]_{\mathbb Q_p}.\] Scalar-extension naturality from Theorem 10 gives \[\bigl (\Theta (\delta _f^{SO}(g))\bigr )_p =j_p\bigl (\nu _Q(g)\bigr ).\] Consequently \(\nu _Q(g)=1\) implies \(\delta _f^{SO}(g)\in \ker \Theta \), since every homomorphism \(j_p\) sends the identity to the identity. No converse is asserted. The cited naturality proof covers positive dimension; in dimension zero the identity is the only proper isometry, so the same formula holds directly. If \(\dim V\leq 1\), all local SO groups, hence \(SO_f(U)\) and \(\ker \Theta \), are trivial, as in Definition 41. In dimension zero the actual Spin carrier is also trivial Lemma [fcap-003H]; no additional scalar sign is introduced.

For an arbitrary \(g\in \ker \Theta \), Theorem 9 supplies a Spin lift of each local \(g_p\). Choosing these lifts separately does not prove that they belong to the chosen \(U_p^{\operatorname {Spin}}\) at all but finitely many primes. Thus the local lifting theorem alone does not establish surjectivity of \(\bar \rho _f\) for the chosen reference tuple.

The local reverse-norm argument is grounded in [chevalley1954algebraic, II.3.5-6, pp. 52-53], with the even-lift convention explained in Theorem 9. The kernel description and continuous corestriction above are deductions from that local theorem and the restricted-product map. Their precise formal counterparts are TauCeti.QuadraticMap.OrthogonalCompactOpens.mem_adelicSpinorKernel_iff and TauCeti.QuadraticMap.OrthogonalCompactOpens.continuous_finiteAdelicSpinToSpinorKernel. The rational coordinate identity is TauCeti.QuadraticMap.OrthogonalCompactOpens.adelicSpinorNorm_finiteAdelicSpecialOrthogonalDiagonal_apply; its trivial-norm consequence is TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalDiagonal_mem_adelicSpinorKernel. These statements retain nondegeneracy and the same chosen references.

A restricted tuple of local transformations can be changed on the left by one rational transformation and on the right by a tuple in the chosen reference subgroups. The resulting equivalence classes depend on which of O, SO or Spin is used at both ends.

Let \(Q\) be nondegenerate on a finite-dimensional rational space \(V\), with a compatible compact-open reference tuple \(U\). Use the finite adelic groups of Definition 33 and their rational diagonal subgroups. Define separately \[\begin {aligned} \Gamma _O&=\delta _f^O(O(V,Q)), & K_O&=\prod _p U_p^O,\\ \Gamma _{SO}&=\delta _f^{SO}(SO(V,Q)), & K_{SO}&=\prod _p U_p^{SO},\\ \Gamma _{\operatorname {Spin}}&=\delta _f^{\operatorname {Spin}}(\operatorname {Spin}(V,Q)), & K_{\operatorname {Spin}}&=\prod _p U_p^{\operatorname {Spin}}. \end {aligned}\] Each \(\Gamma _G\) is the actual image subgroup in \(G_f(U)\). Each \(K_G\) is its product reference subgroup, so it is compact and open by the restricted-product construction. The SO references are \(U_p^{SO}=i_p^{-1}(U_p^O)\); Spin uses its own chosen references and its actual generated carrier.

For each \(G\in \{O,SO,\operatorname {Spin}\}\), define a relation on \(G_f(U)\) by \[x\sim _G y\quad \Longleftrightarrow \quad \exists \gamma \in \Gamma _G\;\exists k\in K_G,\quad y=\gamma xk.\] The finite adelic class sets are the three quotient sets \[\begin {aligned} \mathcal C_O(U)&=\Gamma _O\backslash O_f(U)/K_O,\\ \mathcal C_{SO}(U)&=\Gamma _{SO}\backslash SO_f(U)/K_{SO},\\ \mathcal C_{\operatorname {Spin}}(U)&=\Gamma _{\operatorname {Spin}}\backslash \operatorname {Spin}_f(U)/K_{\operatorname {Spin}}. \end {aligned}\] Here \(\Gamma _G\backslash G_f(U)/K_G\) means the set of equivalence classes for \(\sim _G\), with no quotient topology assigned.

The class of \(x\) is the double coset \(\Gamma _GxK_G\). In coordinates, equality of the classes of \(x\) and \(y\) means \[y_p=h_p x_p k_p\qquad \text {for every prime }p,\] for one rational \(h\in G(V,Q)\) and a tuple \((k_p)_p\in \prod _p U_p^G\). In particular, a tuple supported at one prime \(\ell \), with value \(u\in U_\ell ^G\) there, represents the identity class: it already lies in \(K_G\). The left changes must come from a single rational element; unrelated local left changes do not define this equivalence.

The actual products \(K_G\) are part of these definitions. Eventual equality of reference families identifies the ambient restricted products by Definition 33, but it need not identify their product reference subgroups. The definition therefore does not supply a class-set bijection from eventual equality alone. In dimension zero all three class sets are singletons. These are quotient-set constructions, without a finiteness, measure or approximation assertion.

The finite-stage adelic construction and rational-point diagonal have classical context in [conrad2011adelic, Example 2.3, p. 3, and Theorem 3.6, pp. 6-8]. The quotient relation and its elementary verification above are applied here to the explicit chosen subgroups, rather than attributed to a class-number theorem. TauCeti's corresponding definitions are TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicOrthogonalDoubleCoset, TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalDoubleCoset and TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDoubleCoset. They use the rational diagonal ranges and the subgroups of tuples lying in every reference, without assuming that those ranges are discrete or that the double-coset sets are finite.

Let \(G\) be a group and let \(\Gamma ,K,K'\) be subgroups of \(G\), with \(K\subseteq K'\). Write \([x]_K\) for the double coset \(\Gamma xK\); throughout, \(\Gamma \) is fixed. There is a surjection \[\begin {aligned} p_{K,K'}:\Gamma \backslash G/K&\longrightarrow \Gamma \backslash G/K',\\ [x]_K&\longmapsto [x]_{K'}. \end {aligned}\] Thus allowing more right transformations can identify classes that were previously distinct.

Injectivity fails even for the group \(C_2=\{1,s\}\), where \(s^2=1\) and \(s\ne 1\). Take \(\Gamma =K=\{1\}\) and \(K'=C_2\). The source classes are exactly \(\{1\}\) and \(\{s\}\): with both witnesses equal to \(1\), two representatives are equivalent only when they are equal. The target has the single class \(C_2\), because \(\Gamma xK'=xC_2=C_2\) for each \(x\). Hence precisely two source classes map to one target class. This is a general-group counterexample, without an asserted adelic realization.

For the finite adelic class sets, fix a nondegenerate quadratic form \(Q\) on a finite-dimensional rational space \(V\) and one compatible compact-open reference tuple \(U\). Apply the proposition separately with \[(G,\Gamma ,K)= \bigl (H_f(U),\delta _f^H(H(V,Q)),K_H\bigr ), \qquad H\in \{O,SO,\operatorname {Spin}\}.\] Here the ambient restricted group is from Definition 33, the rational image is from Definition 38, and \(K_H\) is the actual product reference subgroup. Any subgroup \(K'_H\) of that same \(H_f(U)\) containing \(K_H\) gives the stated surjection. An enlargement of reference families does not by itself keep the ambient restricted product fixed; the proposition applies only after the ambient group and the rational diagonal have been identified.

The adelic objects have classical context in [conrad2011adelic, Example 2.3, p. 3, and Theorem 3.6, pp. 6-8]. The quotient map and counterexample above are elementary group arguments, not assertions quoted from that source. TauCeti's DoubleCoset.quotientMapOfLERight_surjective formalizes the general surjectivity statement. Its separate adelic specializations are TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicOrthogonalDoubleCosetMapOfLE_surjective, TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalDoubleCosetMapOfLE_surjective and TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDoubleCosetMapOfLE_surjective. No finiteness of these quotient sets is needed.

Let \(G\) be a group, let \(\Gamma ,K\leq G\), and fix \(a\in G\). Write \([x]_K\) for the double coset \(\Gamma xK\). Right translation induces a bijection \[\begin {aligned} T_a:\Gamma \backslash G/K&\longrightarrow \Gamma \backslash G/(a^{-1}Ka),\\ [x]_K&\longmapsto [xa]_{a^{-1}Ka}. \end {aligned}\] Its inverse sends \([z]_{a^{-1}Ka}\) to \([za^{-1}]_K\). The left subgroup stays \(\Gamma \); neither subgroup is assumed normal, and \(G\) need not be commutative.

For the finite adelic class sets, fix a nondegenerate rational quadratic form and a compatible compact-open reference tuple \(U\). For each \(H\in \{O,SO,\operatorname {Spin}\}\), use the same ambient group \(H_f(U)\) of Definition 33, its own rational diagonal subgroup \(\Gamma _H\), and its actual product subgroup \(K_H\). For \(a_H\in H_f(U)\), the bijection is \[\Gamma _H\backslash H_f(U)/K_H \longrightarrow \Gamma _H\backslash H_f(U)/(a_H^{-1}K_Ha_H).\] It changes the right subgroup inside this fixed group, without replacing the chosen O, SO or Spin rational image. It is a bijection of sets; no quotient topology, approximation or class-number assertion is involved.

The restricted groups and rational diagonals have adelic context in [conrad2011adelic, Example 2.3, p. 3, and Theorem 3.6, pp. 6-8]. The conjugation calculation and inverse above are direct group arguments, not statements attributed to that passage. TauCeti's DoubleCoset.quotientConjRight is the general equivalence with this orientation. The three adelic specializations are TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicOrthogonalDoubleCosetConj, TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalDoubleCosetConj and TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDoubleCosetConj. In their targets, the inverse conjugation automorphism sends \(k\) to \(a_H^{-1}ka_H\), as in the displayed proof.

Let \(G,G'\) be groups, let \(\Gamma ,K\leq G\) and \(\Gamma ',K'\leq G'\), and let \(e:G\to G'\) be a group isomorphism satisfying \(e(\Gamma )=\Gamma '\) and \(e(K)=K'\). Then the double cosets are related by a bijection \[\begin {aligned} \overline e:\Gamma \backslash G/K&\longrightarrow \Gamma '\backslash G'/K',\\ [x]&\longmapsto [e(x)]. \end {aligned}\] Its inverse sends \([y]\) to \([e^{-1}(y)]\). Both subgroup equalities concern their images in the specified ambient groups.

For the finite adelic class sets, let \(Q,Q'\) be nondegenerate forms on finite-dimensional rational spaces \(V,V'\), with compatible compact-open reference tuples \(U,U'\). Fix one \(H\in \{O,SO,\operatorname {Spin}\}\) and suppose that group isomorphisms \[\phi _p:H(Q_p)\longrightarrow H(Q'_p)\] satisfy \(\phi _p(U_p^H)=U_p^{\prime H}\) at every prime. They induce a group isomorphism \[e_H:H_f(U)\longrightarrow H_f(U'),\qquad (x_p)_p\longmapsto (\phi _p(x_p))_p.\] Indeed, membership in a reference subgroup is equivalent at each coordinate, so a tuple and its image have the same finite exceptional set. The coordinatewise inverse is defined for the same reason; multiplication and the inverse identities hold at every coordinate.

Write \(\Gamma _H(U)=\delta _f^H(H(V,Q))\) and \(\Gamma _H(U')=\delta _f^{\prime H}(H(V',Q'))\) for the actual rational diagonal images. Assume additionally \[e_H(\Gamma _H(U))=\Gamma _H(U').\] Everywhere reference preservation gives \(e_H(\prod _pU_p^H)=\prod _pU_p^{\prime H}\): inclusion follows coordinatewise, and the coordinatewise inverse proves the reverse inclusion. The proposition therefore gives \(\mathcal C_H(U)\simeq \mathcal C_H(U')\), with representatives sent by \((x_p)_p\mapsto (\phi _p(x_p))_p\). The rational-image condition is a separate hypothesis; local group isomorphisms alone do not assert it. For SO use the derived reference subgroups \(i_p^{-1}(U_p^O)\) and \((i'_p)^{-1}(U_p^{\prime O})\); for Spin use its own references and actual generated carrier. The argument applies separately to all three groups, without identifying their rational images.

The adelic objects have classical context in [conrad2011adelic, Example 2.3, p. 3, and Theorem 3.6, pp. 6-8]. The transport and inverse above are direct group arguments, not claims quoted from that passage. TauCeti's DoubleCoset.quotientCongr formalizes the general equivalence. Its three corresponding specializations are TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicOrthogonalDoubleCosetCongr, TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpecialOrthogonalDoubleCosetCongr and TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinDoubleCosetCongr. These are equivalences of sets; no continuity of the local isomorphisms or quotient topology is assumed.

Let \(G_p\) be groups indexed by rational primes, with subgroups \(U_p,U'_p\leq G_p\) equal outside a finite set \(F\). Write \(G_f(U)\) and \(G_f(U')\) for their restricted products, regarded here as groups of tuples, and \(K(U)=\prod _pU_p\), \(K(U')=\prod _pU'_p\) for their product reference subgroups. The coordinate identity gives a group isomorphism \(e:G_f(U)\to G_f(U')\), but \[e(K(U))=K(U')\quad \Longleftrightarrow \quad U_p=U'_p\ \text {for every prime }p.\]

In particular, finite changes need not preserve even the number of double cosets. Take \(G_p=C_2=\{1,s\}\) at every prime, with \(s^2=1\ne s\), and take \(U_p=C_2\) for every \(p\). Change only \(U'_2=\{1\}\), keeping \(U'_p=C_2\) for \(p\ne 2\). Both restricted products are \(\prod _pC_2\): the changed condition can fail only at \(2\). With left subgroup \(\Gamma =\{1\}\), the quotient by \(K(U)=\prod _pC_2\) has one class. The quotient by \(K(U')\) has exactly two classes, distinguished by the \(2\)-coordinate. Indeed, right multiplication by \(K(U')\) preserves that coordinate; if \(x_2=y_2\), then \(x^{-1}y\in K(U')\) and \(y=x(x^{-1}y)\). Both coordinates \(1,s\) occur. This is a group-family example, without an asserted realization by adelic O, SO or Spin groups.

For two compatible tuples \(U,U'\) for the same rational quadratic form, fix \(H\in \{O,SO,\operatorname {Spin}\}\) and suppose their \(H\)-references agree outside a finite set. The coordinate identity \(e_H\) identifies the ambient groups \(H_f(U)\) and \(H_f(U')\) and carries their actual rational diagonal images onto each other: both scalar extensions of any rational \(h\) have the same coordinate \(h_p\) at every prime. Thus Proposition 46 gives \[\Gamma _H(U)\backslash H_f(U)/K_H(U) \simeq \Gamma _H(U')\backslash H_f(U')/e_H(K_H(U)).\] The right subgroup displayed in the target is the transported product, which equals \(K_H(U')\) exactly when all the \(H\)-references agree. Eventual equality alone does not supply the hypotheses for transport to \(\mathcal C_H(U')\) with its chosen right subgroup. This does not assert that different right subgroups always give nonisomorphic class sets. The O, derived SO and generated Spin cases each retain their own subgroups.

Finite-stage adelic constructions provide the background in [conrad2011adelic, Theorem 3.6, pp. 6-8]; the product-subgroup criterion and counterexample above are direct deductions. TauCeti's TauCeti.map_integralSubgroup_restrictedProductCongr_eq_iff formalizes the criterion, and TauCeti.doubleCosetCongr transports double cosets to the image subgroups. Neither statement replaces that image with a different product subgroup.

The extensions in Theorem 18 and Theorem 20 are exact sequences of abstract groups. They record a surjective homomorphism and its two-element kernel, but no topology. For the positive real form, the actual finite-dimensional carrier topology, compact double cover, and connectedness are established in Proposition 49; the stabilizer argument and the universal-cover boundary are established in Proposition 50. Those results do not extend the compact connectedness conclusion to arbitrary real signature.

For \(n\geq 0\), let \[Q_n^+(x)=\sum _{i=1}^n x_i^2\] on \(\mathbb R^n\), and give its actual vector-generated group \(\operatorname {Spin}(Q_n^+)\) the subspace topology from the finite-dimensional real Clifford algebra. This group is compact for every \(n\); it is path-connected for \(n\geq 2\). For \(n\geq 1\), the vector action is a two-sheeted covering \[\operatorname {Spin}(Q_n^+)\longrightarrow SO(n)\] with kernel \(\{1,-1\}\).

Here is the compactness mechanism. Cartan--Dieudonne writes every special orthogonal transformation as a bounded even word of reflections. Positive definiteness normalizes every reflecting vector to the unit sphere. An additional unit-vector pair corrects the possible scalar \(-1\), and pairs \((e,e)\) pad the lift to a fixed length. Clifford multiplication therefore gives a continuous surjection \[\bigl (S^{n-1}\times S^{n-1}\bigr )^{n+1} \longrightarrow \operatorname {Spin}(Q_n^+)\qquad (n\geq 1).\] For \(n=0\), the actual vector-generated carrier is the singleton group, hence compact. For \(n\geq 1\), the displayed source is compact, proving compactness. For \(n\geq 2\) it is also path-connected, proving path-connectedness of the target. The plane curve in Example [fcap-0038] independently joins \(1\) to \(-1\).

The vector action is a continuous surjection onto the Hausdorff group \(SO(n)\). Compactness makes it a quotient map. Its two-element kernel is discrete and acts freely, so the quotient-covering theorem makes the action a two-sheeted covering. The finite kernel alone would not prove either the quotient-map or covering assertion.

[gallier2014clifford, Section 1.8, pp. 38--40] gives the compact double cover for \(n\geq 1\) and path-connectedness for \(n\geq 2\), using generators with negative square in \(\operatorname {Cl}_{0,n}\). [lawson2016spin, I.2 and I.4, pp. 14, 19, 25] use the same compact sign through \(v^2=-q(v)\).

To compare their carrier with the positive-square model above, let \(e_i^2=1\) and \(f_i^2=-1\). The complex map \(e_i\mapsto i f_i\) restricts on real even PBW words to \[F(e_{i_1}\cdots e_{i_{2k}}) =(-1)^k f_{i_1}\cdots f_{i_{2k}}.\] The same formula is its inverse. It is a real linear homeomorphism, preserves multiplication and reversal, and carries an even product of real vectors to the corresponding even product up to a scalar \(-1\). That scalar belongs to both actual carriers, since \(e(-e)=-1\) and \(ff=-1\). Thus \(F\) and its inverse identify the actual Spin carriers. Complexifying the vector action and cancelling the common factor \(i\) shows that they also intertwine the actions on \(\mathbb R^n\). Gallier defines Spin through a normalizer condition; the carrier-completion argument in Proposition [fcap-0037], applied after this sign transfer, identifies that normalizer-defined group with the selected vector-generated carrier. This translates the source convention without identifying the two full real Clifford algebras.

TauCeti proves compactness for every \(n\), path-connectedness in dimensions \(n+2\), and the quotient-covering and covering statements for nonzero dimension: CliffordAlgebra.instCompactSpaceRealCliffordSpinGroupZero, CliffordAlgebra.pathConnectedSpace_realCliffordSpinGroupZero_add_two, CliffordAlgebra.isQuotientCoveringMap_realCliffordSpinDoubleCoverZero_rightHom, and CliffordAlgebra.isCoveringMap_realCliffordSpinDoubleCoverZero_rightHom. These exact results concern the positive form and the finite-dimensional carrier topology; they do not assert simple connectedness.

For \(n\geq 3\), the covering in Proposition 49 is the universal covering of \(SO(n)\). The proof uses the action on the unit sphere from Theorem 16, together with the topology just supplied.

Fix a unit vector \(e\). Its stabilizer in \(\operatorname {Spin}(Q_n^+)\) is the preimage of \(SO(e^\perp )\). The Clifford map for the orthogonal inclusion \(e^\perp \hookrightarrow \mathbb R^n\) embeds \(\operatorname {Spin}(Q_{n-1}^+)\) into that preimage, maps onto \(SO(e^\perp )\), and has the same kernel \(\{1,-1\}\). Hence the embedded subgroup is exactly the stabilizer. It is closed. Using the concrete Lie group structure of Proposition [fcap-0037], the closed-subgroup bundle theorem gives \[\operatorname {Spin}(n-1)\longrightarrow \operatorname {Spin}(n)\longrightarrow S^{n-1}.\] This supplies the stabilizer step rather than inferring a fibration from transitivity alone.

One can see the local section directly in the positive-square convention. For a unit vector \(x\ne -e\), put \[u(x)=\frac {e+x}{\sqrt {Q_n^+(e+x)}},\qquad s(x)=\iota (u(x))\iota (e).\] Positive definiteness makes the denominator nonzero, and both vectors have square one. Thus \(s(x)\) is even with reverse norm one. If \(h=\iota (e+x)\), the Clifford relation gives \[h\iota (e)h=\bigl (2+B_Q(e,x)\bigr )\iota (x) =Q_n^+(e+x)\iota (x),\] so \(s(x)\iota (e)s(x)^{-1}=\iota (x)\). The formula is continuous on \(S^{n-1}\setminus \{-e\}\). In TauCeti \(e\) is the last coordinate vector: TauCeti.realCliffordSpinLastLocalSection_apply records the formula, TauCeti.continuousOn_realCliffordSpinLastLocalSection its continuity on that punctured sphere, and TauCeti.realCliffordSpinLastLocalSection_action its orbit identity. The definition assigns the identity at \(-e\); this totalization is not a continuous section on the whole sphere.

With \(k=n-1\geq 1\), CliffordAlgebra.realCliffordSpinContinuousMulEquivLastStabilizer identifies \(\operatorname {Spin}(k)\) with the entire last-vector stabilizer in \(\operatorname {Spin}(k+1)\), continuously and multiplicatively. CliffordAlgebra.exists_realCliffordSpinOrbitTrivialization then provides a bundle chart around every sphere point \(y\), with base \(S^k\setminus \{-y\}\) and fiber \(\operatorname {Spin}(k)\); the resulting fiber-bundle statement is CliffordAlgebra.isFiberBundle_realCliffordSpinOrbitMap. These are charts for the actual orbit map, with the same rank shift as the displayed bundle.

For \(n=3\), Example [fcap-002H] gives the coordinate isomorphism with unit quaternions. Its displayed linear map and inverse restrict continuously to the unit three-sphere, so \(\operatorname {Spin}(3)\) is simply connected. For \(n\geq 4\), the homotopy exact sequence of the bundle and simple connectedness of \(S^{n-1}\) give a surjection \[\pi _1\operatorname {Spin}(n-1)\longrightarrow \pi _1\operatorname {Spin}(n).\] Induction therefore gives \(\pi _1\operatorname {Spin}(n)=0\) for every \(n\geq 3\). Together with path-connectedness and the two-sheeted covering, this makes \(\operatorname {Spin}(n)\to SO(n)\) the universal cover.

The formal base case uses TauCeti.realSpinThreeContinuousMulEquivQuaternionUnitary, the continuous multiplicative quaternion equivalence corresponding to Example [fcap-002H]. The full conclusion CliffordAlgebra.simplyConnectedSpace_realCliffordSpinGroupZero establishes simple connectedness for every \(n\geq 3\). Its induction uses the two antipodal bundle charts: their bases are contractible punctured spheres, their fibers are simply connected by induction, and their overlap is path-connected. Van Kampen then gives simple connectedness of the total space. This implements the same geometric induction through charts rather than the homotopy exact sequence used above. The quaternion case starts the induction; \(\operatorname {Spin}(2)\) is not a simply connected base case. Combining this conclusion with Proposition 49 yields the universal-cover assertion.

[gallier2014clifford, Section 1.8, pp. 40--42] gives this sphere--stabilizer induction. [meinrenken2013clifford, Section 1.6, Lemma 1.4, p. 13] independently checks the base topology using the parallel sphere fibration for \(SO(n)\). The explicit carrier/stabilizer comparison above is the convention bridge to the selected positive-square model.

The lower ranks remain separate: \[\begin {array}{c|c|c} n&\operatorname {Spin}(n)&\text {cover behavior}\\ \hline 0&\{1\}&\text {separate trivial carrier}\\ 1&\{1,-1\}&\text {two sheets over }SO(1),\ \text {not universal}\\ 2&S^1&\text {twofold circle cover of }SO(2),\ \pi _1\ne 0. \end {array}\] The rank-two identification follows from \(a+b e_1e_2\) with \(a=\cos \phi \) and \(b=\sin \phi \). In the orientation of Example [fcap-0038], its vector action has angle \(-2\phi \); hence the map is a twofold circle cover. The formal simple-connectedness theorem therefore has exactly the lower bound needed here; the universal-cover claim combines it with the separately established covering.