Changing the field need not require new generators or a new quadratic
basis. Let \(L/K\) be a field extension with \(\operatorname {char}K\ne 2\),
and let \((V,Q)\) be a finite-dimensional quadratic space, possibly degenerate.
Its scalar extension is \(V_L=L\otimes _K V\) with quadratic form
\(Q_L\) characterized by \(Q_L(a\otimes v)=a^2Q(v)\) and the extended polar
form. There are canonical \(L\)-algebra isomorphisms
\[\begin {aligned}
\beta _Q:L\otimes _K\mathcal {C}\kern -2pt\ell _K(Q)&\longrightarrow \mathcal {C}\kern -2pt\ell _L(Q_L),\\
a\otimes \iota _Q(v)&\longmapsto a\,\iota _{Q_L}(1\otimes v),\\
\beta _\wedge :L\otimes _K\bigwedge _K V&\longrightarrow \bigwedge _L V_L,\\
a\otimes (v_1\wedge \cdots \wedge v_r)&\longmapsto
a(1\otimes v_1)\wedge \cdots \wedge (1\otimes v_r).
\end {aligned}\]
The first preserves the word-length filtration
and parity; the second preserves exterior degree. No nondegeneracy hypothesis
or chosen basis is needed to define either map.
The Clifford statement is [chevalley1954algebraic, II.1.5, p. 41].
The proof below uses the universal property; applying it
to the zero form gives the exterior algebra statement.
Write \(C=\mathcal {C}\kern -2pt\ell _K(Q)\) and \(C_L=\mathcal {C}\kern -2pt\ell _L(Q_L)\), and denote the
leading-symbol equivalences of Theorem [fcap-000I] by \(\sigma _K,\sigma _L\).
Scalar extension and taking the exterior symbol commute:
Tensoring vector spaces preserves these filtration quotients.
On each generator word, both paths give the exterior product of its
extended vectors. Such words span every graded piece, so the square commutes.For example, \(\beta _Q(1\otimes \iota _Q(v)^2)=Q(v)1\), whereas
\((1\otimes v)\wedge (1\otimes v)=0\). The square compares
associated graded multiplication. It does not turn the linear
Clifford-to-exterior coordinates of Definition [fcap-0003] into an algebra map.
Chevalley makes this product distinction immediately after II.1.5.
The marked declarations give the two algebra equivalences in the reverse
direction. Mathlib allows arbitrary commutative base and extension rings with
\(2\) invertible; TauCeti's exterior equivalence needs neither invertible two
nor flatness. The symbol square above is the consequence proved here,
using the existing leading-symbol equivalence. The separate Spin-lifting
consequences remain in Theorem [fcap-003N] and Proposition [fcap-003O].
Theorem [ca-000C]Definition [ca-000E]