ofQuaternion — Mathlib

English

Let R be a commutative ring and c1, c2 an element of R. There exists an R-algebra homomorphism from the quaternion algebra ℍ[R, c1, 0, c2] to the Clifford algebra Clifford(Q c1 c2) induced by the quaternion basis.

Русский

Пусть R — коммутативное кольцо, а c1, c2 ∈ R. Существует R-алгебра-гомоморфизм из кватернионной алгебры ℍ[R, c1, 0, c2] в клиффордову алгебру Clifford(Q c1 c2), индуцируемый базисом кватерниона.

LaTeX

$$$\exists \varphi: \mathbb{H}_{R}(c_{1},0,c_{2}) \to_R \mathrm{CliffordAlg}(Q\;c_{1}\;c_{2})\;\text{ such that }\varphi\text{ is an }R\text{-algebra hom}$$$

Lean4

/-- Map a quaternion into the clifford algebra. -/
def ofQuaternion : ℍ[R,c₁,0,c₂] →ₐ[R] CliffordAlgebra (Q c₁ c₂) :=
  (quaternionBasis c₁ c₂).liftHom

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