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

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.

• 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

@[simp]

theorem QuaternionAlgebra.Basis.i_mul_i {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (self : QuaternionAlgebra.Basis A c₁ c₂) : self.i * self.i = c₁ • 1

@[simp]

theorem QuaternionAlgebra.Basis.j_mul_j {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ : R} {c₂ : R} (self : QuaternionAlgebra.Basis A c₁ c₂) : self.j * self.j = c₂ • 1

@[simp]

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

@[simp]

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

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• QuaternionAlgebra.Basis.instInhabited = { default := QuaternionAlgebra.Basis.self R }

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

Equations

• q.lift x = (algebraMap R A) x.re + x.imI • q.i + x.imJ • q.j + x.imK • q.k

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₂) : q.lift 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₂) : q.lift 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₂) : q.lift (x + y) = q.lift x + q.lift 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₂) : q.lift (x * y) = q.lift x * q.lift 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₂) : q.lift (r • x) = r • q.lift 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₂) : q.liftHom a = q.lift 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.

Equations

• q.liftHom = AlgHom.mk' { toFun := q.lift, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } ⋯

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

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

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.

Equations

• q.compHom 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 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 = q.liftHom

@[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.self R).compHom 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.

Equations

• QuaternionAlgebra.lift = { toFun := QuaternionAlgebra.Basis.liftHom, invFun := (QuaternionAlgebra.Basis.self R).compHom, left_inv := ⋯, right_inv := ⋯ }

theorem QuaternionAlgebra.hom_ext {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⦄ ⦃g : QuaternionAlgebra R c₁ c₂ →ₐ[R] A⦄ (hi : f (QuaternionAlgebra.Basis.self R).i = g (QuaternionAlgebra.Basis.self R).i) (hj : f (QuaternionAlgebra.Basis.self R).j = g (QuaternionAlgebra.Basis.self R).j) : f = g

Two R-algebra morphisms from a quaternion algebra are equal if they agree on i and j.

theorem Quaternion.hom_ext {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] ⦃f : Quaternion R →ₐ[R] A⦄ ⦃g : Quaternion R →ₐ[R] A⦄ (hi : f (QuaternionAlgebra.Basis.self R).i = g (QuaternionAlgebra.Basis.self R).i) (hj : f (QuaternionAlgebra.Basis.self R).j = g (QuaternionAlgebra.Basis.self R).j) : f = g

Two R-algebra morphisms from the quaternions are equal if they agree on i and j.