English
For a commutative ring R and a quadratic form Q on an R-module M, there is a canonical R-linear map ι_Q from M into the Clifford algebra Clifford(Q). This map is obtained by composing the natural injection of M into the tensor algebra with the quotient map that enforces the defining relations of the Clifford algebra.
Русский
Для кольца R и квадратичной формы Q на R-модуле M существует каноническое R-линейное отображение ι_Q: M → Clifford(Q). Это отображение получается как композиция естественного вложения M в тензор-алгебру и фактор-мозаики, задающей отношения Клиффорда.
LaTeX
$$$\\iota_Q = (\\operatorname{RingQuot.mkAlgHom}\\, R\\, (Rel\\ Q)).toLinearMap \\circ (TensorAlgebra.\\ι\\ R)$. In particular, for each $m\\in M$, $\\iota_Q(m)$ is the image of $m$ in the Clifford algebra via the canonical construction.$$
Lean4
/-- The canonical linear map `M →ₗ[R] CliffordAlgebra Q`.
-/
def ι : M →ₗ[R] CliffordAlgebra Q :=
(RingQuot.mkAlgHom R _).toLinearMap.comp (TensorAlgebra.ι R)
