Proposition. Adelic component maps and sign kernels [fcap-004J]
✍️source

    Definition [spin-000N]

    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 [fcap-004C]. 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 [fcap-004F], Definition [fcap-004G] and Definition [fcap-004H]. 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 [fcap-0045], 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 [fcap-001C], 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 [fcap-004C] to the single rational Spin element \(-1\), which exists by Lemma [fcap-001C]. Scalar extension carries it to the local scalar \(-1\): the Clifford algebra map preserves \(1\) and negation, as in Theorem [fcap-003N]. 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 [fcap-0023]: 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 [fcap-001C]. 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.

      References

        Reference. Clifford Algebras, Clifford Groups, and a Generalization of the Quaternions: The Pin and Spin Groups [gallier2014clifford]

        • 2014
        • Jean Gallier
        @article{gallier2014clifford,
 title = {Clifford Algebras, Clifford Groups, and a Generalization of the Quaternions: The Pin and Spin Groups},
 author = {Gallier, Jean},
 year = {2014},
 journal = {arXiv preprint arXiv:0805.0311}
}

        Reference. Weil and Grothendieck Approaches to Adelic Points [conrad2011adelic]

        @misc{conrad2011adelic,
 title = {Weil and Grothendieck Approaches to Adelic Points},
 author = {Conrad, Brian},
 year = {2011},
 note = {Author manuscript dated December 31, 2011},
 url = {https://math.stanford.edu/~conrad/papers/adelictop.pdf}
}

        Context

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

            How does reflection generation lead to the Pin and Spin groups? Starting with the Clifford algebra and its norm, we first lift orthogonal transformations and use determinant parity to select the even carrier, while the spinor norm measures the obstruction to normalization over a general field. Field extension and explicit transvections then give concrete lifts and examples of the obstruction.

            Over local fields, finite-dimensional coordinates give the carriers their topologies and let us study the Spin projection and its image. For rational transformations, compatible compact-open reference subgroups provide the prerequisites for passing from these local groups to the restricted product and its away and full adelic variants.

            The rational diagonal and the finite adelic spinor norm connect the rational and local pictures. We then form the finite adelic class sets and compare them under Proposition [fcap-004Q] enlargement and Proposition [fcap-004R] conjugation of the right subgroup, and under Proposition [fcap-004S] isomorphisms preserving both subgroups. Proposition [fcap-004T] distinguishes finite changes of references from equality of their product subgroups. The final leaves return to the real Spin covers.

            Lemma. Fixed-subspace correction by reflections [cartan1981theory, Section 10, pp. 10--12] [fcap-000V]

              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.

              Proof. 

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

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

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

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

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

                    Proof. 

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

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

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

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

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

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

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

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

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

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

                            Proof. 

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

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

                                Let \(K\) be a field of characteristic different from \(2\), let \(V\) be finite-dimensional, and let \(Q\) be nondegenerate. Suppose that for every nonisotropic \(v\in V\), the scalar \(-Q(v)^{-1}\) is a square in \(K\). Then the twisted-adjoint action restricts to a surjection \[\operatorname {Spin}(V,Q)\twoheadrightarrow SO(V,Q).\] The underlying homomorphism is 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 [fcap-000X]. It lifts an element of \(SO(V,Q)\) to Pin; the lift has determinant \(1\), so Lemma [fcap-001A] shows that it is even and therefore lies in Spin. The restriction square

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

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

                                Proposition. The reverse norm descends through the Lipschitz action [fcap-002D]

                                  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:

                                  The determinant arrow is a separate branch: \(SO(V,Q)=\ker (\det )\). It is not part of a longer exact row after \(O(V,Q)\). Positive dimension supplies an anisotropic vector, so scalar units form the displayed kernel; the Lipschitz action is onto CliffordAlgebra.scalarUnits_injective CliffordAlgebra.ker_lipschitzToOrthogonal CliffordAlgebra.lipschitzToOrthogonal_surjective. The right vertical map is the orthogonal spinor norm, while \(\nu _Q=\nu _Q^O|_{SO(V,Q)}\) is its restriction used in Theorem [fcap-0023]. The square expresses descent through the action, not surjectivity of \(\nu _Q^O\) CliffordAlgebra.orthogonalSpinorNorm_lipschitzToOrthogonal.

                                  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 [fcap-0029].

                                  Theorem. The Spin image is the spinor-norm kernel [fcap-0023]
                                  range_spinToSpecialOrthogonal_eq_ker_spinorNorm
                                  L∃∀N

                                    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.

                                    Proof. 

                                      Every Spin element has reverse norm one, so its image has trivial spinor norm CliffordAlgebra.spinorNorm_spinToSpecialOrthogonal. Conversely, suppose first that \(V\) has positive dimension. Take \(g\in SO(V,Q)\) with \(\nu _Q(g)=1\), and choose a Lipschitz lift \(x\) of \(g\). Since \(\det (g)=1\), determinant parity first shows that \(x\) is even CliffordAlgebra.mem_even_of_det_lipschitzToOrthogonal_eq_one Lemma [fcap-001A]. Trivial spinor class says that \(N_{\mathrm {rev}}(x)\) is a square. Scalar normalization therefore produces an even lift with reverse norm one source theorem; by the even-element comparison in Remark [fcap-0028], it lies in Spin and has the same orthogonal action. In dimension zero \(SO(V,Q)\) is trivial, so the image and the spinor-norm kernel are both its identity subgroup.

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

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

                                        Proof. 

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

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

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

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

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

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

                                            Proof. 

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

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

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

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

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

                                                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 [fcap-0023] CliffordAlgebra.spinorNorm_transvection.

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

                                                Example. A null-frame Spin transvection and a radical shear [fcap-002N]

                                                  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 [fcap-0023].

                                                  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.

                                                  Example. A mixed-sign isometry has no norm-one Spin lift [fcap-002E]

                                                    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 [fcap-002D], so no lift can be normalized into the norm-one Spin carrier. Equivalently, the image theorem in Theorem [fcap-0023] 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.

                                                    Remark. Real spinor-norm images and the low-rank boundary [fcap-002F]

                                                      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 [fcap-0023]; 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.

                                                      Theorem. Spin acts transitively on a positive quadratic sphere [fcap-0024]
                                                      exists_spinVectorAction_eq_of_posDef
                                                      L∃∀N

                                                        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.

                                                        Proof. 

                                                          Write \(B_Q\) for the polar form. For \(a\ne 0\), reflection in the hyperplane perpendicular to \(a\) is \[r_a(v)=v-\frac {B_Q(a,v)}{Q(a)}a.\] If \(x+y\ne 0\), then positive definiteness makes \(x+y\) anisotropic, and \[Q(x+y)=2c+B_Q(x,y)=B_Q(x+y,x).\] Hence \(r_{x+y}(x)=-y\) and \(r_y r_{x+y}(x)=y\). If \(y=-x\), choose a nonzero \(z\) with \(B_Q(z,x)=0\), possible because \(\dim V\geq 2\). Then \(r_z(x)=x\) and \(r_x r_z(x)=y\). Both maps are products of two reflections, so they lie in \(SO(Q)\). The positive-definite surjectivity CliffordAlgebra.spinToSpecialOrthogonal_surjective_of_posDef lifts the chosen map to Spin, whose vector action is the same map.

                                                          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 [fcap-001B].

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

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

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

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

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

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

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

                                                                  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.

                                                                  Proposition. Isometries transport the Spin vector action [fcap-0029]
                                                                  spinGroupMap_spinVectorAction
                                                                  L∃∀N

                                                                    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.

                                                                    Definition. The canonical topology on local points [fcap-0044]

                                                                      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.

                                                                      Lemma. Closed local carriers and continuous Clifford actions [fcap-0045]

                                                                        Definition [spin-000O]

                                                                        Let \(K\) be a local field of characteristic different from two in the sense of Definition [fcap-0044], 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 [fcap-002D], 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 [fcap-0044]; 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 [fcap-001A] 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.

                                                                        Proposition. The open Clifford quotient and locally constant spinor norms [fcap-0046]

                                                                          Let \(K\), \(V\), \(Q\) and their topologies be as in Lemma [fcap-0045]. 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 [fcap-002D], \[\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.

                                                                          Proof. 

                                                                            First suppose \(\dim _K V>0\). Local fields are locally compact and \(\sigma \)-compact, meaning a countable union of compact subsets. For a nonarchimedean local field, its valuation ring is compact: completeness and the finite residue quotients make it a complete totally bounded metric space. Its scalar dilates exhaust \(K\); ordinary closed balls give the analogous exhaustion for \(\mathbb R\) and \(\mathbb C\). Finite products give compact exhaustions of \(A=\mathcal {C}\kern -2pt\ell (Q)\) and \(A^2\).

                                                                            By Definition [fcap-0044], the units identify homeomorphically with the closed inverse graph \(\{(x,y):xy=yx=1\}\subseteq A^2\). Hence \(A^\times \) is locally compact and \(\sigma \)-compact. The closedness of \(\Gamma (Q)\) in Lemma [fcap-0045] gives the same properties to \(\Gamma (Q)\). Its vector action is continuous there and onto by Proposition [fcap-002D]; the target \(O(Q)\) is locally compact Hausdorff.

                                                                            Here is the open-map argument. Given an open identity neighborhood \(U\subseteq \Gamma (Q)\), choose an open identity neighborhood \(W\) with compact closure and \(\overline W\,\overline W^{-1}\subseteq U\). Such \(W\) exists by continuity of multiplication and inversion and local compactness. A compact exhaustion and finite subcovers of its terms give a countable cover \(\Gamma (Q)=\bigcup _j g_jW\). Thus \[O(Q)=\bigcup _j\tau (g_j)\tau (\overline W).\] Each set in this union is closed, because \(\tau (\overline W)\) is compact and the target is Hausdorff. The Baire theorem for locally compact Hausdorff spaces implies that \(\tau (\overline W)\) has nonempty interior. If \(D\) is a nonempty open subset of this image and \(d\in D\), then \(Dd^{-1}\) is an open identity neighborhood contained in \[\tau (\overline W)\tau (\overline W)^{-1}\subseteq \tau (U).\] Translating this conclusion around every point of any open subset of \(\Gamma (Q)\) proves that \(\tau \) is open. A continuous open surjection is a quotient map: a subset of the target whose inverse image is open is the open image of that inverse image. This is the argument underlying Mathlib's MonoidHom.isOpenMap_of_sigmaCompact.

                                                                            The reverse norm \(N_{\mathrm {rev}}:\Gamma (Q)\to K^\times \) is continuous. Indeed, Proposition [fcap-002D] identifies \(\operatorname {rev}(x)x\) with the scalar \(N_{\mathrm {rev}}(x)\); extracting its scalar coefficient is a linear map on \(A\). Its values are nonzero, and \(K^\times \) has the subspace topology from \(K\) by Definition [fcap-0044].

                                                                            The square subgroup is open in \(K^\times \). Over \(\mathbb R\) it is the positive half-line, and over \(\mathbb C\) it is all of \(K^\times \). For a complete discretely valued field of characteristic different from two, let \(\mathcal O_K\) be its valuation ring and \(\mathfrak m_K\) its maximal ideal. The local square theorem gives \[1+4\mathfrak m_K\subseteq (K^\times )^2.\] This is [lam2005quadratic, VI.2, Theorem 2.19 and Corollary 2.20, p. 161]; its complete discrete valuation hypotheses apply also in residue characteristic two. Since \(4\ne 0\), multiplication by \(4\) is a homeomorphism, so the left side is an open identity neighborhood. Translating it by squares proves that the subgroup is open. Every square coset is therefore open, which makes its quotient \(\mathcal S_K\) discrete.

                                                                            Let \(q:K^\times \to \mathcal S_K\) be the quotient map. The norm identity in Proposition [fcap-002D] is \[\nu _Q^O\circ \tau =q\circ N_{\mathrm {rev}}.\] The right side is continuous. The established quotient property of \(\tau \) therefore proves continuity of \(\nu _Q^O\); restricting to the subgroup \(SO(Q)\) proves continuity of \(\nu _Q\). A continuous map to a discrete space is locally constant. More explicitly, \[\ker \nu _Q^O=\tau \bigl (N_{\mathrm {rev}}^{-1}((K^\times )^2)\bigr )\] is open, since both the preimage and \(\tau \) are open. Its intersection with \(SO(Q)\) is \(\ker \nu _Q\), identified with the Spin image by Theorem [fcap-0023]. In dimension zero all domain groups are trivial by Lemma [fcap-0045]; the same square-class topology and conclusions apply.

                                                                            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.

                                                                            Theorem. Proper Spin projections and anisotropic compactness [fcap-0047]

                                                                              Let \(K\) be a local field of characteristic different from two as in Definition [fcap-0044], and let \(Q\) be a nondegenerate quadratic form on a finite-dimensional \(K\)-space \(V\). Use the canonical topologies of Definition [fcap-0044]. 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 [fcap-0045] and Proposition [fcap-0046], using the scalar-kernel and reverse-norm identities of Proposition [fcap-002D]. Thus compactness depends on the quadratic form, even when the projection has finite kernel.

                                                                              Proof. 

                                                                                If \(V=0\), the generated Spin carrier and both orthogonal groups are singletons by Lemma [fcap-0045]; all assertions follow. Suppose henceforth that \(\dim _K V>0\), and let \(C\subseteq O(Q)\) be compact. Write \(\tau :\Gamma (Q)\to O(Q)\) for the open surjection in Proposition [fcap-0046]. Choose a lift of each point of \(C\), and an open neighborhood of that lift with compact closure in the locally compact group \(\Gamma (Q)\). Their open images cover \(C\). A finite subcover therefore supplies a compact set \(L\subseteq \Gamma (Q)\) such that \(C\subseteq \tau (L)\). If \(C\) is empty, its preimage is already compact.

                                                                                Let \(x\in \operatorname {Spin}(Q)\) have action in \(C\). Choose \(y\in L\) with \(\tau (y)=\rho (x)\), viewing \(SO(Q)\) inside \(O(Q)\). The scalar-kernel identity gives \(x=cy\) for some \(c\in K^\times \). The star-unitary Spin convention has reverse norm one on even elements by Remark [fcap-0028]. Hence the scalar-scaling identity of Proposition [fcap-002D] gives \[\begin {gathered} 1=c^2N_{\mathrm {rev}}(y),\\ c^2=N_{\mathrm {rev}}(y)^{-1}. \end {gathered}\] The inverse norm is continuous on \(L\) by Proposition [fcap-0046]. Its absolute value is bounded there, say by \(M\geq 1\), so \(|c|\leq \sqrt M\). Closed bounded scalar balls are compact over a local field: in the nonarchimedean case they are closed subsets of a scalar dilate of the compact valuation ring, and in the archimedean cases this is the usual closed-ball compactness. Write \(D=\{a\in K:|a|\leq \sqrt M\}\). Then the set \[DL=\{ay:a\in D,\ y\in L\}\] is compact in \(\mathcal {C}\kern -2pt\ell (Q)\), as a continuous image of a product of compact sets. The preimage of \(C\) in Spin is closed in the Clifford algebra: Spin is closed by Lemma [fcap-0045], \(C\) is closed in the Hausdorff group \(O(Q)\), and the projection is continuous. It is contained in the displayed compact set, so it is compact. A compact subset of \(SO(Q)\) is also compact in \(O(Q)\), proving properness of \(\rho \).

                                                                                Suppose now that \(Q\) is anisotropic. Choose coordinates and put \(\|v\|=\max _i|v_i|\). The unit sphere \(\|v\|=1\) is a compact subset of the coordinate unit ball. On it the continuous function \(|Q|\) is positive, so has a positive minimum \(m\). For \(v\ne 0\), choose a coordinate \(a=v_j\) of maximal absolute value. Then \(\|a^{-1}v\|=1\), giving \[\begin {aligned} |Q(v)|&=|a|^2|Q(a^{-1}v)|\\ &\geq m\|v\|^2. \end {aligned}\] This also holds at zero. If \(g\in O(Q)\), its \(i\)-th column satisfies \(Q(ge_i)=Q(e_i)\), so the inequality bounds every column, uniformly in \(g\). The closed matrix carrier \(O(Q)\) from Lemma [fcap-0045] is consequently a closed subset of a compact finite product of scalar balls. Thus \(O(Q)\) is compact. Its inverse image is all of Spin, which is compact by the properness just proved.

                                                                                Conversely, suppose \(Q\) is isotropic. Take \(u\ne 0\) with \(Q(u)=0\). Write \(B_Q\) for the unhalved polar form of Convention [fcap-0027]. Nondegeneracy supplies \(w\) with \(B_Q(u,w)=1\); set \(v=w-Q(w)u\). Then \(Q(v)=0\) and \(B_Q(u,v)=1\). Such \(u,v\) form a hyperbolic pair: their plane \(H=Ku+Kv\) has \(Q(au+bv)=ab\), and is nondegenerate, so \(V=H\perp H^\perp \). This is the hyperbolic plane of [lam2005quadratic, I.3, Theorems 3.2 and 3.4, pp. 9--10]; Lam's symmetric bilinear form is our half-polar form \(b_Q=B_Q/2\). It specializes to the real model in Definition [fcap-0012].

                                                                                For \(t\in K^\times \), define \(h_t\) by \[\begin {gathered} h_tu=tu,\quad h_tv=t^{-1}v,\\ h_t|_{H^\perp }=\operatorname {id}. \end {gathered}\] It preserves \(Q\) and has determinant \(1\). Square classes have exponent two, so \(\nu _Q(h_t^2)=\nu _Q(h_t)^2=1\). The exact image statement Theorem [fcap-0023] therefore gives an actual Spin lift of each \(h_t^2\). Choose \(a\in K^\times \) with \(|a|>1\) and let \(t=a^r\), \(r=1,2,\ldots \). In a basis beginning with \(u,v\), the first diagonal entry of \(h_t^2\) is \(a^{2r}\), an unbounded scalar sequence. If Spin were compact, its continuous matrix image and every matrix coordinate would be compact, hence bounded. This contradiction proves noncompactness, including when \(H=V\) is a split binary plane.

                                                                                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.

                                                                                Example. Compact and split binary Spin groups over the 3-adic field [fcap-0048]

                                                                                  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 [fcap-0047]. The local-field convention is Definition [fcap-0044]; 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 [fcap-0047]. 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.

                                                                                  Proposition. Binary local spinor norms and the Spin index [fcap-0049]

                                                                                    Let \(K\) be a nonarchimedean local field of characteristic different from two, as in Definition [fcap-0044], and let \(Q\) be a nondegenerate form on a finite-dimensional \(K\)-space. Use the reverse-norm convention of Proposition [fcap-002D]: \(\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 [fcap-0023] 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 [fcap-0048], 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.

                                                                                    Proof. 

                                                                                      For the anisotropic binary form, the nonzero represented values are exactly \(aN\), because \(Q(x,y)=a(x^2-dy^2)\). Every isometry is a product of reflections by Theorem [fcap-000W], and determinant parity counts the factors by Lemma [fcap-001A]. Its spinor norm is the square class of the product of their quadratic values Proposition [fcap-002D]. Even products therefore have class in \(H\). Conversely, choose vectors with values \(a\) and \(an\) for any \(n\in N\). Their reflection product has class \([a^2n]=[n]\), so every class of \(H\) occurs on \(SO(Q)\). Multiplying by the reflection of value \(a\) gives the odd coset \([a]H\), proving the formula on \(O(Q)\). For a split binary form, the hyperbolic coordinate form \(xy\) represents every nonzero scalar; reflections of values \(1\) and \(c\) give any prescribed class \([c]\).

                                                                                      To obtain the index of \(N\), use the local Hilbert symbol \((u,v)_K\): it is \(1\) when the quaternion algebra \((u,v\mid K)\) is a matrix algebra, and \(-1\) otherwise. This is a symmetric bilinear pairing on \(S\), nondegenerate by [lam2005quadratic, VI.2, discussion on p. 159 and Theorem 2.16, p. 160]. The quaternion norm criterion [lam2005quadratic, III.2, Theorem 2.7(1), (8) and proof, pp. 58--59] says that \((n,d)_K=1\) exactly when \(n\in N\). Since \([d]\ne 1\), nondegeneracy makes \([n]\mapsto (n,d)_K\) onto \(\{1,-1\}\). Its kernel is \(H\), so \([S:H]=2\). The formula for \(I_Q\) follows from Theorem [fcap-0023]. For \(Q_+\), the first coefficient is \(1\in N\), so the two norm images coincide, as claimed.

                                                                                      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.

                                                                                      Proposition. Higher-rank local spinor norms and square-class counts [fcap-004A]

                                                                                        Let \(K\) be a nonarchimedean local field of characteristic different from two, as in Definition [fcap-0044]. 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 [fcap-0049]. 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].

                                                                                        Proof. 

                                                                                          Fix \(c\in K^\times \). If \(Q\) is isotropic, a hyperbolic plane in \(V\) represents every scalar, so choose vectors of values \(1\) and \(c\); their reflection product has spinor norm \([c]\) by Proposition [fcap-002D]. To see the hyperbolic plane explicitly, take a nonzero isotropic \(u\). Nondegeneracy supplies \(w\) with \(B_Q(u,w)=1\), in the unhalved convention Convention [fcap-0027]. Then \(v=w-Q(w)u\) satisfies \(Q(v)=0\), \(B_Q(u,v)=1\), and \(Q(xu+yv)=xy\).

                                                                                          If \(Q\) is anisotropic, the nondegenerate form \[\begin {gathered} F(v,w)=Q(v)-cQ(w)\\ \text {on }V\oplus V \end {gathered}\] has dimension at least six. Restricting a diagonalization to five coordinates and applying the cited theorem gives a nonzero \((v,w)\) with \(Q(v)=cQ(w)\). Neither vector can vanish, since anisotropy would then force the other to vanish too. Set \(b=Q(v)\ne 0\); thus \(Q(w)=b/c\ne 0\). The two reflections give \[\begin {gathered} r_vr_w\in SO(Q),\\ \nu _Q(r_vr_w)=[b^2/c]=[c]. \end {gathered}\] The last equality uses \((b^2/c)/c=(b/c)^2\). This proves surjectivity on \(SO(Q)\), hence on \(O(Q)\). Finally, \(\rho (\operatorname {Spin}(Q))=\ker \nu _Q\) by Theorem [fcap-0023], so the first isomorphism theorem gives \(I_Q=|S|\).

                                                                                          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 [fcap-0049] 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\).

                                                                                          Example. A rational Spin obstruction vanishes over the 7-adic field [fcap-004B]

                                                                                            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 [fcap-003N].

                                                                                            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 [fcap-002D]. 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 [fcap-0023] 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 [fcap-003N] becomes

                                                                                            Here \(j([a]_{\mathbb {Q}})=[a]_{\mathbb {Q}_7}\). Its value on \(\nu _q(g)\) is \(j([2]_{\mathbb {Q}})=1\), so \(g_7\) has a Spin lift. The following calculation supplies that lift explicitly.

                                                                                            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 [fcap-003O] 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\).

                                                                                            Definition. Compatible compact-open reference subgroups [fcap-004C]

                                                                                              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 [fcap-0044]. The actions are continuous by Lemma [fcap-0045]. For a rational orthogonal or Spin point \(x\), write \(x_p\) for its scalar extension; the action compatibility is Theorem [fcap-003N].

                                                                                              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 [fcap-0045]: 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 [fcap-004D].

                                                                                              Proposition. A rational basis supplies compatible reference subgroups [fcap-004D]

                                                                                                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 [fcap-004C]. 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.

                                                                                                Proof. 

                                                                                                  Suppose first that \(n>0\). In the basis \(b_p\), the condition \(gL_p=L_p\) means that both the matrix \(A\) of \(g\) and its inverse have entries in \(\mathbb Z_p\). Indeed, integral columns are exactly the condition \(gL_p\subseteq L_p\); the inverse condition gives the reverse inclusion. These conditions are closed under products and inverses, so \(H_p\) is a subgroup.

                                                                                                  The ring \(\mathbb Z_p\) is open in \(\mathbb Q_p\). Every entry of \(A\) and \(A^{-1}\) varies continuously on \(O_p\) by Definition [fcap-0044]. Requiring their finitely many entries to lie in \(\mathbb Z_p\) is therefore an open condition, proving that \(H_p\) is open.

                                                                                                  For compactness, retain both matrix coordinates. Let \(\mathcal C_p\subseteq M_n(\mathbb Z_p)^2\) be defined by \[\begin {gathered} AC=CA=I,\\ Q_p(Ax)=Q_p(x). \end {gathered}\] The second identity is required for every \(x\in V_p\). This is a finite collection of polynomial equations in the entries of \(A\): expand the two quadratic forms in the coordinates of \(x\) and equate their coefficients. The inverse equations are also polynomial. Thus \(\mathcal C_p\) is closed in \(M_n(\mathbb Z_p)^2\). Since \(\mathbb Z_p\) is compact, this finite product and its closed subset \(\mathcal C_p\) are compact. Projection \((A,C)\mapsto A\) identifies \(\mathcal C_p\) homeomorphically with \(H_p\); its inverse is \(A\mapsto (A,A^{-1})\). This is precisely the inverse-graph topology from Definition [fcap-0044]. Consequently \(H_p\) is compact. This matrix argument itself does not require nondegeneracy of the quadratic form.

                                                                                                  The full action preimage \(U_p^{\operatorname {Spin}}\) is a subgroup and is open by continuity of \(i_p\rho _p\). Nondegeneracy persists over \(\mathbb Q_p\): a rational Gram determinant remains nonzero after the field embedding. The derived group \(U_p^{SO}\) is compact by the closed-inclusion argument in Definition [fcap-004C], so \[U_p^{\operatorname {Spin}}=\rho _p^{-1}(U_p^{SO})\] is compact by the properness theorem Theorem [fcap-0047]. This is the step that uses nondegeneracy. The full-preimage definition also gives \(i_p\rho _p(U_p^{\operatorname {Spin}})\subseteq H_p\) directly.

                                                                                                  Fix one \(g\in O(Q)\). Its matrix and inverse matrix in the rational basis \(b\) contain finitely many rational entries. Let \(S_O(g)\) be the union of the prime divisors of their reduced denominators. It is finite. If \(p\notin S_O(g)\), each denominator is a unit of \(\mathbb Z_p\), so all entries of both localized matrices lie in \(\mathbb Z_p\). Hence \(g_p\in H_p\). There is no need to require the coefficients of \(Q\) to be integral in \(b\).

                                                                                                  Now fix \(s\in \operatorname {Spin}(Q)\) and let \(g=i\rho (s)\in O(Q)\) be its rational orthogonal action. Scalar-extension naturality from Theorem [fcap-003N] gives \[i_p\rho _p(s_p)=g_p.\] The preceding argument therefore puts \(s_p\) in \(U_p^{\operatorname {Spin}}\) for every \(p\notin S_O(g)\). Taking \(S_{\operatorname {Spin}}(s)=S_O(i\rho (s))\) proves the remaining rational membership condition. The set is chosen separately for each \(s\); no uniform denominator bound on all rational Spin points is asserted.

                                                                                                  If \(n=0\), the basis and all matrix-coordinate conditions are empty. Both orthogonal groups are trivial, and the actual generated Spin carrier is \(\{1\}\), by Lemma [fcap-0045]. Thus every displayed reference subgroup is the singleton group, compact and open, and all exceptional sets can be empty.

                                                                                                  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 [fcap-0048], 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 [fcap-0047] 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.

                                                                                                  Proposition. Changing compact-open reference subgroups [fcap-004E]

                                                                                                    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 [fcap-004D] 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 [fcap-004C].

                                                                                                    Proof. 

                                                                                                      For bases \(b\) and \(b'\), let \(C\) express the vectors of \(b'\) in the basis \(b\). Let \(F_b\) contain the denominator primes of every entry of both \(C\) and \(C^{-1}\). This is a finite set. Write \(L_p,L'_p\) for the respective \(\mathbb Z_p\)-spans of \(b_p,b'_p\). For \(p\notin F_b\), the entries of \(C\) belong to \(\mathbb Z_p\), so every vector of \(b'_p\) belongs to \(L_p\). Applying \(C^{-1}\) gives the reverse containment. Thus \(L'_p=L_p\). Their stabilizers in \(O_p\) are equal. Taking full preimages under \(i_p\rho _p\) and \(i_p\) gives equality of the Spin and SO references as well. No integrality condition on the coefficients of \(Q\) is needed.

                                                                                                      For shrinking, an open subgroup of a topological group is closed: its complement is the union of its other open cosets. Hence \(U_p^O\cap W_p\) is open and is a closed subset of the compact group \(U_p^O\). The continuous action \(i_p\rho _p\) has an open and closed preimage of \(W_p\). Intersecting this preimage with the compact-open \(U_p^{\operatorname {Spin}}\) likewise gives an open compact subgroup. The action sends the Spin intersection into the orthogonal intersection. The derived SO group has the required properties by Definition [fcap-004C].

                                                                                                      If \(p\notin F\), the orthogonal intersection equals \(U_p^O\). Compatibility of \(U\) gives \(i_p\rho _p(U_p^{\operatorname {Spin}})\subseteq U_p^O\subseteq W_p\), so the Spin intersection also equals \(U_p^{\operatorname {Spin}}\); the derived SO preimages are then equal. For a rational point \(x\), adjoining \(F\) to its original finite exceptional set proves eventual membership in the new references. The union is taken separately for each \(x\), as required. In dimension zero all groups are singletons and these statements retain their literal meanings.

                                                                                                      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 [fcap-004D] 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.

                                                                                                      Definition. Finite restricted products [fcap-004F]

                                                                                                        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 [fcap-004D]. 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.

                                                                                                        Proof. 

                                                                                                          The identity belongs to every reference subgroup. The product of tuples with exceptional sets \(S\) and \(T\) has exceptional set contained in \(S\cup T\); inversion preserves a tuple's exceptional set. Thus the coordinate operations define a group on \(G_f(U)\), which is the union of its principal stages.

                                                                                                          If \(S\subseteq T\), the inclusion \(G_S(U)\to G_T(U)\) replaces only the finitely many factors \(U_p\) for \(p\in T\setminus S\) by \(G_p\). Each inclusion \(U_p\hookrightarrow G_p\) is an open embedding, so the product inclusion is an open embedding. For arbitrary finite \(S,T\), \[G_S(U)\cap G_T(U)=G_{S\cap T}(U).\] This intersection is open in both stages with the same topology. If \(A\) is open in \(G_S(U)\), its intersection with \(G_T(U)\) is therefore open in \(G_T(U)\): first intersect with the open \(G_{S\cap T}(U)\), then use its open inclusion into \(G_T(U)\). Hence \(A\) is open in the union topology. Conversely, an open set of the union restricts to an open set in each stage by definition. This proves both the claimed stage topology and stage openness.

                                                                                                          A coordinate evaluation is continuous on every stage, hence on the union by the definition of its topology. Two distinct tuples differ at some prime; disjoint neighborhoods in that Hausdorff factor pull back to disjoint neighborhoods of the tuples. Thus the union is Hausdorff. Multiplication restricts to a continuous map \[G_S(U)\times G_T(U)\longrightarrow G_{S\cup T}(U)\] by continuity in each factor of the product topology. These open products cover \(G_f(U)\times G_f(U)\), proving continuity of multiplication. Inversion is continuous on each open stage, hence on the union. Finally \(K(U)\) is compact by the product compactness theorem and open as the empty stage. Its translates are compact neighborhoods of every point, proving local compactness.

                                                                                                          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 [fcap-0045]. 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 [fcap-004E] 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.

                                                                                                          Definition. Away restricted products and finite-prime splitting [fcap-004G]

                                                                                                            Use the Hausdorff locally compact groups \(G_p\) and compact open references \(U_p\) of Definition [fcap-004F]. 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 [fcap-004F] 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 [fcap-004F], 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\).

                                                                                                            Proof. 

                                                                                                              The inverse of \(d_R\) reinserts the coordinates indexed by \(R\). If the away tuple has finite exceptional set \(T\), the reconstructed tuple has exceptional set contained in \(R\cup T\). This is finite, so the inverse is well defined. Coordinate restriction and reinsertion are mutually inverse homomorphisms. Continuity of \(d_R\) follows from the continuous coordinate evaluations of Definition [fcap-004F] and the continuous map \(r_R\).

                                                                                                              For the inverse, the open subsets \[\Bigl (\prod _{p\in R}G_p\Bigr )\times G_T^R(U)\] cover the target as \(T\) ranges over the finite subsets of the complement. On each such subset reinsertion is the product rearrangement onto \(G_{R\cup T}(U)\), followed by its continuous inclusion into \(G_f(U)\). Hence the inverse is continuous on an open cover, and therefore continuous everywhere. This argument uses the established open stages and the ordinary product topology.

                                                                                                              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.

                                                                                                              Definition. Full adelic groups and the real factor [fcap-004H]

                                                                                                                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 [fcap-0044]. In particular \(\operatorname {Spin}_\infty \) uses the actual vector-generated, even, reverse-norm-one carrier of Lemma [fcap-0045].

                                                                                                                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 [fcap-004F]. 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 [fcap-0045] gives those properties for the real factor, and Definition [fcap-004F] 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.

                                                                                                                Example. A moving prime separates two topologies [fcap-004I]

                                                                                                                  Use the hyperbolic plane \(Q(x,y)=xy\) and the integral orthogonal references of the example in Definition [fcap-004F]. 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 [fcap-004F] 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.

                                                                                                                  Proposition. Adelic component maps and sign kernels [fcap-004J]
                                                                                                                  ✍️source

                                                                                                                    Definition [spin-000N]

                                                                                                                    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 [fcap-004C]. 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 [fcap-004F], Definition [fcap-004G] and Definition [fcap-004H]. 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 [fcap-0045], 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 [fcap-001C], 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 [fcap-004C] to the single rational Spin element \(-1\), which exists by Lemma [fcap-001C]. Scalar extension carries it to the local scalar \(-1\): the Clifford algebra map preserves \(1\) and negation, as in Theorem [fcap-003N]. 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 [fcap-0023]: 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 [fcap-001C]. 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.

                                                                                                                      Definition. Rational diagonal subgroups [fcap-004K]

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

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

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

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

                                                                                                                        Proof. 

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

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

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

                                                                                                                          Proposition. Full rational diagonals are discrete under lattice containment [fcap-004L]

                                                                                                                            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 [fcap-004D]. 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 [fcap-004D], its rational-basis changes and its finite shrinkings from Proposition [fcap-004E].

                                                                                                                            Proof. 

                                                                                                                              Put \(W_p=U_p^O\cap H_p\). The groups \(W_p\) are open, since both factors are open by Definition [fcap-004C] and Proposition [fcap-004D]. Choose a finite set \(F\) outside which \(U_p^O\subseteq H_p\); then \(W_p=U_p^O\) for \(p\notin F\). Thus \[K_W=\prod _p W_p\subseteq O_f(U)\] is an open identity neighborhood. Indeed, inside the open principal stage \(O_F(U)\) it imposes an open condition on only the finitely many coordinates in \(F\), and leaves the other reference factors unchanged. This uses the stage topology of Definition [fcap-004F].

                                                                                                                              Let \(M_b(g_\infty )\) be the real matrix of \(g_\infty \in O_\infty \) in the extended basis, and put \[A=\left \{g_\infty \in O_\infty : \left |M_b(g_\infty )_{ij}-\delta _{ij}\right |<\tfrac 12 \text { for every }i,j\right \}.\] Here \(\delta _{ij}\) is the Kronecker delta. The finitely many matrix entries are continuous by Definition [fcap-0044], so \(A\) is open and contains the identity. Hence \(A\times K_W\) is an open identity neighborhood in \(O_{\mathbb A}(U)\).

                                                                                                                              Suppose a rational \(g\in O(Q)\) has diagonal in this neighborhood. Every \(g_p\) stabilizes \(L_p\); therefore each entry of its rational matrix \(M_b(g)\) belongs to \(\mathbb Z_p\) at every prime. A reduced fraction \(a/d\), with \(d>0\), has this property only if \(d=1\): a prime divisor \(p\) of \(d\) does not divide \(a\), giving negative \(p\)-adic valuation. Thus all the entries of \(M_b(g)\) are integers. Their real values differ from \(\delta _{ij}\) by less than \(1/2\); an integer with that property must equal \(\delta _{ij}\). Consequently \(g=1\). This isolates the identity in the orthogonal diagonal image. Translation by each diagonal element isolates every point of that image.

                                                                                                                              Pull the neighborhood back under the continuous inclusion \(SO_{\mathbb A}(U)\to O_{\mathbb A}(U)\) from Proposition [fcap-004J]. Naturality from Definition [fcap-004K] shows that its intersection with the rational SO image contains only the identity: the underlying rational orthogonal transformation is already the identity. This proves SO discreteness.

                                                                                                                              Pull this SO neighborhood back along the continuous map \(\rho _{\mathbb A}:\operatorname {Spin}_{\mathbb A}(U)\to SO_{\mathbb A}(U)\). A rational Spin point in this preimage has rational projection \(1\), by naturality and injectivity of the SO diagonal. If \(\dim V>0\), the field version of the scalar-kernel statement in Lemma [fcap-001C] gives precisely \(s=1\) or \(s=-1\). The real Spin group is Hausdorff, and the scalar elements \(1\) and \(-1\) are distinct there. Choose an open real identity neighborhood \(B_\infty \) excluding \(-1\). Intersect the preceding preimage with \(B_\infty \times \operatorname {Spin}_f(U)\). The intersection is open and its rational diagonal points consist of \(1\) alone. Translation proves Spin discreteness.

                                                                                                                              If \(\dim V=0\), the actual vector-generated Spin carrier is \(\{1\}\), as in Lemma [fcap-003H]; both orthogonal carriers are also singleton. The conclusion is immediate. In particular there is no extra scalar \(-1\) in this generated zero-dimensional carrier.

                                                                                                                              For the integral tuple, \(U_p^O=H_p\) at every prime. Finite shrinking only replaces reference subgroups by smaller ones, so it preserves containment. Changing rational basis changes \(H_p\) at only finitely many primes by Proposition [fcap-004E]. Adjoin these primes to the exceptional set to retain the hypothesis.

                                                                                                                              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 [fcap-001C] 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.

                                                                                                                              Proposition. Isotropic rational SO diagonals accumulate in the finite adeles [fcap-004M]
                                                                                                                              not_discreteTopology_range_finiteAdelicSpecialOrthogonalDiagonal
                                                                                                                              L∃∀N

                                                                                                                                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.

                                                                                                                                Proof. 

                                                                                                                                  Write \(B(x,y)=Q(x+y)-Q(x)-Q(y)\) for the unhalved polar form. Choose \(u\ne 0\) with \(Q(u)=0\). Nondegeneracy makes \(B(u,-)\) a nonzero functional, so its kernel \(u^\perp \) has dimension \(d-1\geq 2\). It contains the line \(\mathbb Q u\); choose \(w\in u^\perp \setminus \mathbb Q u\). The Eichler transvection of Proposition [fcap-002M] is \[T=E_{u,w}\in SO(Q),\qquad T^m=E_{u,mw} \quad (m\in \mathbb Z).\] The power formula follows from the additive composition law there.

                                                                                                                                  Every nonzero integer power is nonidentity. Indeed, if \(E_{u,v}=1\) with \(v\in u^\perp \), its formula on \(x\in u^\perp \) reduces to \[E_{u,v}(x)-x=-B(x,v)u.\] Since \(u\ne 0\), this forces \(v\in (u^\perp )^\perp \). Nondegeneracy and finite dimension give \((u^\perp )^\perp =\mathbb Q u\): the left side has dimension one and contains \(u\). Taking \(v=mw\), with \(m\ne 0\), contradicts the choice of \(w\).

                                                                                                                                  Apply the tuple's rational membership condition to the single element \(T\). There is a finite set of primes \(S\) such that \(T_p\in U_p^{SO}\) for every \(p\notin S\). Each reference is a subgroup, so every power \(T_p^{n!}\) belongs there too. Consequently all terms of the sequence \[g_n=\delta _f^{SO}(T^{n!})\quad (n\geq 1)\] belong to the same principal stage \[SO_S(U)=\prod _{p\in S}SO_p\times \prod _{p\notin S}U_p^{SO}.\] The identity also belongs to this stage. The exceptional set is independent of \(n\); separate exceptional sets for each term would not suffice for this convergence argument.

                                                                                                                                  Fix a prime \(p\). With the valuation normalized by \(v_p(p)=1\), \[v_p(n!)\geq \lfloor n/p\rfloor \longrightarrow \infty , \qquad n!\longrightarrow 0\quad \text {in }\mathbb Q_p.\] Scalar extension of the formula for \(T\) gives \(T_p^{n!}=E_{u_p,n!w_p}\). In any fixed local basis, the entries of \(E_{u_p,tw_p}\) are polynomials in \(t\), with value the identity at \(t=0\). Its inverse is \(E_{u_p,-tw_p}\), whose entries have the same property. Hence \(T_p^{n!}\to 1\) in the canonical inverse-graph topology of Definition [fcap-0044]. For \(p\notin S\), the convergence also holds in the subgroup topology of \(U_p^{SO}\).

                                                                                                                                  Coordinatewise convergence is convergence in the product topology of this one stage. Its inclusion into the restricted product is continuous by Definition [fcap-004F], so \(g_n\to 1\) in \(SO_f(U)\). The rational diagonal is injective by Definition [fcap-004K]; since \(n!\ne 0\), every \(g_n\ne 1\). If the diagonal image were discrete, an ambient neighborhood would meet it only at the identity, contrary to convergence of this sequence.

                                                                                                                                  In the explicit matrix of Example [fcap-002N], 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 [fcap-004L]. 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 [fcap-002M]; 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.

                                                                                                                                  Definition. The finite adelic spinor norm and its reference images [fcap-004N]

                                                                                                                                    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 [fcap-0023], 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 [fcap-004F]; 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 [fcap-0046] 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 [fcap-004F].

                                                                                                                                    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 [fcap-004J]: 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.

                                                                                                                                    Proposition. The adelic spinor kernel [fcap-004O]

                                                                                                                                      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 [fcap-004J] 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\).

                                                                                                                                      Proof. 

                                                                                                                                        The identity of the restricted product \(C_f(U)\) has identity at every prime. Thus \(\Theta (g)=1\) if and only if every \(\theta _p(g_p)=1\), proving the kernel description. For a restricted Spin element \(s\), the local image/kernel theorem Theorem [fcap-0023] gives \(\theta _p(\rho _p(s_p))=1\) at every prime. The already constructed \(\rho _f(s)\) is restricted, so it lies in \(\ker \Theta \). Corestriction preserves its homomorphism law.

                                                                                                                                        Let \(j:\ker \Theta \hookrightarrow SO_f(U)\) be the inclusion. Every open subset of the kernel is of the form \(A\cap \ker \Theta \), for some open \(A\subseteq SO_f(U)\). Its preimage under \(\bar \rho _f\) is \(\rho _f^{-1}(A)\), which is open by continuity of \(\rho _f\). This proves continuity of the corestriction and the factorization \(j\bar \rho _f=\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 [fcap-003N] 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 [fcap-004N]. 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 [fcap-0023] 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 [fcap-0023]. 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.

                                                                                                                                        Definition. Finite adelic class sets [fcap-004P]

                                                                                                                                          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 [fcap-004F] 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.

                                                                                                                                          Proof. 

                                                                                                                                            Reflexivity follows from \(x=1x1\). If \(y=\gamma xk\), then \(x=\gamma ^{-1}yk^{-1}\), and the inverses remain in their respective subgroups, proving symmetry. If also \(z=\eta y\ell \), where \(\eta \in \Gamma _G\) and \(\ell \in K_G\), then associativity gives \[z=\eta (\gamma xk)\ell =(\eta \gamma )x(k\ell ).\] The products \(\eta \gamma \in \Gamma _G\) and \(k\ell \in K_G\) give transitivity. Their order matters; neither subgroup is assumed commutative or normal. This proves the equivalence relation separately for all three groups.

                                                                                                                                            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 [fcap-004F], 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.

                                                                                                                                            Proposition. Enlarging the right subgroup of a double coset [fcap-004Q]

                                                                                                                                              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.

                                                                                                                                              Proof. 

                                                                                                                                                If \([x]_K=[y]_K\), there are \(\gamma \in \Gamma \) and \(k\in K\) with \(y=\gamma xk\). The inclusion puts the same \(k\) in \(K'\), so the same witnesses give \([x]_{K'}=[y]_{K'}\). The assignment therefore does not depend on the representative. For any target class \(c\), choose a representative \(x\in G\) with \(c=[x]_{K'}\). Then \([x]_K\) is a source class and \(p_{K,K'}([x]_K)=c\), proving surjectivity.

                                                                                                                                                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 [fcap-004F], the rational image is from Definition [fcap-004K], 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.

                                                                                                                                                Proposition. Right translation and conjugate double cosets [fcap-004R]

                                                                                                                                                  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.

                                                                                                                                                  Proof. 

                                                                                                                                                    The map \(c_a(k)=a^{-1}ka\) is a group automorphism: \(c_a(1)=1\) and \[(a^{-1}ka)(a^{-1}\ell a)=a^{-1}(k\ell )a,\] while its inverse is \(h\mapsto aha^{-1}\). Thus \(a^{-1}Ka=\{a^{-1}ka:k\in K\}\) is a subgroup: it contains \(1\), and the displayed product and \((a^{-1}ka)^{-1}=a^{-1}k^{-1}a\) keep products and inverses inside it.

                                                                                                                                                    Suppose \(y=\gamma xk\) with \(\gamma \in \Gamma \) and \(k\in K\). Associativity and cancellation give \[ya=\gamma (xa)(a^{-1}ka).\] Since \(a^{-1}ka\in a^{-1}Ka\), this proves that \(T_a\) is independent of the representative. For the proposed inverse, suppose \(w=\eta z h\), where \(\eta \in \Gamma \) and \(h\in a^{-1}Ka\). Choose \(k\in K\) with \(h=a^{-1}ka\). Then the inverse's witnesses are \(\eta \) and \(k\), since \[wa^{-1}=\eta z(a^{-1}ka)a^{-1} =\eta (za^{-1})k.\] The inverse assignment is therefore well defined. On a source representative its composite with \(T_a\) gives \((xa)a^{-1}=x\); on a target representative the other composite gives \((za^{-1})a=z\). Every quotient class has a representative, so both composites are the identity.

                                                                                                                                                    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 [fcap-004F], 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.

                                                                                                                                                    Proposition. Transporting double cosets by a group isomorphism [fcap-004S]

                                                                                                                                                      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.

                                                                                                                                                      Proof. 

                                                                                                                                                        If \(y=\gamma xk\) with \(\gamma \in \Gamma \) and \(k\in K\), then \[e(y)=e(\gamma )e(x)e(k).\] The two image equalities put \(e(\gamma )\) in \(\Gamma '\) and \(e(k)\) in \(K'\), so the proposed map is independent of the representative. Conversely, suppose \(w=\gamma 'zk'\) with \(\gamma '\in \Gamma '\) and \(k'\in K'\). The same equalities give \(e^{-1}(\gamma ')\in \Gamma \) and \(e^{-1}(k')\in K\), and \[e^{-1}(w)=e^{-1}(\gamma ')e^{-1}(z)e^{-1}(k').\] Thus the inverse assignment is well defined. Applying the two assignments successively to any representative gives \(e^{-1}(e(x))=x\) or \(e(e^{-1}(z))=z\), respectively. Every class has a representative, so both composites are identities.

                                                                                                                                                        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.

                                                                                                                                                        Proposition. Finite changes of references and the product subgroup [fcap-004T]

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

                                                                                                                                                          Proof. 

                                                                                                                                                            If \(x_p\in U_p\) outside a finite set \(S\), then \(x_p\in U'_p\) outside \(S\cup F\). Interchanging the two families proves the converse. Thus the two groups have the same tuples and coordinate operations, giving the stated isomorphism.

                                                                                                                                                            Everywhere equality of references immediately gives equality of their products. For the converse, suppose \(e(K(U))=K(U')\). Fix a prime \(p\) and \(u\in U_p\). The tuple with component \(u\) at \(p\) and identity at every other prime belongs to \(K(U)\). Its image is the same tuple in \(K(U')\), so \(u\in U'_p\). This proves \(U_p\subseteq U'_p\). Interchange the products and repeat the argument to obtain \(U'_p\subseteq U_p\). Since \(p\) was arbitrary, all reference subgroups agree.

                                                                                                                                                            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 [fcap-004S] 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.

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

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

                                                                                                                                                              Proposition. The compact real Spin projection is a two-sheeted cover [fcap-0039]

                                                                                                                                                                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.

                                                                                                                                                                Proposition. The compact Spin cover is universal from dimension three [fcap-003A]

                                                                                                                                                                  For \(n\geq 3\), the covering in Proposition [fcap-0039] is the universal covering of \(SO(n)\). The proof uses the action on the unit sphere from Theorem [fcap-0024], 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 [fcap-0039] 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.

                                                                                                                                                                  Backlinks

                                                                                                                                                                    Proposition. Full rational diagonals are discrete under lattice containment [fcap-004L]

                                                                                                                                                                      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 [fcap-004D]. 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 [fcap-004D], its rational-basis changes and its finite shrinkings from Proposition [fcap-004E].

                                                                                                                                                                      Proof. 

                                                                                                                                                                        Put \(W_p=U_p^O\cap H_p\). The groups \(W_p\) are open, since both factors are open by Definition [fcap-004C] and Proposition [fcap-004D]. Choose a finite set \(F\) outside which \(U_p^O\subseteq H_p\); then \(W_p=U_p^O\) for \(p\notin F\). Thus \[K_W=\prod _p W_p\subseteq O_f(U)\] is an open identity neighborhood. Indeed, inside the open principal stage \(O_F(U)\) it imposes an open condition on only the finitely many coordinates in \(F\), and leaves the other reference factors unchanged. This uses the stage topology of Definition [fcap-004F].

                                                                                                                                                                        Let \(M_b(g_\infty )\) be the real matrix of \(g_\infty \in O_\infty \) in the extended basis, and put \[A=\left \{g_\infty \in O_\infty : \left |M_b(g_\infty )_{ij}-\delta _{ij}\right |<\tfrac 12 \text { for every }i,j\right \}.\] Here \(\delta _{ij}\) is the Kronecker delta. The finitely many matrix entries are continuous by Definition [fcap-0044], so \(A\) is open and contains the identity. Hence \(A\times K_W\) is an open identity neighborhood in \(O_{\mathbb A}(U)\).

                                                                                                                                                                        Suppose a rational \(g\in O(Q)\) has diagonal in this neighborhood. Every \(g_p\) stabilizes \(L_p\); therefore each entry of its rational matrix \(M_b(g)\) belongs to \(\mathbb Z_p\) at every prime. A reduced fraction \(a/d\), with \(d>0\), has this property only if \(d=1\): a prime divisor \(p\) of \(d\) does not divide \(a\), giving negative \(p\)-adic valuation. Thus all the entries of \(M_b(g)\) are integers. Their real values differ from \(\delta _{ij}\) by less than \(1/2\); an integer with that property must equal \(\delta _{ij}\). Consequently \(g=1\). This isolates the identity in the orthogonal diagonal image. Translation by each diagonal element isolates every point of that image.

                                                                                                                                                                        Pull the neighborhood back under the continuous inclusion \(SO_{\mathbb A}(U)\to O_{\mathbb A}(U)\) from Proposition [fcap-004J]. Naturality from Definition [fcap-004K] shows that its intersection with the rational SO image contains only the identity: the underlying rational orthogonal transformation is already the identity. This proves SO discreteness.

                                                                                                                                                                        Pull this SO neighborhood back along the continuous map \(\rho _{\mathbb A}:\operatorname {Spin}_{\mathbb A}(U)\to SO_{\mathbb A}(U)\). A rational Spin point in this preimage has rational projection \(1\), by naturality and injectivity of the SO diagonal. If \(\dim V>0\), the field version of the scalar-kernel statement in Lemma [fcap-001C] gives precisely \(s=1\) or \(s=-1\). The real Spin group is Hausdorff, and the scalar elements \(1\) and \(-1\) are distinct there. Choose an open real identity neighborhood \(B_\infty \) excluding \(-1\). Intersect the preceding preimage with \(B_\infty \times \operatorname {Spin}_f(U)\). The intersection is open and its rational diagonal points consist of \(1\) alone. Translation proves Spin discreteness.

                                                                                                                                                                        If \(\dim V=0\), the actual vector-generated Spin carrier is \(\{1\}\), as in Lemma [fcap-003H]; both orthogonal carriers are also singleton. The conclusion is immediate. In particular there is no extra scalar \(-1\) in this generated zero-dimensional carrier.

                                                                                                                                                                        For the integral tuple, \(U_p^O=H_p\) at every prime. Finite shrinking only replaces reference subgroups by smaller ones, so it preserves containment. Changing rational basis changes \(H_p\) at only finitely many primes by Proposition [fcap-004E]. Adjoin these primes to the exceptional set to retain the hypothesis.

                                                                                                                                                                        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 [fcap-001C] 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.

                                                                                                                                                                        Definition. Rational diagonal subgroups [fcap-004K]

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

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

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

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

                                                                                                                                                                          Proof. 

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

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

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

                                                                                                                                                                            Proposition. The adelic spinor kernel [fcap-004O]

                                                                                                                                                                              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 [fcap-004J] 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\).

                                                                                                                                                                              Proof. 

                                                                                                                                                                                The identity of the restricted product \(C_f(U)\) has identity at every prime. Thus \(\Theta (g)=1\) if and only if every \(\theta _p(g_p)=1\), proving the kernel description. For a restricted Spin element \(s\), the local image/kernel theorem Theorem [fcap-0023] gives \(\theta _p(\rho _p(s_p))=1\) at every prime. The already constructed \(\rho _f(s)\) is restricted, so it lies in \(\ker \Theta \). Corestriction preserves its homomorphism law.

                                                                                                                                                                                Let \(j:\ker \Theta \hookrightarrow SO_f(U)\) be the inclusion. Every open subset of the kernel is of the form \(A\cap \ker \Theta \), for some open \(A\subseteq SO_f(U)\). Its preimage under \(\bar \rho _f\) is \(\rho _f^{-1}(A)\), which is open by continuity of \(\rho _f\). This proves continuity of the corestriction and the factorization \(j\bar \rho _f=\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 [fcap-003N] 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 [fcap-004N]. 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 [fcap-0023] 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 [fcap-0023]. 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.

                                                                                                                                                                                Definition. The finite adelic spinor norm and its reference images [fcap-004N]

                                                                                                                                                                                  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 [fcap-0023], 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 [fcap-004F]; 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 [fcap-0046] 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 [fcap-004F].

                                                                                                                                                                                  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 [fcap-004J]: 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.

                                                                                                                                                                                  Related

                                                                                                                                                                                    Definition. Away restricted products and finite-prime splitting [fcap-004G]

                                                                                                                                                                                      Use the Hausdorff locally compact groups \(G_p\) and compact open references \(U_p\) of Definition [fcap-004F]. 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 [fcap-004F] 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 [fcap-004F], 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\).

                                                                                                                                                                                      Proof. 

                                                                                                                                                                                        The inverse of \(d_R\) reinserts the coordinates indexed by \(R\). If the away tuple has finite exceptional set \(T\), the reconstructed tuple has exceptional set contained in \(R\cup T\). This is finite, so the inverse is well defined. Coordinate restriction and reinsertion are mutually inverse homomorphisms. Continuity of \(d_R\) follows from the continuous coordinate evaluations of Definition [fcap-004F] and the continuous map \(r_R\).

                                                                                                                                                                                        For the inverse, the open subsets \[\Bigl (\prod _{p\in R}G_p\Bigr )\times G_T^R(U)\] cover the target as \(T\) ranges over the finite subsets of the complement. On each such subset reinsertion is the product rearrangement onto \(G_{R\cup T}(U)\), followed by its continuous inclusion into \(G_f(U)\). Hence the inverse is continuous on an open cover, and therefore continuous everywhere. This argument uses the established open stages and the ordinary product topology.

                                                                                                                                                                                        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.

                                                                                                                                                                                        Lemma. Closed local carriers and continuous Clifford actions [fcap-0045]

                                                                                                                                                                                          Definition [spin-000O]

                                                                                                                                                                                          Let \(K\) be a local field of characteristic different from two in the sense of Definition [fcap-0044], 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 [fcap-002D], 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 [fcap-0044]; 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 [fcap-001A] 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.

                                                                                                                                                                                          Definition. Compatible compact-open reference subgroups [fcap-004C]

                                                                                                                                                                                            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 [fcap-0044]. The actions are continuous by Lemma [fcap-0045]. For a rational orthogonal or Spin point \(x\), write \(x_p\) for its scalar extension; the action compatibility is Theorem [fcap-003N].

                                                                                                                                                                                            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 [fcap-0045]: 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 [fcap-004D].

                                                                                                                                                                                            Definition. Finite restricted products [fcap-004F]

                                                                                                                                                                                              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 [fcap-004D]. 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.

                                                                                                                                                                                              Proof. 

                                                                                                                                                                                                The identity belongs to every reference subgroup. The product of tuples with exceptional sets \(S\) and \(T\) has exceptional set contained in \(S\cup T\); inversion preserves a tuple's exceptional set. Thus the coordinate operations define a group on \(G_f(U)\), which is the union of its principal stages.

                                                                                                                                                                                                If \(S\subseteq T\), the inclusion \(G_S(U)\to G_T(U)\) replaces only the finitely many factors \(U_p\) for \(p\in T\setminus S\) by \(G_p\). Each inclusion \(U_p\hookrightarrow G_p\) is an open embedding, so the product inclusion is an open embedding. For arbitrary finite \(S,T\), \[G_S(U)\cap G_T(U)=G_{S\cap T}(U).\] This intersection is open in both stages with the same topology. If \(A\) is open in \(G_S(U)\), its intersection with \(G_T(U)\) is therefore open in \(G_T(U)\): first intersect with the open \(G_{S\cap T}(U)\), then use its open inclusion into \(G_T(U)\). Hence \(A\) is open in the union topology. Conversely, an open set of the union restricts to an open set in each stage by definition. This proves both the claimed stage topology and stage openness.

                                                                                                                                                                                                A coordinate evaluation is continuous on every stage, hence on the union by the definition of its topology. Two distinct tuples differ at some prime; disjoint neighborhoods in that Hausdorff factor pull back to disjoint neighborhoods of the tuples. Thus the union is Hausdorff. Multiplication restricts to a continuous map \[G_S(U)\times G_T(U)\longrightarrow G_{S\cup T}(U)\] by continuity in each factor of the product topology. These open products cover \(G_f(U)\times G_f(U)\), proving continuity of multiplication. Inversion is continuous on each open stage, hence on the union. Finally \(K(U)\) is compact by the product compactness theorem and open as the empty stage. Its translates are compact neighborhoods of every point, proving local compactness.

                                                                                                                                                                                                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 [fcap-0045]. 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 [fcap-004E] 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.

                                                                                                                                                                                                Definition. Full adelic groups and the real factor [fcap-004H]

                                                                                                                                                                                                  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 [fcap-0044]. In particular \(\operatorname {Spin}_\infty \) uses the actual vector-generated, even, reverse-norm-one carrier of Lemma [fcap-0045].

                                                                                                                                                                                                  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 [fcap-004F]. 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 [fcap-0045] gives those properties for the real factor, and Definition [fcap-004F] 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.

                                                                                                                                                                                                  Definition. Spin group [gallier2014clifford] [spin-000N]

                                                                                                                                                                                                     Every Clifford algebra \(\mathrm {Cl}(\Phi )\) possesses a canonical anti-automorphism \(t: \mathrm {Cl}(\Phi ) \rightarrow \mathrm {Cl}(\Phi )\) satisfying the properties \[ t(x y)=t(y) t(x), \quad t \circ t=\mathrm {id}, \quad \text { and } \quad t(i(v))=i(v), \] for all \(x, y \in \mathrm {Cl}(\Phi )\) and all \(v \in V\). Furthermore, such an anti-automorphism is unique. Every Clifford algebra \(\mathrm {Cl}(\Phi )\) has a unique canonical automorphism \(\alpha : \mathrm {Cl}(\Phi ) \rightarrow \mathrm {Cl}(\Phi )\) satisfying the properties \[ \alpha \circ \alpha =\mathrm {id}, \quad \text { and } \quad \alpha (i(v))=-i(v), \] for all \(v \in V\). First, we define conjugation on a Clifford algebra \(\mathrm {Cl}(\Phi )\) as the map \[ x \mapsto \bar {x}=t(\alpha (x)) \text { for all } x \in \mathrm {Cl}(\Phi ) . \] Given a finite dimensional vector space \(V\) and a quadratic form \(\Phi \) on \(V\), the Clifford group of \(\Phi \) is the group \[ \Gamma (\Phi )=\left \{x \in \mathrm {Cl}(\Phi )^* \mid \alpha (x) v x^{-1} \in V \quad \text { for all } v \in V\right \} . \] The map \(N: \mathrm {Cl}(Q) \rightarrow \mathrm {Cl}(Q)\) given by \[ N(x)=x \bar {x} \] is called the norm of \(\mathrm {Cl}(\Phi )\).

                                                                                                                                                                                                    We also define the group \(\Gamma ^{+}(\Phi )\), called the special Clifford group, by \[ \Gamma ^{+}(\Phi )=\Gamma (\Phi ) \cap \mathrm {Cl}^0(\Phi ) . \]

                                                                                                                                                                                                    We define the pinor group \(\operatorname {Pin}(p, q)\) as the group \[ \operatorname {Pin}(p, q)=\left \{x \in \Gamma _{p, q} \mid N(x)= \pm 1\right \}, \] and the spinor group \(\operatorname {Spin}(p, q)\) as \(\operatorname {Pin}(p, q) \cap \Gamma _{p, q}^{+}\).

                                                                                                                                                                                                    The restriction of \(\rho : \Gamma _{p, q} \rightarrow \mathbf {G L}(n)\) to the pinor group \(\operatorname {Pin}(p, q)\) is a surjective homomorphism \(\rho : \mathbf {P i n}(p, q) \rightarrow \mathbf {O}(p, q)\) whose kernel is \(\{-1,1\}\), and the restriction of \(\rho \) to the spinor group \(\mathbf {S p i n}(p, q)\) is a surjective homomorphism \(\rho : \mathbf {S p i n}(p, q) \rightarrow \mathbf {S O}(p, q)\) whose kernel is \(\{-1,1\}\).

                                                                                                                                                                                                    Remark: According to Atiyah, Bott and Shapiro, the use of the name \(\operatorname {Pin}(k)\) is a joke due to Jean-Pierre Serre (Atiyah, Bott and Shapiro Clifford modules, page 1).

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

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

                                                                                                                                                                                                      Proof. 

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

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

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

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

                                                                                                                                                                                                        Theorem. The Spin image is the spinor-norm kernel [fcap-0023]
                                                                                                                                                                                                        range_spinToSpecialOrthogonal_eq_ker_spinorNorm
                                                                                                                                                                                                        L∃∀N

                                                                                                                                                                                                          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.

                                                                                                                                                                                                          Proof. 

                                                                                                                                                                                                            Every Spin element has reverse norm one, so its image has trivial spinor norm CliffordAlgebra.spinorNorm_spinToSpecialOrthogonal. Conversely, suppose first that \(V\) has positive dimension. Take \(g\in SO(V,Q)\) with \(\nu _Q(g)=1\), and choose a Lipschitz lift \(x\) of \(g\). Since \(\det (g)=1\), determinant parity first shows that \(x\) is even CliffordAlgebra.mem_even_of_det_lipschitzToOrthogonal_eq_one Lemma [fcap-001A]. Trivial spinor class says that \(N_{\mathrm {rev}}(x)\) is a square. Scalar normalization therefore produces an even lift with reverse norm one source theorem; by the even-element comparison in Remark [fcap-0028], it lies in Spin and has the same orthogonal action. In dimension zero \(SO(V,Q)\) is trivial, so the image and the spinor-norm kernel are both its identity subgroup.

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

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

                                                                                                                                                                                                              Lemma. The volume term does not obstruct Spin in dimension five [fcap-003H]

                                                                                                                                                                                                                Let \(K\) be a field of characteristic different from two, and let \((V,Q)\) be a nondegenerate quadratic space of dimension five over \(K\). For \(x\in \mathcal {C}\kern -2pt\ell ^{+}(Q)\), \[x\text { is the Clifford value of a Spin element} \quad \Longleftrightarrow \quad \operatorname {rev}(x)x=1.\] The norm condition implies Lipschitz membership in this dimension CliffordAlgebra.evenUnitaryGroup_le_lipschitzGroup_of_finrank_eq_five. The point is to remove the possible degree-five term left by the dimension-four argument of Lemma [fcap-002J].

                                                                                                                                                                                                                Choose an orthogonal basis \(e_1,\ldots ,e_5\), suppress the generator map, and put \(\omega =e_1\cdots e_5\). Nondegeneracy gives \[\omega ^2=\delta 1,\qquad \delta =\prod _{i=1}^5 Q(e_i)\ne 0.\] The element \(\omega \) is central and invertible. Suppose \(\operatorname {rev}(x)x=1\). Finite dimensionality makes the left inverse a two-sided inverse. For any \(v\in V\), the element \(y=xvx^{-1}\) is odd and satisfies \(\operatorname {rev}(y)=y\). In the orthogonal monomial basis, reversal has signs \(+1,-1,+1\) on degrees one, three and five. Hence \[y=w+c\omega \qquad (w\in V,\ c\in K).\]

                                                                                                                                                                                                                Conjugation preserves the scalar square of a vector. Since \(\omega \) is central, \[Q(v)1=y^2=Q(w)1+2c\omega w+c^2\delta 1.\] Each \(\omega e_i\) is a nonzero scalar multiple of the product of the other four basis vectors. Thus \(\omega w\) has pure degree four in this basis, whereas the other terms in the equation are scalar. Independence of the Clifford basis gives \(2c\omega w=0\). As two and \(\omega \) are invertible, either \(c=0\) or \(w=0\). In the latter case \(y=c\omega \) is central, so conjugating back gives \(v=x^{-1}yx=y=c\omega \). The degree-one and degree-five subspaces have zero intersection; therefore \(v=0\) and \(c=0\). In both cases \(y\in V\).

                                                                                                                                                                                                                Thus \(x\) normalizes the vector space. The Clifford-group characterization makes it Lipschitz; together with evenness and reverse norm one, this is the Spin criterion of Remark [fcap-0028]. The reverse implication is that same criterion. In fact the carrier equality holds in every dimension from one through five CliffordAlgebra.range_spinGroup_toUnits_eq_evenUnitaryGroup. The lower bound matters: in dimension zero the vector-generated Lipschitz group is trivial, whereas the even-unitary group contains both \(1\) and \(-1\). This carrier equality alone supplies no symplectic matrix model; the spinor pairing and matrix inverse for complex dimension five remain the separate argument of Proposition [fcap-0033].

                                                                                                                                                                                                                Porteous gives the real dimension-five proof by separating the vector, trivector and volume terms [porteous1995clifford, Chapter 16, Proposition 16.15, p. 147]. His relation is \(v^2=-q(v)\), so here \(Q=-q\); his conjugation is \(\operatorname {rev}\circ \alpha \), equal to reversal on even elements. His indefinite Spin carrier permits norm \(\pm 1\); we select norm \(+1\). The basis calculation above extends the norm-one argument from real spaces to the stated fields: orthogonality, nonzero basis squares and invertibility of two replace any need for real unit-length normalization. Gallier records the compact boundary at five and the failure at six [gallier2014clifford, Section 1.4, closing Remark, p. 31]; the next example computes that failure.