The real quaternions as two-by-two complex matrices, and SU(2)

The real quaternion algebra ℍ[ℝ] is a four-dimensional real form of the eight-dimensional real algebra M₂(ℂ). This file builds the embedding realizing it, as a homomorphism of ℝ-algebras compatible with the two conjugations:

Quaternion.toComplexMatrix : ℍ[ℝ] →⋆ₐ[ℝ] Matrix (Fin 2) (Fin 2) ℂ

sending the quaternion units to

i ↦ !![I, 0; 0, -I],    j ↦ !![0, 1; -1, 0],    k ↦ !![0, I; I, 0],

so that a general quaternion goes to

a + b i + c j + d k  ↦  !![a + b I, c + d I; -c + d I, a - b I].

Three facts make the embedding useful. Its determinant is the reduced norm (Quaternion.det_toComplexMatrix); it carries quaternion conjugation to the conjugate transpose, which is what makes it a StarAlgHom at all; and its image is cut out by two entry identities (Quaternion.mem_range_toComplexMatrix_iff), so the real form is explicit. Together they identify the unit quaternions with the special unitary group of degree two:

Quaternion.unitaryEquivSpecialUnitaryGroup :
  unitary ℍ[ℝ] ≃* Matrix.specialUnitaryGroup (Fin 2) ℂ.

Both inclusions are entry computations. A unit quaternion has determinant one and conjugate transpose its own inverse, so it lands in SU(2); conversely, for a special unitary matrix the conjugate transpose is the adjugate (Matrix.specialUnitaryGroup.star_eq_adjugate), and in degree two the adjugate swaps the diagonal and negates the off-diagonal, which is exactly the pair of identities carving out the real form.

Main definitions

• Quaternion.toComplexMatrix: the ℝ-algebra embedding ℍ[ℝ] →⋆ₐ[ℝ] M₂(ℂ).
• Quaternion.unitaryEquivSpecialUnitaryGroup: the unit quaternions are SU(2).

Main results

• Quaternion.toComplexMatrix_apply: the entries of the embedding.
• Quaternion.det_toComplexMatrix and Quaternion.trace_toComplexMatrix: the determinant is the reduced norm and the trace is the reduced trace.
• Quaternion.toComplexMatrix_injective: the embedding is injective.
• Quaternion.mem_range_toComplexMatrix_iff: the image is the set of matrices whose lower row is determined by the upper one by M 1 1 = star (M 0 0) and M 1 0 = -star (M 0 1).
• Quaternion.mem_specialUnitaryGroup_toComplexMatrix and Quaternion.exists_eq_toComplexMatrix_of_mem_specialUnitaryGroup: the two inclusions behind the equivalence, packaged as Quaternion.mem_specialUnitaryGroup_iff_exists_toComplexMatrix.

Implementation notes

This is not a splitting of a quaternion algebra, and it is not an instance of the splittings in TauCeti/Algebra/Quaternion/Split.lean or TauCeti/Algebra/Quaternion/SquareSplit.lean. Those produce algebra equivalences ℍ[R,a,b] ≃ₐ[R] M₂(R) when the symbol is split; ℍ[ℝ] is a division algebra, so no such equivalence exists over ℝ, and the base change ℂ ⊗[ℝ] ℍ[ℝ] ≃ₐ[ℂ] M₂(ℂ) that those files do supply is a homomorphism of ℂ-algebras out of a larger algebra. What is needed here is the ℝ-algebra embedding of ℍ[ℝ] itself, together with the information that it matches quaternion conjugation with the conjugate transpose: it is the compatibility of the two involutions, not the algebra structure alone, that sends unit quaternions to unitary matrices. That compatibility also pins the generators down to unitary conjugacy: conjugating the basis below by any invertible P leaves an algebra embedding, but the result is a StarAlgHom only when Pᴴ * P commutes with the whole image, hence — the image spanning M₂(ℂ) over ℂ — only when Pᴴ * P is a positive scalar matrix, which is to say when P is a positive multiple of a unitary matrix. Such a P conjugates exactly as its unitary part does, so the generators below are canonical only up to unitary conjugation, and a general conjugation need not respect star at all.

Quaternion.unitaryEquivSpecialUnitaryGroup is stated against Mathlib's Matrix.specialUnitaryGroup (Fin 2) ℂ; TauCeti.SU2 is a reducible abbreviation for that type, so the equivalence applies to it with no transport.

References

• W. Fulton and J. Harris, Representation Theory: A First Course, GTM 129, Lecture 20, §20.1.
• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I, §§3-4.

The embedding

noncomputable def Quaternion.toComplexMatrix : Quaternion ℝ →⋆ₐ[ℝ] Matrix (Fin 2) (Fin 2) ℂ

