English
Base-changing the vector space is isomorphic as an algebra to the base-changed Clifford algebra; i.e., there exists a canonical algebra equivalence between Cℓ(A ⊗_R V, Q_A) and A ⊗_R Cℓ(V, Q).
Русский
Изменение базы векторного пространства совпадает по структуре как алгебра с базовым изменением CliffordAlgebra; существует каноническое алгебро-эквивалентное отображение между Cℓ(A ⊗_R V, Q_A) и A ⊗_R Cℓ(V, Q).
LaTeX
$$$\mathrm{Cℓ}(A \otimes_R V, Q_A) \simeq_A A \otimes_R \mathrm{Cℓ}(V, Q)$$$
Lean4
/-- 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)<|.
This is `CliffordAlgebra.toBaseChange` and `CliffordAlgebra.ofBaseChange` as an equivalence. -/
@[simps!]
def equivBaseChange (Q : QuadraticForm R V) : CliffordAlgebra (Q.baseChange A) ≃ₐ[A] A ⊗[R] CliffordAlgebra Q :=
AlgEquiv.ofAlgHom (toBaseChange A Q) (ofBaseChange A Q) (toBaseChange_comp_ofBaseChange A Q)
(ofBaseChange_comp_toBaseChange A Q)
