Hurwitz's theorem: dimension

The statement

A nontrivial finite-dimensional real algebra has a unit, a bilinear multiplication, and a positive definite multiplicative norm form. Then its real dimension is 1, 2, 4, or 8. Associativity, commutativity, and a division property aren’t assumed.

dimℝ C ∈ {1, 2, 4, 8}.

The norm form is N(x) = B(x, x), where B is a symmetric bilinear form and N(xy) = N(x)N(y).

Hypotheses

• C is a NonAssocRing with a real module structure. IsScalarTower and SMulCommClass make the product real-bilinear.
• CompositionAlgebra C carries the form B, symmetry, positive definiteness, and the composition law.
• C is nontrivial and finite-dimensional over ℝ. Nontriviality excludes the zero algebra, which satisfies the other hypotheses but has dimension zero.

What’s not proved

This entry gives a dimension restriction. It doesn’t identify the algebra up to isomorphism; that stronger conclusion is the separate classification entry.

It doesn’t cover indefinite norm forms, split composition algebras, algebras without a unit, or composition over other fields. The dimension statement itself doesn’t construct representatives of all four dimensions.

open scoped Quaternion

universe u

theorem finrank_eq_one_or_two_or_four_or_eight
    {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] :
    Module.finrank ℝ C = 1 ∨ Module.finrank ℝ C = 2 ∨ Module.finrank ℝ C = 4 ∨
      Module.finrank ℝ C = 8