English
Two Clifford algebras are isomorphic as algebras if their quadratic forms are isometric; given an isometry equivalence e, there is an algebra isomorphism equivOfIsometry e.
Русский
Две CliffordAlgebra являются изоморфными как алгебры, если их квадратичные формы изометричны; для изометрического эквивалентного отображения e существует алгебраическое изоморфизм equivOfIsometry e.
LaTeX
$$$ \mathrm{equivOfIsometry} (e) : \mathrm{CliffordAlgebra}(Q_1) \simeq_{\!R} \mathrm{CliffordAlgebra}(Q_2). $$$
Lean4
/-- Two `CliffordAlgebra`s are equivalent as algebras if their quadratic forms are
equivalent. -/
@[simps! apply]
def equivOfIsometry (e : Q₁.IsometryEquiv Q₂) : CliffordAlgebra Q₁ ≃ₐ[R] CliffordAlgebra Q₂ :=
AlgEquiv.ofAlgHom (map e.toIsometry) (map e.symm.toIsometry)
((map_comp_map _ _).trans <| by
convert map_id Q₂ using 2
ext m
exact e.toLinearEquiv.apply_symm_apply m)
((map_comp_map _ _).trans <| by
convert map_id Q₁ using 2
ext m
exact e.toLinearEquiv.symm_apply_apply m)
