mathlib3 documentation

algebra.quaternion_basis

Basis on a quaternion-like algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

Instances for quaternion_algebra.basis
@[protected, 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}
@[protected]
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}
@[protected, instance]
def quaternion_algebra.basis.inhabited {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
Equations
@[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 : quaternion_algebra 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 : quaternion_algebra 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 : quaternion_algebra 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 : quaternion_algebra 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₂) (ᾰ : quaternion_algebra 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₂) :

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} :

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 : quaternion_algebra R c₁ c₂ →ₐ[R] A) :