Quaternion models of ternary even Clifford algebras

For the diagonal form ⟨a, b, c⟩, with c a unit, its even Clifford algebra is the quaternion algebra with symbols -a/c and -b/c. Clifford reversal becomes quaternion conjugation and the reverse norm becomes the quaternion norm form. The explicit equivalence works over a commutative ring; over a field of characteristic different from two, diagonalization therefore supplies such a model for every nondegenerate ternary form.

The construction composes TauCeti.CliffordAlgebra.evenProdSMulSqEquiv with Mathlib's CliffordAlgebraQuaternion.equiv, and uses Mathlib's unit-weight diagonalization for arbitrary forms. The symbols need not be squares, so the model includes nonsplit quaternion algebras.

For the sum of three squares, the generic diagonal model is identified with the Hamilton quaternions. Compatible pure-quaternion coordinates identify the original quadratic space with the pure Hamilton norm form.

Main results

• CliffordAlgebra.evenWeightedSumSquaresThreeQuaternionEquiv models a diagonal ternary even Clifford algebra by a quaternion algebra.
• CliffordAlgebra.evenHamiltonEquivWeightedSumSquaresOne specializes this model to the Hamilton quaternions for the sum of three squares.
• CliffordAlgebra.pureHamiltonEquivWeightedSumSquaresOne gives compatible pure-quaternion coordinates for the underlying quadratic space.

References

• M.-A. Knus, A. Merkurjev, M. Rost and J.-P. Tignol, The Book of Involutions (1998), §15.

noncomputable def CliffordAlgebra.evenQuaternionEquiv {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) : ↥(even (QuadraticMap.prod (CliffordAlgebraQuaternion.Q a b) (↑c • QuadraticMap.sq))) ≃ₐ[R] QuaternionAlgebra R (-↑c⁻¹ * a) 0 (-↑c⁻¹ * b)

The even Clifford algebra of ⟨a, b, c⟩ is the quaternion algebra (-a/c, -b/c).

theorem CliffordAlgebra.evenQuaternionEquiv_ι {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) (x y : (R × R) × R) : (evenQuaternionEquiv a b c) (((even.ι (QuadraticMap.prod (CliffordAlgebraQuaternion.Q a b) (↑c • QuadraticMap.sq))).bilin x) y) = -↑c • ({ re := x.2, imI := x.1.1, imJ := x.1.2, imK := 0 } * { re := -y.2, imI := y.1.1, imJ := y.1.2, imK := 0 })

The quaternion coordinates of a product of two ternary Clifford generators.

theorem CliffordAlgebra.evenQuaternionEquiv_symm_mk {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) (r i j k : R) : (evenQuaternionEquiv a b c).symm { re := r, imI := i, imJ := j, imK := k } = (algebraMap R ↥(even (QuadraticMap.prod (CliffordAlgebraQuaternion.Q a b) (↑c • QuadraticMap.sq)))) r + (-↑c⁻¹ * i) • ((even.ι (QuadraticMap.prod (CliffordAlgebraQuaternion.Q a b) (↑c • QuadraticMap.sq))).bilin ((0, 0), 1)) ((1, 0), 0) + (-↑c⁻¹ * j) • ((even.ι (QuadraticMap.prod (CliffordAlgebraQuaternion.Q a b) (↑c • QuadraticMap.sq))).bilin ((0, 0), 1)) ((0, 1), 0) + (-↑c⁻¹ * k) • ((even.ι (QuadraticMap.prod (CliffordAlgebraQuaternion.Q a b) (↑c • QuadraticMap.sq))).bilin ((1, 0), 0)) ((0, 1), 0)

The inverse quaternion model expresses the coordinates in the scalar and three even Clifford basis elements.

@[simp]

theorem CliffordAlgebra.evenQuaternionEquiv_reverseEven {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) (x : ↥(even (QuadraticMap.prod (CliffordAlgebraQuaternion.Q a b) (↑c • QuadraticMap.sq)))) : (evenQuaternionEquiv a b c) ((reverseEven (QuadraticMap.prod (CliffordAlgebraQuaternion.Q a b) (↑c • QuadraticMap.sq))) x) = star ((evenQuaternionEquiv a b c) x)

Quaternion conjugation is the image of reversal in the ternary even Clifford algebra.

