Split quaternion unitary groups

The norm-one group of a split quaternion algebra is the two-dimensional special linear group. This file constructs the identification from an arbitrary algebra equivalence with a two-by-two matrix algebra.

The key compatibility is intrinsic: quaternion conjugation is anti-multiplicative and the sum of a quaternion and its conjugate is scalar. Transported to two-by-two matrices, those two properties characterize matrix adjugation. Consequently, the quaternion unitary equation becomes adjugate A * A = 1, which is equivalent to det A = 1.

Over a field of characteristic different from two, a quaternion algebra whose first unit symbol parameter is a square splits, so its unitary group is noncanonically isomorphic to SL₂. This applies in particular over a separably closed field.

Main results

• QuaternionAlgebra.map_star_eq_adjugate_of_algEquiv_matrix shows that any splitting algebra equivalence carries quaternion conjugation to matrix adjugation.
• QuaternionAlgebra.unitaryEquivSpecialLinearOfAlgEquiv restricts a splitting equivalence to an equivalence from the quaternion unitary group to SL₂.
• QuaternionAlgebra.nonempty_unitaryEquivSpecialLinear_of_isSquare supplies such an equivalence when the first unit symbol parameter is a square.
• QuaternionAlgebra.nonempty_unitaryEquivSpecialLinear_of_isSepClosed supplies such an equivalence over a separably closed field.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields (2005), Chapter III, §2.
• P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology (2006), §1.1.

@[simp]

theorem QuaternionAlgebra.map_star_eq_adjugate_of_algEquiv_matrix {R : Type u_1} [CommRing R] {c₁ c₂ c₃ : R} (e : QuaternionAlgebra R c₁ c₂ c₃ ≃ₐ[R] Matrix (Fin 2) (Fin 2) R) (q : QuaternionAlgebra R c₁ c₂ c₃) : e (star q) = (e q).adjugate

Any algebra equivalence from a quaternion algebra to two-by-two matrices carries quaternion conjugation to matrix adjugation.

noncomputable def QuaternionAlgebra.unitaryEquivSpecialLinearOfAlgEquiv {R : Type u_1} [CommRing R] {c₁ c₂ c₃ : R} (e : QuaternionAlgebra R c₁ c₂ c₃ ≃ₐ[R] Matrix (Fin 2) (Fin 2) R) : ↥(unitary (QuaternionAlgebra R c₁ c₂ c₃)) ≃* Matrix.SpecialLinearGroup (Fin 2) R

A splitting algebra equivalence restricts to an equivalence from the quaternion norm-one group to the two-dimensional special linear group.

Equations

• QuaternionAlgebra.unitaryEquivSpecialLinearOfAlgEquiv e = MulEquiv.ofBijective { toFun := fun (q : ↥(unitary (QuaternionAlgebra R c₁ c₂ c₃))) => ⟨e ↑q, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ } ⋯

@[simp]

theorem QuaternionAlgebra.coe_unitaryEquivSpecialLinearOfAlgEquiv_apply {R : Type u_1} [CommRing R] {c₁ c₂ c₃ : R} (e : QuaternionAlgebra R c₁ c₂ c₃ ≃ₐ[R] Matrix (Fin 2) (Fin 2) R) (q : ↥(unitary (QuaternionAlgebra R c₁ c₂ c₃))) : ↑((unitaryEquivSpecialLinearOfAlgEquiv e) q) = e ↑q

The quaternion-to-SL₂ equivalence evaluates the chosen splitting algebra equivalence.

@[simp]

theorem QuaternionAlgebra.coe_unitaryEquivSpecialLinearOfAlgEquiv_symm_apply {R : Type u_1} [CommRing R] {c₁ c₂ c₃ : R} (e : QuaternionAlgebra R c₁ c₂ c₃ ≃ₐ[R] Matrix (Fin 2) (Fin 2) R) (A : Matrix.SpecialLinearGroup (Fin 2) R) : ↑((unitaryEquivSpecialLinearOfAlgEquiv e).symm A) = e.symm ↑A

The inverse quaternion-to-SL₂ equivalence evaluates the inverse splitting algebra equivalence.

theorem QuaternionAlgebra.nonempty_unitaryEquivSpecialLinear_of_isSquare {K : Type u_2} [Field K] [NeZero 2] (a b : Kˣ) (ha : IsSquare ↑a) : Nonempty (↥(unitary (QuaternionAlgebra K (↑a) 0 ↑b)) ≃* Matrix.SpecialLinearGroup (Fin 2) K)

Over a field of characteristic different from two, the norm-one group of a quaternion algebra with unit symbol parameters is noncanonically isomorphic to SL₂ when its first parameter is a square.

theorem QuaternionAlgebra.nonempty_unitaryEquivSpecialLinear_of_isSepClosed {K : Type u_2} [Field K] [NeZero 2] [IsSepClosed K] (a b : Kˣ) : Nonempty (↥(unitary (QuaternionAlgebra K (↑a) 0 ↑b)) ≃* Matrix.SpecialLinearGroup (Fin 2) K)

Over a separably closed field of characteristic different from two, the norm-one group of a quaternion algebra with unit symbol parameters is noncanonically isomorphic to SL₂.