equiv — Mathlib

English

There is an algebra equivalence between the Clifford algebra over Q c1 c2 and the quaternion algebra ℍ[R,c1,0,c2], establishing a canonical isomorphism of R-algebras.

Русский

Между клиффордовой алгеброй над Q c1 c2 и кватернионной алгеброй ℍ[R,c1,0,c2] существует каноническое равносилование алгебр, т.е. изоморфизм R-алгебр.

LaTeX

$$$\text{CliffordAlgebra}(Q) \cong_R \mathbb{H}_{R}(c_{1},0,c_{2})$$$

Lean4

/-- The clifford algebra over `CliffordAlgebraQuaternion.Q c₁ c₂` is isomorphic as an `R`-algebra
to `ℍ[R,c₁,c₂]`. -/
@[simps!]
protected def equiv : CliffordAlgebra (Q c₁ c₂) ≃ₐ[R] ℍ[R,c₁,0,c₂] :=
  AlgEquiv.ofAlgHom toQuaternion ofQuaternion toQuaternion_comp_ofQuaternion ofQuaternion_comp_toQuaternion

Похожие утверждения