Hurwitz's theorem: classification

The statement

Every nontrivial finite-dimensional Euclidean composition algebra over the reals is isomorphic to ℝ, ℂ, ℍ, or 𝕆. The isomorphism is real-linear and preserves the unit, multiplication, and norm form. All four targets are constructed in the statement file, including octonions from their multiplication table.

C ≅ ℝ, ℂ, ℍ, or 𝕆, as a Euclidean composition algebra.

The predicate IsCompIso f includes preservation of the norm form, so the conclusion says more than an isomorphism of rings or vector spaces. The octonion target is named Oct in this entry.

Hypotheses

• C has a unital, real-bilinear product via NonAssocRing, Module ℝ, IsScalarTower, and SMulCommClass.
• Its symmetric positive definite bilinear form B satisfies B(xy, xy) = B(x, x)B(y, y).
• It is nontrivial and finite-dimensional. No associativity, commutativity, or division hypothesis is supplied.

What’s not proved

This is the Euclidean real classification. It doesn’t classify split or indefinite composition algebras, nonunital algebras, or algebras over other fields. No uniqueness of the isomorphism is asserted.

The theorem doesn’t identify the octonion automorphism group, prove triality, construct the exceptional Jordan algebra H₃(𝕆), or coordinatize Jordan algebras.

open scoped Quaternion

universe u v

theorem hurwitz_classification
    {C : Type u} [instRing : NonAssocRing C] [instMod : Module ℝ C]
    [instTower : IsScalarTower ℝ C C] [instSMulComm : SMulCommClass ℝ C C]
    [instCA : CompositionAlgebra C] [instNT : Nontrivial C] [instFD : FiniteDimensional ℝ C] :
    (∃ f : C ≃ₗ[ℝ] ℝ, IsCompIso f) ∨ (∃ f : C ≃ₗ[ℝ] ℂ, IsCompIso f) ∨
      (∃ f : C ≃ₗ[ℝ] ℍ[ℝ], IsCompIso f) ∨ (∃ f : C ≃ₗ[ℝ] Oct, IsCompIso f)