liftHom — Mathlib

English

There is an R-algebra homomorphism from the quaternion algebra to A associated to a basis B, called liftHom.

Русский

Существует R-алгебра-гомоморфизм из кватернионной алгебры в A, соответствующий базису B, называемый liftHom.

LaTeX

$$$\\text{liftHom} : \\mathbb{H}(R,c_1,c_2,c_3) \\to_{R} A$$$

Lean4

/-- A `QuaternionAlgebra.Basis` implies an `AlgHom` from the quaternions. -/
@[simps!]
def liftHom : ℍ[R,c₁,c₂,c₃] →ₐ[R] A :=
  AlgHom.mk'
    { toFun := q.lift
      map_zero' := q.lift_zero
      map_one' := q.lift_one
      map_add' := q.lift_add
      map_mul' := q.lift_mul } q.lift_smul

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