A quaternion curve with scalar squares

In the quaternions ℍ[R] over a commutative ring, the three pure quaternions ξ = t i, η = t j, ζ = t k square to the scalar −t² and anticommute pairwise.

Main results

• xi_mul_self, eta_mul_self, zeta_mul_self: ξ² = η² = ζ² = −t².
• xi_mul_eta_add, eta_mul_zeta_add, zeta_mul_xi_add: ξ η + η ξ = 0 and the other two pairs.

def ThreeAxes.QuaternionCurve.xi {R : Type u_1} [CommRing R] (t : R) : Quaternion R

ξ = t i.

Equations

• ThreeAxes.QuaternionCurve.xi t = { re := 0, imI := t, imJ := 0, imK := 0 }

def ThreeAxes.QuaternionCurve.eta {R : Type u_1} [CommRing R] (t : R) : Quaternion R

η = t j.

Equations

• ThreeAxes.QuaternionCurve.eta t = { re := 0, imI := 0, imJ := t, imK := 0 }

def ThreeAxes.QuaternionCurve.zeta {R : Type u_1} [CommRing R] (t : R) : Quaternion R

ζ = t k.

Equations

• ThreeAxes.QuaternionCurve.zeta t = { re := 0, imI := 0, imJ := 0, imK := t }

theorem ThreeAxes.QuaternionCurve.xi_mul_self {R : Type u_1} [CommRing R] (t : R) : xi t * xi t = ↑(-t ^ 2)

theorem ThreeAxes.QuaternionCurve.eta_mul_self {R : Type u_1} [CommRing R] (t : R) : eta t * eta t = ↑(-t ^ 2)

theorem ThreeAxes.QuaternionCurve.zeta_mul_self {R : Type u_1} [CommRing R] (t : R) : zeta t * zeta t = ↑(-t ^ 2)

theorem ThreeAxes.QuaternionCurve.xi_mul_eta_add {R : Type u_1} [CommRing R] (t : R) : xi t * eta t + eta t * xi t = 0

theorem ThreeAxes.QuaternionCurve.eta_mul_zeta_add {R : Type u_1} [CommRing R] (t : R) : eta t * zeta t + zeta t * eta t = 0

theorem ThreeAxes.QuaternionCurve.zeta_mul_xi_add {R : Type u_1} [CommRing R] (t : R) : zeta t * xi t + xi t * zeta t = 0