# Documentation

Mathlib.Algebra.QuaternionBasis

# 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
• i : A
• j : A
• k : A
• i_mul_i : s.i * s.i = c₁ 1
• j_mul_j : s.j * s.j = c₂ 1
• i_mul_j : s.i * s.j = s.k
• j_mul_i : s.j * s.i = -s.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
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.

Instances For
@[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.

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 : ) :
theorem QuaternionAlgebra.Basis.lift_one {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : ) :
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₂) :
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₂) :
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₂) :
=
@[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₂) :
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.

Instances For
@[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) :
().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) :
().j = F q.j
@[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) :
().i = F q.i
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.

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 =
@[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 =
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.

Instances For