English
There is a canonical way to map the quaternion algebra to any algebra A using a given basis q, producing a homomorphism that respects the quaternion relations.
Русский
Существует канонический способ сопоставить кватернионную алгебру произвольному A через данный базис q, образующий гомоморфизм, сохраняющий кватернионные соотношения.
LaTeX
$$$\\text{lift}: \\mathbb{H}(R,c_1,c_2,c_3) \\to A \\quad \\text{is defined by} \\quad \\text{lift}(x) = \\mathrm{algebraMap}_{R,A}(x_{\\text{re}}) + x_{\\text{imI}} \\cdot q.i + x_{\\text{imJ}} \\cdot q.j + x_{\\text{imK}} \\cdot q.k$$$
Lean4
/-- Intermediate result used to define `QuaternionAlgebra.Basis.liftHom`. -/
def lift (x : ℍ[R,c₁,c₂,c₃]) : A :=
algebraMap R _ x.re + x.imI • q.i + x.imJ • q.j + x.imK • q.k
