English
The augmented quadratic form Q' on M×R computed via the product with - squared term relates to Q(m).
Русский
Расширенная квадратичная форма Q' на пространстве M×R выражается через произведение и вычитание квадрата.
LaTeX
$$Q'(m, r) = Q(m) - r^2$$
Lean4
/-- Every algebra morphism from the even subalgebra is in one-to-one correspondence with a
bilinear map that sends duplicate arguments to the quadratic form, and contracts across
multiplication. -/
@[simps! symm_apply_bilin]
def lift : EvenHom Q A ≃ (CliffordAlgebra.even Q →ₐ[R] A)
where
toFun f := AlgHom.ofLinearMap (aux f) (aux_one f) (aux_mul f)
invFun F := (even.ι Q).compr₂ F
left_inv f := EvenHom.ext <| LinearMap.ext₂ <| even.lift.aux_ι f
right_inv _ := even.algHom_ext Q <| EvenHom.ext <| LinearMap.ext₂ <| even.lift.aux_ι _
