Documentation

TauCeti.Algebra.CentralSimple.Quaternion

Splitting the real quaternions #

The real quaternions ℍ[ℝ] are a central division algebra of dimension 4 over ℝ, hence a central simple ℝ-algebra of degree 2. They are not a matrix algebra over ℝ, but they become one in two ways: after tensoring with their opposite, or with themselves, over ℝ, and after extending scalars to ℂ.

For the first, this file runs the opposite isomorphism of TauCeti/Algebra/CentralSimple/Opposite.lean on ℍ[ℝ], in the two forms

ℍ[ℝ] ⊗[ℝ] ℍ[ℝ]ᵐᵒᵖ ≃ₐ[ℝ] Matrix (Fin 4) (Fin 4) ℝ and ℍ[ℝ] ⊗[ℝ] ℍ[ℝ] ≃ₐ[ℝ] Matrix (Fin 4) (Fin 4) ℝ.

The tensor-square form follows from the opposite form because quaternion conjugation is an ℝ-algebra isomorphism ℍ[ℝ] ≃ₐ[ℝ] ℍ[ℝ]ᵐᵒᵖ (Mathlib's Quaternion.starAe): the quaternions are their own opposite.

For the second, ℂ is algebraically closed, so it splits ℍ[ℝ] already at its degree: ℂ ⊗[ℝ] ℍ[ℝ] ≃ₐ[ℂ] Matrix (Fin 2) (Fin 2) ℂ. That is, the complexification of the quaternions is the full matrix algebra M₂(ℂ).

Nothing below is a statement about BrauerGroup ℝ: the main results are algebra isomorphisms, and the two examples closing the file are a degree computation and a nonexistence statement. Informally, the tensor-square isomorphisms exhibit the Brauer class of ℍ[ℝ] as self-inverse; that the class is moreover not the identity, so that its order is exactly 2, is TauCeti.Quaternion.orderOf_mk_eq_two in TauCeti/Algebra/BrauerGroup/Quaternion.lean. Saying that BrauerGroup ℝ ≃ ℤ/2 is a further and independent matter, needing the classification of real division algebras to know the class generates; that is TauCeti.Quaternion.brauerGroupMulEquiv in TauCeti/Algebra/BrauerGroup/Real.lean.

The matrix size is 4 and not 2: it is the dimension Module.finrank ℝ ℍ[ℝ] = 4 of the algebra, not its degree TauCeti.Algebra.deg ℝ ℍ[ℝ] = 2. Squaring the degree is exactly what taking the tensor product with the opposite algebra does, and the degree example at the end of the file checks it.

Main results #

References #

source
noncomputable def TauCeti.Quaternion.tensorOpAlgEquivMatrix :
TensorProduct ℝ (Quaternion ℝ) (Quaternion ℝ)ᵐᵒᵖ ≃ₐ[ℝ] Matrix (Fin 4) (Fin 4) ℝ

ℍ[ℝ] ⊗[ℝ] ℍ[ℝ]ᵐᵒᵖ ≃ₐ[ℝ] Matrix (Fin 4) (Fin 4) ℝ: the opposite isomorphism at the real quaternions. TauCeti.Algebra.tensorOpAlgEquivMatrix asks for IsAzumaya ℝ ℍ[ℝ], which TauCeti.IsSimpleRing.isAzumaya supplies and which is not an instance, so it is installed by hand; its own three hypotheses are found by instance search -- Algebra.IsCentral ℝ ℍ[ℝ] from TauCeti.Quaternion.instIsCentral, IsSimpleRing ℍ[ℝ] because a division ring is simple, and FiniteDimensional ℝ ℍ[ℝ] -- so beyond it only the dimension Quaternion.finrank_eq_four has to be supplied.

Equations
Instances For
    source
    noncomputable def TauCeti.Quaternion.tensorSelfAlgEquivMatrix :
    TensorProduct ℝ (Quaternion ℝ) (Quaternion ℝ) ≃ₐ[ℝ] Matrix (Fin 4) (Fin 4) ℝ

    ℍ[ℝ] ⊗[ℝ] ℍ[ℝ] ≃ₐ[ℝ] Matrix (Fin 4) (Fin 4) ℝ. Quaternion conjugation is an ℝ-algebra isomorphism ℍ[ℝ] ≃ₐ[ℝ] ℍ[ℝ]ᵐᵒᵖ (Quaternion.starAe), so the tensor square of ℍ[ℝ] is its tensor product with its own opposite, which TauCeti.Quaternion.tensorOpAlgEquivMatrix splits.

    In Brauer-group language this exhibits the class of ℍ[ℝ] as its own inverse. Whether that class is the identity is a separate question, not settled by this isomorphism; see the module docstring.

    Equations
    Instances For
      source
      noncomputable def TauCeti.Quaternion.complexTensorAlgEquivMatrix :
      TensorProduct ℝ ℂ (Quaternion ℝ) ≃ₐ[ℂ] Matrix (Fin 2) (Fin 2) ℂ

      ℂ ⊗[ℝ] ℍ[ℝ] ≃ₐ[ℂ] Matrix (Fin 2) (Fin 2) ℂ: the complex numbers split the real quaternions at their degree 2, so after extending scalars to ℂ the quaternions become the full matrix algebra M₂(ℂ).

      Equations
      Instances For