# Basis on a quaternion-like algebra #

## Main definitions #

• QuaternionAlgebra.Basis A c₁ c₂: a basis for a subspace of an R-algebra A 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 basis b by an AlgHom f.
• QuaternionAlgebra.lift: Define an AlgHom out of ℍ[R,c₁,c₂] by its action on the basis elements i, j, and k. In essence, this is a universal property. Analogous to Complex.lift, but takes a bundled QuaternionAlgebra.Basis instead of just a Subtype as the amount of data / proves is non-negligible.
structure QuaternionAlgebra.Basis {R : Type u_1} (A : Type u_2) [] [Ring A] [Algebra R A] (c₁ : R) (c₂ : R) :
Type u_2

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.

• 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
Instances For
@[simp]
theorem QuaternionAlgebra.Basis.i_mul_i {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (self : ) :
self.i * self.i = c₁ 1
@[simp]
theorem QuaternionAlgebra.Basis.j_mul_j {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (self : ) :
self.j * self.j = c₂ 1
@[simp]
theorem QuaternionAlgebra.Basis.i_mul_j {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (self : ) :
self.i * self.j = self.k
@[simp]
theorem QuaternionAlgebra.Basis.j_mul_i {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (self : ) :
self.j * self.i = -self.k
theorem QuaternionAlgebra.Basis.ext {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} ⦃q₁ : ⦃q₂ : (hi : q₁.i = q₂.i) (hj : q₁.j = q₂.j) :
q₁ = q₂

Since k is redundant, it is not necessary to show q₁.k = q₂.k when showing q₁ = q₂.

@[simp]
theorem QuaternionAlgebra.Basis.self_j (R : Type u_1) [] {c₁ : R} {c₂ : R} :
= { re := 0, imI := 0, imJ := 1, imK := 0 }
@[simp]
theorem QuaternionAlgebra.Basis.self_i (R : Type u_1) [] {c₁ : R} {c₂ : R} :
= { re := 0, imI := 1, imJ := 0, imK := 0 }
@[simp]
theorem QuaternionAlgebra.Basis.self_k (R : Type u_1) [] {c₁ : R} {c₂ : R} :
= { re := 0, imI := 0, imJ := 0, imK := 1 }
def QuaternionAlgebra.Basis.self (R : Type u_1) [] {c₁ : R} {c₂ : R} :

There is a natural quaternionic basis for the QuaternionAlgebra.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance QuaternionAlgebra.Basis.instInhabited {R : Type u_1} [] {c₁ : R} {c₂ : R} :
Equations
• QuaternionAlgebra.Basis.instInhabited = { default := }
@[simp]
theorem QuaternionAlgebra.Basis.i_mul_k {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : ) :
q.i * q.k = c₁ q.j
@[simp]
theorem QuaternionAlgebra.Basis.k_mul_i {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : ) :
q.k * q.i = -c₁ q.j
@[simp]
theorem QuaternionAlgebra.Basis.k_mul_j {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : ) :
q.k * q.j = c₂ q.i
@[simp]
theorem QuaternionAlgebra.Basis.j_mul_k {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : ) :
q.j * q.k = -c₂ q.i
@[simp]
theorem QuaternionAlgebra.Basis.k_mul_k {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : ) :
q.k * q.k = -((c₁ * c₂) 1)
def QuaternionAlgebra.Basis.lift {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : ) (x : QuaternionAlgebra R c₁ c₂) :
A

Intermediate result used to define QuaternionAlgebra.Basis.liftHom.

Equations
• q.lift x = () x.re + x.imI q.i + x.imJ q.j + x.imK q.k
Instances For
theorem QuaternionAlgebra.Basis.lift_zero {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : ) :
q.lift 0 = 0
theorem QuaternionAlgebra.Basis.lift_one {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : ) :
q.lift 1 = 1
theorem QuaternionAlgebra.Basis.lift_add {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : ) (x : QuaternionAlgebra R c₁ c₂) (y : QuaternionAlgebra R c₁ c₂) :
q.lift (x + y) = q.lift x + q.lift y
theorem QuaternionAlgebra.Basis.lift_mul {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : ) (x : QuaternionAlgebra R c₁ c₂) (y : QuaternionAlgebra R c₁ c₂) :
q.lift (x * y) = q.lift x * q.lift y
theorem QuaternionAlgebra.Basis.lift_smul {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : ) (r : R) (x : QuaternionAlgebra R c₁ c₂) :
q.lift (r x) = r q.lift x
@[simp]
theorem QuaternionAlgebra.Basis.liftHom_apply {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : ) (a : QuaternionAlgebra R c₁ c₂) :
q.liftHom a = q.lift a
def QuaternionAlgebra.Basis.liftHom {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : ) :

A QuaternionAlgebra.Basis implies an AlgHom from the quaternions.

Equations
• q.liftHom = AlgHom.mk' { toFun := q.lift, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem QuaternionAlgebra.Basis.compHom_i {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {c₁ : R} {c₂ : R} (q : ) (F : A →ₐ[R] B) :
(q.compHom F).i = F q.i
@[simp]
theorem QuaternionAlgebra.Basis.compHom_k {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {c₁ : R} {c₂ : R} (q : ) (F : A →ₐ[R] B) :
(q.compHom F).k = F q.k
@[simp]
theorem QuaternionAlgebra.Basis.compHom_j {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {c₁ : R} {c₂ : R} (q : ) (F : A →ₐ[R] B) :
(q.compHom F).j = F q.j
def QuaternionAlgebra.Basis.compHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {c₁ : R} {c₂ : R} (q : ) (F : A →ₐ[R] B) :

Transform a QuaternionAlgebra.Basis through an AlgHom.

Equations
• q.compHom F = { i := F q.i, j := F q.j, k := F q.k, i_mul_i := , j_mul_j := , i_mul_j := , j_mul_i := }
Instances For
@[simp]
theorem QuaternionAlgebra.lift_apply {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : ) :
QuaternionAlgebra.lift q = q.liftHom
@[simp]
theorem QuaternionAlgebra.lift_symm_apply {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (F : QuaternionAlgebra R c₁ c₂ →ₐ[R] A) :
QuaternionAlgebra.lift.symm F = .compHom F
def QuaternionAlgebra.lift {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} :
(QuaternionAlgebra R c₁ c₂ →ₐ[R] A)

A quaternionic basis on A is equivalent to a map from the quaternion algebra to A.

Equations
• QuaternionAlgebra.lift = { toFun := QuaternionAlgebra.Basis.liftHom, invFun := .compHom, left_inv := , right_inv := }
Instances For
theorem QuaternionAlgebra.hom_ext {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} ⦃f : QuaternionAlgebra R c₁ c₂ →ₐ[R] A ⦃g : QuaternionAlgebra R c₁ c₂ →ₐ[R] A (hi : f = g ) (hj : f = g ) :
f = g

Two R-algebra morphisms from a quaternion algebra are equal if they agree on i and j.

theorem Quaternion.hom_ext {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] ⦃f : →ₐ[R] A ⦃g : →ₐ[R] A (hi : f = g ) (hj : f = g ) :
f = g

Two R-algebra morphisms from the quaternions are equal if they agree on i and j.