The 2 × 2 representation Θ of the quaternion curve

Over a commutative ring R with an element ι, ι² = −1 (in the paper R = ℂ[t], ι = √−1), let 𝐢 = diag(ι, −ι), 𝐣 = !![0,1;−1,0], 𝐤 = 𝐢𝐣. The map Θ of §4.2 sends the generators to I + t𝐢, I + t𝐣, I + t𝐤, so ξ = x − 1, η = y − 1, ζ = z − 1 go to t𝐢, t𝐣, t𝐤.

Main results

• mi_mul_mi, mj_mul_mj, mk_mul_mk, mi_mul_mj, mj_mul_mi: the quaternion relations.
• smul_mul_smul_self: if q² = −1, then (t q)² = −t² I (so ξ² = η² = ζ² = −t² I under Θ).
• theta_c_eq_zero: c = ξη + ηξ ↦ t²(𝐢𝐣 + 𝐣𝐢) = 0.
• det_one_add_smul: det(I + t q) = 1 + t² for q ∈ {𝐢, 𝐣, 𝐤}.
• one_add_smul_mul_one_sub_smul, one_sub_smul_mul_one_add_smul: (I + t q)(I − t q) = (1 + t²) I in both orders, so Θ(x)⁻¹ = (I − t𝐢)/(1 + t²) wherever 1 + t² is invertible.

def ThreeAxes.QuaternionTheta.mi {R : Type u_1} [CommRing R] (ι : R) : Matrix (Fin 2) (Fin 2) R

𝐢 = diag(ι, −ι).

Equations

• ThreeAxes.QuaternionTheta.mi ι = !![ι, 0; 0, -ι]

def ThreeAxes.QuaternionTheta.mj {R : Type u_1} [CommRing R] : Matrix (Fin 2) (Fin 2) R

𝐣 = !![0, 1; −1, 0].

Equations

• ThreeAxes.QuaternionTheta.mj = !![0, 1; -1, 0]

def ThreeAxes.QuaternionTheta.mk {R : Type u_1} [CommRing R] (ι : R) : Matrix (Fin 2) (Fin 2) R

𝐤 = 𝐢𝐣.

Equations

• ThreeAxes.QuaternionTheta.mk ι = ThreeAxes.QuaternionTheta.mi ι * ThreeAxes.QuaternionTheta.mj

theorem ThreeAxes.QuaternionTheta.mi_mul_mi {R : Type u_1} [CommRing R] {ι : R} (hι : ι * ι = -1) : mi ι * mi ι = -1

theorem ThreeAxes.QuaternionTheta.mj_mul_mj {R : Type u_1} [CommRing R] : mj * mj = -1

theorem ThreeAxes.QuaternionTheta.mi_mul_mj {R : Type u_1} [CommRing R] {ι : R} : mi ι * mj = mk ι

theorem ThreeAxes.QuaternionTheta.mj_mul_mi {R : Type u_1} [CommRing R] {ι : R} : mj * mi ι = -mk ι

theorem ThreeAxes.QuaternionTheta.mk_mul_mk {R : Type u_1} [CommRing R] {ι : R} (hι : ι * ι = -1) : mk ι * mk ι = -1

theorem ThreeAxes.QuaternionTheta.mi_mul_mj_add {R : Type u_1} [CommRing R] {ι : R} : mi ι * mj + mj * mi ι = 0

theorem ThreeAxes.QuaternionTheta.smul_mul_smul_self {R : Type u_1} [CommRing R] {q : Matrix (Fin 2) (Fin 2) R} (hq : q * q = -1) (t : R) : t • q * t • q = -t ^ 2 • 1

If q² = −1, then (t q)² = −t² I.

theorem ThreeAxes.QuaternionTheta.theta_c_eq_zero {R : Type u_1} [CommRing R] {ι : R} (t : R) : t • mi ι * t • mj + t • mj * t • mi ι = 0

c = ξη + ηξ maps to 0.

theorem ThreeAxes.QuaternionTheta.det_one_add_smul_mi {R : Type u_1} [CommRing R] {ι : R} (hι : ι * ι = -1) (t : R) : (1 + t • mi ι).det = 1 + t ^ 2

theorem ThreeAxes.QuaternionTheta.det_one_add_smul_mj {R : Type u_1} [CommRing R] (t : R) : (1 + t • mj).det = 1 + t ^ 2

theorem ThreeAxes.QuaternionTheta.det_one_add_smul_mk {R : Type u_1} [CommRing R] {ι : R} (hι : ι * ι = -1) (t : R) : (1 + t • mk ι).det = 1 + t ^ 2

theorem ThreeAxes.QuaternionTheta.one_add_smul_mul_one_sub_smul {R : Type u_1} [CommRing R] {q : Matrix (Fin 2) (Fin 2) R} (hq : q * q = -1) (t : R) : (1 + t • q) * (1 - t • q) = (1 + t ^ 2) • 1

(I + t q)(I − t q) = (1 + t²) I when q² = −1.

theorem ThreeAxes.QuaternionTheta.one_sub_smul_mul_one_add_smul {R : Type u_1} [CommRing R] {q : Matrix (Fin 2) (Fin 2) R} (hq : q * q = -1) (t : R) : (1 - t • q) * (1 + t • q) = (1 + t ^ 2) • 1