theorem CliffordAlgebra.evenQuaternionEquiv_reverseEven_mul_self {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) (x : ↥(even (QuadraticMap.prod (CliffordAlgebraQuaternion.Q a b) (↑c • QuadraticMap.sq)))) : (evenQuaternionEquiv a b c) ((reverseEven (QuadraticMap.prod (CliffordAlgebraQuaternion.Q a b) (↑c • QuadraticMap.sq))) x * x) = ↑((QuaternionAlgebra.normForm (-↑c⁻¹ * a) 0 (-↑c⁻¹ * b)) ((evenQuaternionEquiv a b c) x))

The reverse norm becomes the norm form of the corresponding quaternion algebra.

noncomputable def CliffordAlgebra.evenWeightedSumSquaresThreeQuaternionEquiv {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) : ↥(even (QuadraticMap.weightedSumSquares R ![a, b, ↑c])) ≃ₐ[R] QuaternionAlgebra R (-↑c⁻¹ * a) 0 (-↑c⁻¹ * b)

The even Clifford algebra of the diagonal ternary form ⟨a, b, c⟩ is the quaternion algebra (-a/c, -b/c).

theorem CliffordAlgebra.evenWeightedSumSquaresThreeQuaternionEquiv_ι {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) (x y : Fin 3 → R) : (evenWeightedSumSquaresThreeQuaternionEquiv a b c) (((even.ι (QuadraticMap.weightedSumSquares R ![a, b, ↑c])).bilin x) y) = -↑c • ({ re := x 2, imI := x 0, imJ := x 1, imK := 0 } * { re := -y 2, imI := y 0, imJ := y 1, imK := 0 })

The quaternion coordinates of a product of two generators of the even Clifford algebra of the diagonal ternary form.

theorem CliffordAlgebra.evenWeightedSumSquaresThreeQuaternionEquiv_symm_mk {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) (r i j k : R) : (evenWeightedSumSquaresThreeQuaternionEquiv a b c).symm { re := r, imI := i, imJ := j, imK := k } = (algebraMap R ↥(even (QuadraticMap.weightedSumSquares R ![a, b, ↑c]))) r + (-↑c⁻¹ * i) • ((even.ι (QuadraticMap.weightedSumSquares R ![a, b, ↑c])).bilin (Pi.single 2 1)) (Pi.single 0 1) + (-↑c⁻¹ * j) • ((even.ι (QuadraticMap.weightedSumSquares R ![a, b, ↑c])).bilin (Pi.single 2 1)) (Pi.single 1 1) + (-↑c⁻¹ * k) • ((even.ι (QuadraticMap.weightedSumSquares R ![a, b, ↑c])).bilin (Pi.single 0 1)) (Pi.single 1 1)

The inverse quaternion model of the diagonal ternary form expresses the coordinates in the scalar and three products of basis generators.

@[simp]

theorem CliffordAlgebra.evenWeightedSumSquaresThreeQuaternionEquiv_reverseEven {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) (x : ↥(even (QuadraticMap.weightedSumSquares R ![a, b, ↑c]))) : (evenWeightedSumSquaresThreeQuaternionEquiv a b c) ((reverseEven (QuadraticMap.weightedSumSquares R ![a, b, ↑c])) x) = star ((evenWeightedSumSquaresThreeQuaternionEquiv a b c) x)

Quaternion conjugation is the image of reversal in the even Clifford algebra of the diagonal ternary form.

theorem CliffordAlgebra.evenWeightedSumSquaresThreeQuaternionEquiv_reverseEven_mul_self {R : Type u_1} [CommRing R] (a b : R) (c : Rˣ) (x : ↥(even (QuadraticMap.weightedSumSquares R ![a, b, ↑c]))) : (evenWeightedSumSquaresThreeQuaternionEquiv a b c) ((reverseEven (QuadraticMap.weightedSumSquares R ![a, b, ↑c])) x * x) = ↑((QuaternionAlgebra.normForm (-↑c⁻¹ * a) 0 (-↑c⁻¹ * b)) ((evenWeightedSumSquaresThreeQuaternionEquiv a b c) x))

The reverse norm of the diagonal ternary form becomes the norm form of the corresponding quaternion algebra.

The Hamilton model of the sum of three squares

noncomputable def CliffordAlgebra.evenHamiltonEquivWeightedSumSquaresOne {R : Type u_1} [CommRing R] : ↥(even (QuadraticMap.weightedSumSquares R ![1, 1, 1])) ≃ₐ[R] Quaternion R

The even Clifford algebra of the sum of three squares is canonically the Hamilton quaternion algebra.

