English
There exists a linear map that changes the quadratic form from Q to Q′, sending vectors to vectors and scalars to scalars, adjusting products by a contraction term linked to the bilinear form B. This is the λ_B construction.
Русский
Существует линейное отображение, переходящее от клиффордовой алгебры с формой Q к формe Q′, отправляющее вектора в вектора, скаляры в скаляры, а произведения корректирует поплавок от билиниальной формы B. Это конструкция λ_B.
LaTeX
$$$\text{changeForm}(h) : \mathrm{CliffordAlgebra}(Q) \to_R \mathrm{CliffordAlgebra}(Q')$, где $h : B^{toQuadraticMap} = Q' - Q$ и $B$ задаёт форму перехода.$$
Lean4
/-- Convert between two algebras of different quadratic form, sending vector to vectors, scalars to
scalars, and adjusting products by a contraction term.
This is $\lambda_B$ from [bourbaki2007][] $9 Lemma 2. -/
def changeForm (h : B.toQuadraticMap = Q' - Q) : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q' :=
foldr Q (changeFormAux Q' B)
(fun m x =>
(changeFormAux_changeFormAux Q' B m x).trans <|
by
dsimp only [← BilinMap.toQuadraticMap_apply]
rw [h, QuadraticMap.sub_apply, sub_sub_cancel])
1
