English
There exists an algebra isomorphism between the Clifford algebra on Q and the even subalgebra of the adjusted form Q' Q, implemented by the equivalence EquivEven. This provides a structural bridge between the full algebra and its even part.
Русский
Существует алгебраическое изоморфное отображение между CliffordAlgebra(Q) и чётной подалгеброй (Q' Q), реализованное через эквививалентность EquivEven. Это строит связующую структуру между полной алгеброй и её чётной частью.
LaTeX
$$$ \\mathrm{CliffordAlgebra}(Q) \\cong_R \\mathrm{even}(Q' Q) $$$
Lean4
/-- Any clifford algebra is isomorphic to the even subalgebra of a clifford algebra with an extra
dimension (that is, with vector space `M × R`), with a quadratic form evaluating to `-1` on that new
basis vector. -/
def equivEven : CliffordAlgebra Q ≃ₐ[R] CliffordAlgebra.even (Q' Q) :=
AlgEquiv.ofAlgHom (toEven Q) (ofEven Q) (toEven_comp_ofEven Q) (ofEven_comp_toEven Q)
