English
The Clifford algebra of an R-module M with a quadratic form Q is the quotient of the tensor algebra T_R(M) by the ideal generated by elements of the form v ⊗ v − Q(v)·1, encoding the Clifford relations.
Русский
Клиффордова алгебра модуля M над R с квадратичной формой Q есть фактор-тензорная алгебра T_R(M) по идеалу, порождённому элементами вида v ⊗ v − Q(v)·1, задающим отношения Клиффорда.
LaTeX
$$$\mathrm{CliffordAlgebra}(Q) = \mathrm{T}_R(M) / \langle v \otimes v - Q(v) \cdot 1 \mid v \in M\rangle$$$
Lean4
theorem toBaseChange_comp_involute (Q : QuadraticForm R V) :
(toBaseChange A Q).comp (involute : CliffordAlgebra (Q.baseChange A) →ₐ[A] _) =
(Algebra.TensorProduct.map (AlgHom.id _ _) involute).comp (toBaseChange A Q) :=
by
ext v
change
toBaseChange A Q (involute (ι (Q.baseChange A) (1 ⊗ₜ[R] v))) =
(Algebra.TensorProduct.map (AlgHom.id _ _) involute : A ⊗[R] CliffordAlgebra Q →ₐ[A] _)
(toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))
rw [toBaseChange_ι, involute_ι, map_neg (toBaseChange A Q), toBaseChange_ι, Algebra.TensorProduct.map_tmul,
AlgHom.id_apply, involute_ι, TensorProduct.tmul_neg]
