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) [CommRing R] [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.

theorem QuaternionAlgebra.Basis.ext {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} ⦃q₁ : QuaternionAlgebra.Basis A c₁ c₂⦄ ⦃q₂ : QuaternionAlgebra.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 QuaternionAlgebra.Basis.self_j (R : Type u_1) [CommRing R] {c₁ : R} {c₂ : R} : (QuaternionAlgebra.Basis.self R).j = { re := 0, imI := 0, imJ := 1, imK := 0 }

@[simp]

theorem QuaternionAlgebra.Basis.self_i (R : Type u_1) [CommRing R] {c₁ : R} {c₂ : R} : (QuaternionAlgebra.Basis.self R).i = { re := 0, imI := 1, imJ := 0, imK := 0 }

@[simp]

theorem QuaternionAlgebra.Basis.self_k (R : Type u_1) [CommRing R] {c₁ : R} {c₂ : R} : (QuaternionAlgebra.Basis.self R).k = { re := 0, imI := 0, imJ := 0, imK := 1 }

def QuaternionAlgebra.Basis.self (R : Type u_1) [CommRing R] {c₁ : R} {c₂ : R} : QuaternionAlgebra.Basis (QuaternionAlgebra R c₁ c₂) c₁ c₂

There is a natural quaternionic basis for the QuaternionAlgebra.

instance QuaternionAlgebra.Basis.instInhabitedBasisQuaternionAlgebraInstRingInstAlgebraQuaternionAlgebraToSemiringInstRingToCommSemiringId {R : Type u_1} [CommRing R] {c₁ : R} {c₂ : R} : Inhabited (QuaternionAlgebra.Basis (QuaternionAlgebra R c₁ c₂) c₁ c₂)

@[simp]

theorem QuaternionAlgebra.Basis.i_mul_k {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) : q.i * q.k = c₁ • q.j

@[simp]

theorem QuaternionAlgebra.Basis.k_mul_i {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) : q.k * q.i = -c₁ • q.j

@[simp]

theorem QuaternionAlgebra.Basis.k_mul_j {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) : q.k * q.j = c₂ • q.i

@[simp]

theorem QuaternionAlgebra.Basis.j_mul_k {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) : q.j * q.k = -c₂ • q.i

@[simp]

theorem QuaternionAlgebra.Basis.k_mul_k {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) : q.k * q.k = -((c₁ * c₂) • 1)

def QuaternionAlgebra.Basis.lift {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) (x : QuaternionAlgebra R c₁ c₂) : A

Intermediate result used to define QuaternionAlgebra.Basis.liftHom.

theorem QuaternionAlgebra.Basis.lift_zero {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) : QuaternionAlgebra.Basis.lift q 0 = 0

theorem QuaternionAlgebra.Basis.lift_one {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) : QuaternionAlgebra.Basis.lift q 1 = 1

theorem QuaternionAlgebra.Basis.lift_add {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) (x : QuaternionAlgebra R c₁ c₂) (y : QuaternionAlgebra R c₁ c₂) : QuaternionAlgebra.Basis.lift q (x + y) = QuaternionAlgebra.Basis.lift q x + QuaternionAlgebra.Basis.lift q y

theorem QuaternionAlgebra.Basis.lift_mul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) (x : QuaternionAlgebra R c₁ c₂) (y : QuaternionAlgebra R c₁ c₂) : QuaternionAlgebra.Basis.lift q (x * y) = QuaternionAlgebra.Basis.lift q x * QuaternionAlgebra.Basis.lift q y

theorem QuaternionAlgebra.Basis.lift_smul {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) (r : R) (x : QuaternionAlgebra R c₁ c₂) : QuaternionAlgebra.Basis.lift q (r • x) = r • QuaternionAlgebra.Basis.lift q x

@[simp]

theorem QuaternionAlgebra.Basis.liftHom_apply {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) (a : QuaternionAlgebra R c₁ c₂) : ↑(QuaternionAlgebra.Basis.liftHom q) a = QuaternionAlgebra.Basis.lift q a

def QuaternionAlgebra.Basis.liftHom {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) : QuaternionAlgebra R c₁ c₂ →ₐ[R] A

A QuaternionAlgebra.Basis implies an AlgHom from the quaternions.

@[simp]

theorem QuaternionAlgebra.Basis.compHom_k {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) (F : A →ₐ[R] B) : (QuaternionAlgebra.Basis.compHom q F).k = ↑F q.k

@[simp]

theorem QuaternionAlgebra.Basis.compHom_j {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) (F : A →ₐ[R] B) : (QuaternionAlgebra.Basis.compHom q F).j = ↑F q.j

@[simp]

theorem QuaternionAlgebra.Basis.compHom_i {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) (F : A →ₐ[R] B) : (QuaternionAlgebra.Basis.compHom q F).i = ↑F q.i

def QuaternionAlgebra.Basis.compHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) (F : A →ₐ[R] B) : QuaternionAlgebra.Basis B c₁ c₂

Transform a QuaternionAlgebra.Basis through an AlgHom.

@[simp]

theorem QuaternionAlgebra.lift_apply {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (q : QuaternionAlgebra.Basis A c₁ c₂) : ↑QuaternionAlgebra.lift q = QuaternionAlgebra.Basis.liftHom q

@[simp]

theorem QuaternionAlgebra.lift_symm_apply {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (F : QuaternionAlgebra R c₁ c₂ →ₐ[R] A) : ↑QuaternionAlgebra.lift.symm F = QuaternionAlgebra.Basis.compHom (QuaternionAlgebra.Basis.self R) F

def QuaternionAlgebra.lift {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} : QuaternionAlgebra.Basis A c₁ c₂ ≃ (QuaternionAlgebra R c₁ c₂ →ₐ[R] A)

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