Basis on a quaternion-like algebra

Main definitions

• QuaternionAlgebra.Basis A c₁ c₂ c₃: a basis for a subspace of an R-algebra A that has the same algebra structure as ℍ[R,c₁,c₂,c₃].
• QuaternionAlgebra.Basis.self R: the canonical basis for ℍ[R,c₁,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₂,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₁ c₂ 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₂,c₃] to A; or equivalently, a surjective R-algebra homomorphism from ℍ[R,c₁,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

  The first imaginary unit

• j : A

  The second imaginary unit

• k : A

  The third imaginary unit

• i_mul_i : self.i * self.i = c₁ • 1 + c₂ • self.i
• 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 = c₂ • self.j - self.k

theorem QuaternionAlgebra.Basis.ext {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} ⦃q₁ q₂ : Basis A c₁ 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₂.

theorem QuaternionAlgebra.Basis.ext_iff {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} {q₁ q₂ : Basis A c₁ c₂ c₃} : q₁ = q₂ ↔ q₁.i = q₂.i ∧ q₁.j = q₂.j

def QuaternionAlgebra.Basis.self (R : Type u_1) [CommRing R] {c₁ c₂ c₃ : R} : Basis (QuaternionAlgebra R c₁ c₂ 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.

@[simp]

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

@[simp]

theorem QuaternionAlgebra.Basis.self_j (R : Type u_1) [CommRing R] {c₁ c₂ c₃ : R} : (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₁ c₂ c₃ : R} : (Basis.self R).i = { re := 0, imI := 1, imJ := 0, imK := 0 }

instance QuaternionAlgebra.Basis.instInhabited {R : Type u_1} [CommRing R] {c₁ c₂ c₃ : R} : Inhabited (Basis (QuaternionAlgebra R c₁ c₂ 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₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) : q.i * q.k = c₁ • q.j + c₂ • q.k

@[simp]

theorem QuaternionAlgebra.Basis.k_mul_i {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} (q : Basis A c₁ 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₁ c₂ c₃ : R} (q : Basis A c₁ 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₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) : q.j * q.k = (c₂ * c₃) • 1 - 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₁ c₂ c₃ : R} (q : Basis A c₁ 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₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) (x : QuaternionAlgebra R c₁ 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₁ c₂ c₃ : R} (q : Basis A c₁ 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₁ c₂ c₃ : R} (q : Basis A c₁ 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₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) (x y : QuaternionAlgebra R c₁ 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₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) (x y : QuaternionAlgebra R c₁ 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₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) (r : R) (x : QuaternionAlgebra R c₁ c₂ c₃) : q.lift (r • x) = r • q.lift x

def QuaternionAlgebra.Basis.liftHom {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) : QuaternionAlgebra R c₁ 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.liftHom_apply {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) (a : QuaternionAlgebra R c₁ c₂ c₃) : q.liftHom a = q.lift a

@[simp]

theorem QuaternionAlgebra.Basis.range_liftHom {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} (B : Basis A c₁ c₂ c₃) : B.liftHom.range = Algebra.adjoin R {B.i, B.j, B.k}

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₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) (F : A →ₐ[R] B) : Basis B c₁ 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.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₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) (F : A →ₐ[R] B) : (q.compHom F).i = F q.i

@[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₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) (F : A →ₐ[R] B) : (q.compHom F).j = F q.j

@[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₁ c₂ c₃ : R} (q : Basis A c₁ c₂ c₃) (F : A →ₐ[R] B) : (q.compHom F).k = F q.k

def QuaternionAlgebra.lift {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} : Basis A c₁ c₂ c₃ ≃ (QuaternionAlgebra R c₁ 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 := ⋯ }

@[simp]

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

@[simp]

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

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

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

theorem QuaternionAlgebra.hom_ext_iff {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {c₁ c₂ c₃ : R} {f g : QuaternionAlgebra R c₁ c₂ c₃ →ₐ[R] A} : f = g ↔ f (Basis.self R).i = g (Basis.self R).i ∧ f (Basis.self R).j = g (Basis.self R).j

theorem Quaternion.hom_ext {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] ⦃f 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.

theorem Quaternion.hom_ext_iff {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {f g : Quaternion R →ₐ[R] A} : f = g ↔ f (QuaternionAlgebra.Basis.self R).i = g (QuaternionAlgebra.Basis.self R).i ∧ f (QuaternionAlgebra.Basis.self R).j = g (QuaternionAlgebra.Basis.self R).j