mathlib documentation

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] [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

quaternion_algebra.basis.has_sizeof_inst
quaternion_algebra.basis.inhabited

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

quaternion_algebra.basis (quaternion_algebra R c₁ c₂) c₁ c₂

There is a natural quaternionic basis for the quaternion_algebra.

Equations

quaternion_algebra.basis.self R = {i := {re := 0, im_i := 1, im_j := 0, im_k := 0}, j := {re := 0, im_i := 0, im_j := 1, im_k := 0}, k := {re := 0, im_i := 0, im_j := 0, im_k := 1}, i_mul_i := _, j_mul_j := _, i_mul_j := _, j_mul_i := _}

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

inhabited (quaternion_algebra.basis (quaternion_algebra R c₁ c₂) c₁ c₂)

Equations

quaternion_algebra.basis.inhabited = {default := quaternion_algebra.basis.self R c₂}

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

q.lift x = ⇑(algebra_map R A) x.re + x.im_i • q.i + x.im_j • q.j + x.im_k • q.k

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₂) :

quaternion_algebra R c₁ c₂ →ₐ[R] A

A quaternion_algebra.basis implies an alg_hom from the quaternions.

Equations

q.lift_hom = alg_hom.mk' {to_fun := q.lift, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _} _

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

quaternion_algebra.basis B c₁ c₂

Transform a quaternion_algebra.basis through an alg_hom.

Equations

q.comp_hom 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 := _}

@[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₂) :

⇑quaternion_algebra.lift q = q.lift_hom

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

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

Equations

quaternion_algebra.lift = {to_fun := quaternion_algebra.basis.lift_hom c₂, inv_fun := (quaternion_algebra.basis.self R).comp_hom, left_inv := _, right_inv := _}

@[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) :

⇑(quaternion_algebra.lift.symm) F = (quaternion_algebra.basis.self R).comp_hom F