Documentation

TauCeti.Algebra.Quaternion.Split

Split quaternion algebras #

This file constructs explicit algebra equivalences from split quaternion algebras to two-by-two matrix algebras, over a commutative ring in which two is invertible.

For a unit b, the symbol algebra ℍ[R,1,b] is split. The equivalence sends its standard generators to

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

For a unit a, the symbol algebra ℍ[R,a,-a] is split. The equivalence sends its standard generators to

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

Their squares are respectively a and -a, and they anticommute. This is one of the standard symbol relations for quaternion algebras, useful for reducing identities involving the symbol (a, -a) to computations in a matrix algebra.

The formulas for the equivalences and their inverses are recorded entrywise, so later splitting arguments can use the constructions without unfolding the quaternion-basis implementation.

Main definitions #

References #

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

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

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.QuaternionAlgebra.oneEquivMatrix_apply {R : Type u_1} [CommRing R] [Invertible 2] (b : Rˣ) (q : QuaternionAlgebra R 1 0 ↑b) :
    (oneEquivMatrix b) q = !![q.re + q.imI, ↑b * (q.imJ + q.imK); q.imJ - q.imK, q.re - q.imI]

    The splitting equivalence on an arbitrary quaternion.

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

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

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

    The explicit splitting ℍ[R,a,-a] ≃ₐ[R] M₂(R) for a unit a, over a commutative ring in which 2 is invertible.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.QuaternionAlgebra.aNegAEquivMatrix_apply {R : Type u_1} [CommRing R] [Invertible 2] (a : Rˣ) (x : QuaternionAlgebra R (↑a) 0 (-↑a)) :
      (aNegAEquivMatrix a) x = !![x.re + ↑a * x.imK, ↑a * (x.imI - x.imJ); x.imI + x.imJ, x.re - ↑a * x.imK]

      The splitting equivalence is the standard matrix representation.

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

      The inverse of the splitting equivalence, in matrix coordinates.