Documentation

TauCeti.Algebra.Quaternion.Steinberg

The Steinberg relation for quaternion algebras #

For any a in a commutative ring, this file constructs the Steinberg matrix representation. When 2, a, and 1 - a are invertible, it gives the explicit splitting

ℍ[K, a, 1 - a] ≃ₐ[K] Matrix (Fin 2) (Fin 2) K.

The construction sends the standard quaternion generators to

!![0, a; 1, 0] and !![1, -a; 1, -1].

These matrices square to a and 1 - a, respectively, and anticommute. This is the usual matrix proof of the Steinberg relation for quaternion symbols; see Lam, Introduction to Quadratic Forms over Fields, Chapter III, Section 2.

Main definitions #

source
def TauCeti.QuaternionAlgebra.steinbergToMatrix {K : Type u_1} [CommRing K] (a : K) :
QuaternionAlgebra K a 0 (1 - a) →ₐ[K] Matrix (Fin 2) (Fin 2) K

The Steinberg matrix representation, defined for every parameter over a commutative ring.

Equations
Instances For
    source
    theorem TauCeti.QuaternionAlgebra.steinbergToMatrix_apply {K : Type u_1} [CommRing K] (a : K) (q : QuaternionAlgebra K a 0 (1 - a)) :
    (steinbergToMatrix a) q = !![q.re + q.imJ + a * q.imK, a * (q.imI - q.imJ - q.imK); q.imI + q.imJ + q.imK, q.re - q.imJ - a * q.imK]

    The entrywise formula for the Steinberg matrix representation.

    source
    @[simp]
    theorem TauCeti.QuaternionAlgebra.steinbergToMatrix_apply_i {K : Type u_1} [CommRing K] (a : K) :
    (steinbergToMatrix a) { re := 0, imI := 1, imJ := 0, imK := 0 } = !![0, a; 1, 0]

    The first quaternion generator maps to the standard Steinberg matrix.

    source
    @[simp]
    theorem TauCeti.QuaternionAlgebra.steinbergToMatrix_apply_j {K : Type u_1} [CommRing K] (a : K) :
    (steinbergToMatrix a) { re := 0, imI := 0, imJ := 1, imK := 0 } = !![1, -a; 1, -1]

    The second quaternion generator maps to the standard Steinberg matrix.

    source
    def TauCeti.QuaternionAlgebra.steinbergEquivMatrix {K : Type u_1} [CommRing K] [Invertible 2] (a : K) [Invertible a] [Invertible (1 - a)] :
    QuaternionAlgebra K a 0 (1 - a) ≃ₐ[K] Matrix (Fin 2) (Fin 2) K

    The Steinberg relation for quaternion algebras. If 2, a, and 1 - a are invertible in a commutative ring, the quaternion algebra with symbol (a, 1 - a) is split.

    The forward map sends the standard generators i and j to !![0, a; 1, 0] and !![1, -a; 1, -1], respectively.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.QuaternionAlgebra.steinbergEquivMatrix_toAlgHom {K : Type u_1} [CommRing K] [Invertible 2] (a : K) [Invertible a] [Invertible (1 - a)] :
      ↑(steinbergEquivMatrix a) = steinbergToMatrix a

      The Steinberg equivalence has the Steinberg representation as its underlying homomorphism.

      source
      @[simp]
      theorem TauCeti.QuaternionAlgebra.steinbergEquivMatrix_symm_apply {K : Type u_1} [CommRing K] [Invertible 2] (a : K) [Invertible a] [Invertible (1 - a)] (M : Matrix (Fin 2) (Fin 2) K) :
      (steinbergEquivMatrix a).symm M = have r := ⅟2 * (M 0 0 + M 1 1); have x := ⅟2 * (⅟a * M 0 1 + M 1 0); have s := M 1 0 - x; have z := ⅟(1 - a) * (s - (M 0 0 - r)); { re := r, imI := x, imJ := s - z, imK := z }

      The entrywise formula for the inverse of the Steinberg equivalence.