Quaternion symbols with a square parameter

This file constructs the explicit splitting of a quaternion symbol one of whose parameters is a square, starting with the second parameter. For units a and b over a commutative ring in which two is invertible, the equivalence

QuaternionAlgebra R a 0 b² ≃ₐ[R] Matrix (Fin 2) (Fin 2) R

sends its standard generators to

i ↦ !![0, a; 1, 0],   j ↦ !![b, 0; 0, -b].

The formulas for the equivalence and its inverse are recorded entrywise, so later symbol relations can use the splitting without unfolding the quaternion-basis implementation.

Main definitions

• TauCeti.secondSquareEquivMatrix: the equivalence from the quaternion symbol (a,b²) to Matrix (Fin 2) (Fin 2) R for units a and b.
• TauCeti.firstSquareEquivMatrix: the same for the symbol (a²,b), obtained by exchanging the two generators.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields, Chapter III, Section 2.11.

noncomputable def TauCeti.secondSquareEquivMatrix {R : Type u_1} [CommRing R] [Invertible 2] (a b : Rˣ) : QuaternionAlgebra R (↑a) 0 (↑b ^ 2) ≃ₐ[R] Matrix (Fin 2) (Fin 2) R

The explicit splitting of the symbol (a,b²) as M₂(R) for units a and b over a commutative ring in which two is invertible. It sends the quaternion generators i and j to !![0, a; 1, 0] and !![b, 0; 0, -b], respectively.

Equations

• TauCeti.secondSquareEquivMatrix a b = AlgEquiv.ofBijective (TauCeti.secondSquareMatrixBasis✝ ↑a ↑b).liftHom ⋯

@[simp]

theorem TauCeti.secondSquareEquivMatrix_apply {R : Type u_1} [CommRing R] [Invertible 2] (a b : Rˣ) (q : QuaternionAlgebra R (↑a) 0 (↑b ^ 2)) : (secondSquareEquivMatrix a b) q = !![q.re + ↑b * q.imJ, ↑a * q.imI - ↑a * ↑b * q.imK; q.imI + ↑b * q.imK, q.re - ↑b * q.imJ]

The splitting equivalence on an arbitrary quaternion.

@[simp]

theorem TauCeti.secondSquareEquivMatrix_symm_apply {R : Type u_1} [CommRing R] [Invertible 2] (a b : Rˣ) (M : Matrix (Fin 2) (Fin 2) R) : (secondSquareEquivMatrix a b).symm M = { re := ⅟2 * (M 0 0 + M 1 1), imI := ⅟2 * (↑a⁻¹ * M 0 1 + M 1 0), imJ := ⅟2 * (↑b⁻¹ * (M 0 0 - M 1 1)), imK := ⅟2 * (↑b⁻¹ * (M 1 0 - ↑a⁻¹ * M 0 1)) }

The inverse splitting equivalence recovers the four quaternion coordinates from the four matrix entries.

noncomputable def TauCeti.firstSquareEquivMatrix {R : Type u_1} [CommRing R] [Invertible 2] (a b : Rˣ) : QuaternionAlgebra R (↑a ^ 2) 0 ↑b ≃ₐ[R] Matrix (Fin 2) (Fin 2) R

The explicit splitting of the symbol (a²,b) as M₂(R) for units a and b over a commutative ring in which two is invertible: exchange the two generators with QuaternionAlgebra.swapEquiv and apply secondSquareEquivMatrix. It sends the quaternion generators i and j to !![a, 0; 0, -a] and !![0, b; 1, 0], respectively.

Equations

• TauCeti.firstSquareEquivMatrix a b = (QuaternionAlgebra.swapEquiv (↑a ^ 2) ↑b).trans (TauCeti.secondSquareEquivMatrix b a)

@[simp]

theorem TauCeti.firstSquareEquivMatrix_apply {R : Type u_1} [CommRing R] [Invertible 2] (a b : Rˣ) (q : QuaternionAlgebra R (↑a ^ 2) 0 ↑b) : (firstSquareEquivMatrix a b) q = !![q.re + ↑a * q.imI, ↑b * q.imJ + ↑b * ↑a * q.imK; q.imJ - ↑a * q.imK, q.re - ↑a * q.imI]

The first-parameter splitting equivalence on an arbitrary quaternion.

@[simp]

theorem TauCeti.firstSquareEquivMatrix_symm_apply {R : Type u_1} [CommRing R] [Invertible 2] (a b : Rˣ) (M : Matrix (Fin 2) (Fin 2) R) : (firstSquareEquivMatrix a b).symm M = { re := ⅟2 * (M 0 0 + M 1 1), imI := ⅟2 * (↑a⁻¹ * (M 0 0 - M 1 1)), imJ := ⅟2 * (↑b⁻¹ * M 0 1 + M 1 0), imK := -(⅟2 * (↑a⁻¹ * (M 1 0 - ↑b⁻¹ * M 0 1))) }

The inverse first-parameter splitting equivalence recovers the four quaternion coordinates from the four matrix entries.