toBaseChange_ι — Mathlib

English

Base-changing the vector space is isomorphic to changing the Clifford algebra itself via the canonical equivalence: there is an algebra isomorphism 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) \cong_A A \otimes_R \mathrm{Cℓ}(V, Q)$$$

Lean4

@[simp]
theorem toBaseChange_ι (Q : QuadraticForm R V) (z : A) (v : V) :
    toBaseChange A Q (ι (Q.baseChange A) (z ⊗ₜ v)) = z ⊗ₜ ι Q v :=
  CliffordAlgebra.lift_ι_apply _ _ _

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