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.