toBaseChange_ofBaseChange — Mathlib

English

There exists an equivalence between CliffordAlgebra(Q) and CliffordAlgebra(Q.baseChange A) after base change, with explicit inverse given by ofBaseChange and toBaseChange, forming an isomorphism of A-algebras.

Русский

Существует эквивалентность между CliffordAlgebra(Q) и CliffordAlgebra(Q.baseChange A) после изменения базы, с явным обратным отображением, образованным через ofBaseChange и toBaseChange, образуя изоморфизм А-алгебр.

LaTeX

$$$\text{equivBaseChange}(Q) : \mathrm{Clifford}(Q.baseChange A) \simeq_A A \otimes_R \mathrm{Clifford}(Q)$$$

Lean4

@[simp]
theorem toBaseChange_ofBaseChange (Q : QuadraticForm R V) (x : A ⊗[R] CliffordAlgebra Q) :
    toBaseChange A Q (ofBaseChange A Q x) = x :=
  AlgHom.congr_fun (toBaseChange_comp_ofBaseChange A Q :) x

Похожие утверждения