mathlib documentation

algebra.quaternion_basis

Basis on a quaternion-like algebra #

Main definitions #

structure quaternion_algebra.basis {R : Type u_1} (A : Type u_2) [comm_ring R] [ring A] [algebra R 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] [algebra R A] {c₁ c₂ : R} ⦃q₁ q₂ : quaternion_algebra.basis A c₁ 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} :
(quaternion_algebra.basis.self R).i = {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} :

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} :
(quaternion_algebra.basis.self R).j = {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} :
(quaternion_algebra.basis.self R).k = {re := 0, im_i := 0, im_j := 0, im_k := 1}
@[simp]
theorem quaternion_algebra.basis.i_mul_k {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [algebra R A] {c₁ c₂ : R} (q : quaternion_algebra.basis A c₁ 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] [algebra R A] {c₁ c₂ : R} (q : quaternion_algebra.basis A c₁ 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] [algebra R A] {c₁ c₂ : R} (q : quaternion_algebra.basis A c₁ 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] [algebra R A] {c₁ c₂ : R} (q : quaternion_algebra.basis A c₁ 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] [algebra R A] {c₁ c₂ : R} (q : quaternion_algebra.basis A c₁ 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] [algebra R A] {c₁ c₂ : R} (q : quaternion_algebra.basis A c₁ 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] [algebra R A] {c₁ c₂ : R} (q : quaternion_algebra.basis A c₁ c₂) :
q.lift 0 = 0
theorem quaternion_algebra.basis.lift_one {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [algebra R A] {c₁ c₂ : R} (q : quaternion_algebra.basis A c₁ c₂) :
q.lift 1 = 1
theorem quaternion_algebra.basis.lift_add {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [algebra R A] {c₁ c₂ : R} (q : quaternion_algebra.basis A c₁ 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] [algebra R A] {c₁ c₂ : R} (q : quaternion_algebra.basis A c₁ 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] [algebra R A] {c₁ c₂ : R} (q : quaternion_algebra.basis A c₁ 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] [algebra R A] {c₁ c₂ : R} (q : quaternion_algebra.basis A c₁ 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] [algebra R A] {c₁ c₂ : R} (q : quaternion_algebra.basis A c₁ 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] [algebra R A] [algebra R B] {c₁ c₂ : R} (q : quaternion_algebra.basis A c₁ c₂) (F : A →ₐ[R] B) :

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] [algebra R A] [algebra R B] {c₁ c₂ : R} (q : quaternion_algebra.basis A c₁ 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] [algebra R A] [algebra R B] {c₁ c₂ : R} (q : quaternion_algebra.basis A c₁ 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] [algebra R A] [algebra R B] {c₁ c₂ : R} (q : quaternion_algebra.basis A c₁ 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] [algebra R A] {c₁ c₂ : R} (q : quaternion_algebra.basis A c₁ c₂) :
def quaternion_algebra.lift {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [algebra R A] {c₁ c₂ : R} :
quaternion_algebra.basis A c₁ 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] [algebra R A] {c₁ c₂ : R} (F : ℍ[R,c₁,c₂] →ₐ[R] A) :