theorem CliffordAlgebra.evenHamiltonEquivWeightedSumSquaresOne_ι {R : Type u_1} [CommRing R] (x y : Fin 3 → R) : evenHamiltonEquivWeightedSumSquaresOne (((even.ι (QuadraticMap.weightedSumSquares R ![1, 1, 1])).bilin x) y) = -({ re := x 2, imI := x 0, imJ := x 1, imK := 0 } * { re := -y 2, imI := y 0, imJ := y 1, imK := 0 })

The Hamilton coordinates of a product of two generators in the even Clifford algebra of the sum of three squares.

@[simp]

theorem CliffordAlgebra.evenHamiltonEquivWeightedSumSquaresOne_symm_mk {R : Type u_1} [CommRing R] (r i j k : R) : evenHamiltonEquivWeightedSumSquaresOne.symm { re := r, imI := i, imJ := j, imK := k } = (algebraMap R ↥(even (QuadraticMap.weightedSumSquares R ![1, 1, 1]))) r + -i • ((even.ι (QuadraticMap.weightedSumSquares R ![1, 1, 1])).bilin (Pi.single 2 1)) (Pi.single 0 1) + -j • ((even.ι (QuadraticMap.weightedSumSquares R ![1, 1, 1])).bilin (Pi.single 2 1)) (Pi.single 1 1) + -k • ((even.ι (QuadraticMap.weightedSumSquares R ![1, 1, 1])).bilin (Pi.single 0 1)) (Pi.single 1 1)

The inverse Hamilton model writes a quaternion in the scalar and standard bivector basis.

@[simp]

theorem CliffordAlgebra.evenHamiltonEquivWeightedSumSquaresOne_reverseEven {R : Type u_1} [CommRing R] (x : ↥(even (QuadraticMap.weightedSumSquares R ![1, 1, 1]))) : evenHamiltonEquivWeightedSumSquaresOne ((reverseEven (QuadraticMap.weightedSumSquares R ![1, 1, 1])) x) = star (evenHamiltonEquivWeightedSumSquaresOne x)

The canonical Hamilton model carries Clifford reversal to quaternion conjugation.

theorem CliffordAlgebra.evenHamiltonEquivWeightedSumSquaresOne_reverseEven_mul_self {R : Type u_1} [CommRing R] (x : ↥(even (QuadraticMap.weightedSumSquares R ![1, 1, 1]))) : evenHamiltonEquivWeightedSumSquaresOne ((reverseEven (QuadraticMap.weightedSumSquares R ![1, 1, 1])) x * x) = ↑(Quaternion.normSq (evenHamiltonEquivWeightedSumSquaresOne x))

In the canonical Hamilton model, the reverse norm is the quaternion norm-square.

noncomputable def CliffordAlgebra.pureHamiltonEquivWeightedSumSquaresOne {R : Type u_1} [CommRing R] : (QuadraticMap.weightedSumSquares R ![1, 1, 1]).IsometryEquiv (QuaternionAlgebra.pureNormForm (-1) (-1))

The sum-of-three-squares quadratic space in the coordinates compatible with the canonical Hamilton even-Clifford model. Its image is the pure Hamilton quaternions.

@[simp]

theorem CliffordAlgebra.coe_pureHamiltonEquivWeightedSumSquaresOne_apply {R : Type u_1} [CommRing R] (v : Fin 3 → R) : ↑(pureHamiltonEquivWeightedSumSquaresOne v) = { re := 0, imI := -v 1, imJ := v 0, imK := -v 2 }

The pure Hamilton quaternion corresponding to a vector in the sum-of-three-squares model.

@[simp]

theorem CliffordAlgebra.pureHamiltonEquivWeightedSumSquaresOne_symm_apply {R : Type u_1} [CommRing R] (q : ↥(QuaternionAlgebra.reₗ (-1) 0 (-1)).ker) : pureHamiltonEquivWeightedSumSquaresOne.symm q = ![(↑q).imJ, -(↑q).imI, -(↑q).imK]

The vector coordinates recovered from a pure Hamilton quaternion.

theorem CliffordAlgebra.exists_evenQuaternionEquiv_of_finrank_eq_three {K : Type u_2} {V : Type u_3} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 3) : ∃ (a : Kˣ) (b : Kˣ) (e : ↥(even Q) ≃ₐ[K] QuaternionAlgebra K (↑a) 0 ↑b), ∀ (x : ↥(even Q)), e ((reverseEven Q) x) = star (e x)

Every regular ternary quadratic form admits a quaternion model of its even Clifford algebra, in which reversal is quaternion conjugation. The two symbols are units and need not be squares.