Basis on a quaternion-like algebra #
Main definitions #
quaternion_algebra.basis A c₁ c₂
: a basis for a subspace of anR
-algebraA
that has the same algebra structure asℍ[R,c₁,c₂]
.quaternion_algebra.basis.self R
: the canonical basis forℍ[R,c₁,c₂]
.quaternion_algebra.basis.comp_hom b f
: transform a basisb
by an alg_homf
.quaternion_algebra.lift
: Define analg_hom
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 bundledquaternion_algebra.basis
instead of just asubtype
as the amount of data / proves is non-negligeable.
- i : A
- j : A
- k : A
- i_mul_i : self.i * self.i = c₁ • 1
- j_mul_j : self.j * self.j = c₂ • 1
- i_mul_j : self.i * self.j = self.k
- j_mul_i : self.j * self.i = -self.k
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 quaternion_algebra.basis
- quaternion_algebra.basis.has_sizeof_inst
- quaternion_algebra.basis.inhabited
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 quaternion_algebra
.
Equations
Intermediate result used to define quaternion_algebra.basis.lift_hom
.
A quaternion_algebra.basis
implies an alg_hom
from the quaternions.
Transform a quaternion_algebra.basis
through an alg_hom
.
A quaternionic basis on A
is equivalent to a map from the quaternion algebra to A
.
Equations
- quaternion_algebra.lift = {to_fun := quaternion_algebra.basis.lift_hom c₂, inv_fun := (quaternion_algebra.basis.self R).comp_hom, left_inv := _, right_inv := _}