# mathlibdocumentation

algebra.quaternion_basis

# Basis on a quaternion-like algebra #

## Main definitions #

• quaternion_algebra.basis A c₁ c₂: a basis for a subspace of an R-algebra A 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 basis b by an alg_hom f.
• quaternion_algebra.lift: Define an alg_hom 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 quaternion_algebra.basis instead of just a subtype as the amount of data / proves is non-negligeable.
structure quaternion_algebra.basis {R : Type u_1} (A : Type u_2) [comm_ring R] [ring A] [ A] (c₁ c₂ : R) :
Type u_2
• 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.

@[ext]
theorem quaternion_algebra.basis.ext {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] {c₁ c₂ : R} ⦃q₁ q₂ : c₂⦄ (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 quaternion_algebra.basis.self_i (R : Type u_1) [comm_ring R] {c₁ c₂ : R} :
= {re := 0, im_i := 1, im_j := 0, im_k := 0}
def quaternion_algebra.basis.self (R : Type u_1) [comm_ring R] {c₁ c₂ : R} :
c₁ c₂

There is a natural quaternionic basis for the quaternion_algebra.

Equations
@[simp]
theorem quaternion_algebra.basis.self_j (R : Type u_1) [comm_ring R] {c₁ c₂ : R} :
= {re := 0, im_i := 0, im_j := 1, im_k := 0}
@[simp]
theorem quaternion_algebra.basis.self_k (R : Type u_1) [comm_ring R] {c₁ c₂ : R} :
= {re := 0, im_i := 0, im_j := 0, im_k := 1}
@[instance]
def quaternion_algebra.basis.inhabited {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
inhabited c₁ c₂)
Equations
@[simp]
theorem quaternion_algebra.basis.i_mul_k {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] {c₁ c₂ : R} (q : c₂) :
(q.i) * q.k = c₁ q.j
@[simp]
theorem quaternion_algebra.basis.k_mul_i {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] {c₁ c₂ : R} (q : c₂) :
(q.k) * q.i = -c₁ q.j
@[simp]
theorem quaternion_algebra.basis.k_mul_j {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] {c₁ c₂ : R} (q : c₂) :
(q.k) * q.j = c₂ q.i
@[simp]
theorem quaternion_algebra.basis.j_mul_k {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] {c₁ c₂ : R} (q : c₂) :
(q.j) * q.k = -c₂ q.i
@[simp]
theorem quaternion_algebra.basis.k_mul_k {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] {c₁ c₂ : R} (q : c₂) :
(q.k) * q.k = -((c₁ * c₂) 1)
def quaternion_algebra.basis.lift {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] {c₁ c₂ : R} (q : c₂) (x : ℍ[R,c₁,c₂]) :
A

Intermediate result used to define quaternion_algebra.basis.lift_hom.

Equations
theorem quaternion_algebra.basis.lift_zero {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] {c₁ c₂ : R} (q : c₂) :
q.lift 0 = 0
theorem quaternion_algebra.basis.lift_one {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] {c₁ c₂ : R} (q : c₂) :
q.lift 1 = 1
theorem quaternion_algebra.basis.lift_add {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] {c₁ c₂ : R} (q : c₂) (x y : ℍ[R,c₁,c₂]) :
q.lift (x + y) = q.lift x + q.lift y
theorem quaternion_algebra.basis.lift_mul {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] {c₁ c₂ : R} (q : c₂) (x y : ℍ[R,c₁,c₂]) :
q.lift (x * y) = (q.lift x) * q.lift y
theorem quaternion_algebra.basis.lift_smul {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] {c₁ c₂ : R} (q : c₂) (r : R) (x : ℍ[R,c₁,c₂]) :
q.lift (r x) = r q.lift x
@[simp]
theorem quaternion_algebra.basis.lift_hom_apply {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] {c₁ c₂ : R} (q : c₂) (ᾰ : ℍ[R,c₁,c₂]) :
(q.lift_hom) ᾰ = q.lift
def quaternion_algebra.basis.lift_hom {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] {c₁ c₂ : R} (q : c₂) :
ℍ[R,c₁,c₂] →ₐ[R] A

A quaternion_algebra.basis implies an alg_hom from the quaternions.

Equations
def quaternion_algebra.basis.comp_hom {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [ring A] [ring B] [ A] [ B] {c₁ c₂ : R} (q : c₂) (F : A →ₐ[R] B) :
c₂

Transform a quaternion_algebra.basis through an alg_hom.

Equations
@[simp]
theorem quaternion_algebra.basis.comp_hom_k {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [ring A] [ring B] [ A] [ B] {c₁ c₂ : R} (q : c₂) (F : A →ₐ[R] B) :
(q.comp_hom F).k = F q.k
@[simp]
theorem quaternion_algebra.basis.comp_hom_i {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [ring A] [ring B] [ A] [ B] {c₁ c₂ : R} (q : c₂) (F : A →ₐ[R] B) :
(q.comp_hom F).i = F q.i
@[simp]
theorem quaternion_algebra.basis.comp_hom_j {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [ring A] [ring B] [ A] [ B] {c₁ c₂ : R} (q : c₂) (F : A →ₐ[R] B) :
(q.comp_hom F).j = F q.j
@[simp]
theorem quaternion_algebra.lift_apply {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] {c₁ c₂ : R} (q : c₂) :
def quaternion_algebra.lift {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] {c₁ c₂ : R} :
c₂ (ℍ[R,c₁,c₂] →ₐ[R] A)

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

Equations
@[simp]
theorem quaternion_algebra.lift_symm_apply {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] {c₁ c₂ : R} (F : ℍ[R,c₁,c₂] →ₐ[R] A) :