The real quaternions as two-by-two complex matrices. The embedding of ℝ-algebras with star sending the quaternion units i, j, k to !![I, 0; 0, -I], !![0, 1; -1, 0] and !![0, I; I, 0]. Quaternion conjugation becomes the conjugate transpose.

Equations

• Quaternion.toComplexMatrix = { toAlgHom := Quaternion.complexMatrixBasis✝.liftHom, map_star' := Quaternion.complexMatrixBasis_liftHom_star✝ }

theorem Quaternion.toComplexMatrix_apply (q : Quaternion ℝ) : toComplexMatrix q = !![↑q.re + ↑q.imI * Complex.I, ↑q.imJ + ↑q.imK * Complex.I; -↑q.imJ + ↑q.imK * Complex.I, ↑q.re - ↑q.imI * Complex.I]

The entries of Quaternion.toComplexMatrix.

This is deliberately not a simp lemma: expanding a bundled algebra map into a matrix literal is not a normal form, and it would hide the left-hand sides of Quaternion.det_toComplexMatrix and Quaternion.trace_toComplexMatrix, which are the intended simp-normal readings of the embedding.

@[simp]

theorem Quaternion.det_toComplexMatrix (q : Quaternion ℝ) : (toComplexMatrix q).det = ↑(normSq q)

The determinant of the matrix of a quaternion is its reduced norm.

@[simp]

theorem Quaternion.trace_toComplexMatrix (q : Quaternion ℝ) : (toComplexMatrix q).trace = ↑(2 * q.re)

The trace of the matrix of a quaternion is its reduced trace.

theorem Quaternion.toComplexMatrix_injective : Function.Injective ⇑toComplexMatrix

Quaternion.toComplexMatrix is injective: a quaternion whose matrix vanishes has vanishing reduced norm.

The image is the real form

theorem Quaternion.mem_range_toComplexMatrix_iff {M : Matrix (Fin 2) (Fin 2) ℂ} : M ∈ Set.range ⇑toComplexMatrix ↔ M 1 1 = star (M 0 0) ∧ M 1 0 = -star (M 0 1)

The image of Quaternion.toComplexMatrix is an explicit real form of M₂(ℂ): a complex two-by-two matrix is the matrix of a quaternion exactly when its lower row is read off its upper row by conjugation.

The unit quaternions are SU(2)

theorem Quaternion.mem_specialUnitaryGroup_toComplexMatrix {q : Quaternion ℝ} (hq : q ∈ unitary (Quaternion ℝ)) : toComplexMatrix q ∈ Matrix.specialUnitaryGroup (Fin 2) ℂ

A unit quaternion has special unitary matrix.

theorem Quaternion.exists_eq_toComplexMatrix_of_mem_specialUnitaryGroup {M : Matrix (Fin 2) (Fin 2) ℂ} (hM : M ∈ Matrix.specialUnitaryGroup (Fin 2) ℂ) : ∃ q ∈ unitary (Quaternion ℝ), toComplexMatrix q = M

Every special unitary matrix of degree two is the matrix of a unit quaternion.

theorem Quaternion.mem_specialUnitaryGroup_iff_exists_toComplexMatrix {M : Matrix (Fin 2) (Fin 2) ℂ} : M ∈ Matrix.specialUnitaryGroup (Fin 2) ℂ ↔ ∃ q ∈ unitary (Quaternion ℝ), toComplexMatrix q = M

A complex matrix of degree two is special unitary exactly when it is the matrix of a unit quaternion.

noncomputable def Quaternion.unitaryEquivSpecialUnitaryGroup : ↥(unitary (Quaternion ℝ)) ≃* ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ)

The unit quaternions are the special unitary group of degree two: the group Sp(1) of unit Hamilton quaternions is SU(2), by Quaternion.toComplexMatrix.

Equations

• Quaternion.unitaryEquivSpecialUnitaryGroup = MulEquiv.ofBijective Quaternion.unitaryToSpecialUnitaryGroup✝ Quaternion.unitaryEquivSpecialUnitaryGroup._proof_2✝

@[simp]

theorem Quaternion.coe_unitaryEquivSpecialUnitaryGroup_apply (q : ↥(unitary (Quaternion ℝ))) : ↑(unitaryEquivSpecialUnitaryGroup q) = toComplexMatrix ↑q

The special unitary matrix attached to a unit quaternion is its matrix under Quaternion.toComplexMatrix.

theorem Quaternion.coe_unitaryEquivSpecialUnitaryGroup_symm_apply (M : ↥(Matrix.specialUnitaryGroup (Fin 2) ℂ)) : toComplexMatrix ↑(unitaryEquivSpecialUnitaryGroup.symm M) = ↑M

The unit quaternion attached to a special unitary matrix has that matrix.