English
There is a canonical algebra homomorphism from A ⊗ CliffordAlgebra Q to CliffordAlgebra (Q.baseChange A) implementing the base change, i.e., the morphism that intertwines tensoring with algebra structure and the Clifford relations.
Русский
Существует каноническое алгебро-однозначное отображение из A ⊗ CliffordAlgebra Q в CliffordAlgebra(Q.baseChange A), реализующее изменение базиса и совместимое с отношениями Клиффорда.
LaTeX
$$$\phi : A \otimes_R \mathrm{Clifford}(Q) \to_A \mathrm{Clifford}(Q.baseChange A)$$$
Lean4
/-- Convert from the base-changed clifford algebra to the clifford algebra over a base-changed
module. -/
def ofBaseChange (Q : QuadraticForm R V) : A ⊗[R] CliffordAlgebra Q →ₐ[A] CliffordAlgebra (Q.baseChange A) :=
Algebra.TensorProduct.lift (Algebra.ofId _ _) (ofBaseChangeAux A Q) fun _a _x => Algebra.commutes _ _
