The base change of a clifford algebra #
In this file we show the isomorphism
CliffordAlgebra.equivBaseChange A Q:
CliffordAlgebra (Q.baseChange A) ≃ₐ[A] (A ⊗[R] CliffordAlgebra Q)with forward direction
CliffordAlgebra.toBasechange A Qand reverse direction
CliffordAlgebra.ofBasechange A Q.
This covers a more general case of the complexification of clifford algebras (as described in §2.2
of https://empg.maths.ed.ac.uk/Activities/Spin/Lecture2.pdf), where ℂ and ℝ are replaced by an
2 : R is invertible).
We show the additional results:
CliffordAlgebra.toBasechange_ι: the effect of base-changing pure vectors.
CliffordAlgebra.ofBasechange_tmul_ι: the effect of un-base-changing a tensor of a pure vectors.
CliffordAlgebra.toBasechange_involute: the effect of base-changing an involution.
CliffordAlgebra.toBasechange_reverse: the effect of base-changing a reversal.
Auxiliary construction: note this is really just a heterobasic
Convert from the base-changed clifford algebra to the clifford algebra over a base-changed module.
Convert from the clifford algebra over a base-changed module to the base-changed clifford algebra.
The involution acts only on the right of the tensor product.
Auxiliary theorem used to prove
toBaseChange_reverse without needing induction.
reverse acts only on the right of the tensor product.
Base-changing the vector space of a clifford algebra is isomorphic as an A-algebra to base-changing the clifford algebra itself; <|Cℓ(A ⊗_R V, Q_A) ≅ A ⊗_R Cℓ(V, Q)<|.