Basis on a quaternion-like algebra #
Main definitions #
QuaternionAlgebra.Basis A c₁ c₂
: a basis for a subspace of anR
-algebraA
that has the same algebra structure asℍ[R,c₁,c₂]
.QuaternionAlgebra.Basis.self R
: the canonical basis forℍ[R,c₁,c₂]
.QuaternionAlgebra.Basis.compHom b f
: transform a basisb
by an AlgHomf
.QuaternionAlgebra.lift
: Define anAlgHom
out ofℍ[R,c₁,c₂]
by its action on the basis elementsi
,j
, andk
. In essence, this is a universal property. Analogous toComplex.lift
, but takes a bundledQuaternionAlgebra.Basis
instead of just aSubtype
as the amount of data / proves is non-negligible.
- i : A
- j : A
- k : A
A quaternion basis contains the information both sufficient and necessary to construct an
R
-algebra homomorphism from ℍ[R,c₁,c₂]
to A
; or equivalently, a surjective
R
-algebra homomorphism from ℍ[R,c₁,c₂]
to an R
-subalgebra of A
.
Note that for definitional convenience, k
is provided as a field even though i_mul_j
fully
determines it.
Instances For
Since k
is redundant, it is not necessary to show q₁.k = q₂.k
when showing q₁ = q₂
.
There is a natural quaternionic basis for the QuaternionAlgebra
.
Instances For
Intermediate result used to define QuaternionAlgebra.Basis.liftHom
.
Instances For
A QuaternionAlgebra.Basis
implies an AlgHom
from the quaternions.
Instances For
Transform a QuaternionAlgebra.Basis
through an AlgHom
.
Instances For
A quaternionic basis on A
is equivalent to a map from the quaternion algebra to A
.