Hurwitz's theorem: the dimension of a Euclidean composition algebra is 1, 2, 4 or 8

finrank_eq_one_or_two_or_four_or_eight : a finite-dimensional Euclidean composition algebra has real dimension 1, 2, 4 or 8. Composition/Instances.lean exhibits ℝ, ℂ, ℍ, 𝕆 at each of the four, so all four occur.

The argument, and where the bound actually comes from

Start with A₀ = ℝ ∙ 1 and double: while the current composition subalgebra A is proper, exists_unit_orthogonal produces a unit u ⊥ A and Composition/Doubling.lean's three rules make A ⊕ A u a composition subalgebra of twice the dimension. So finrank C is a power of two, and the whole content of the theorem is that the fourth doubling is impossible.

★ The build plan said the doubling stops "because CD D composes only when D is associative", and flagged that it had not written this out to the level where a Lean gap would show. Written out, the mechanism is not the one the phrase suggests, and the difference matters:

• Closure of A ⊕ A u is unconditional — Doubling.lean proves the three rules with no associativity hypothesis. So the doubling never fails to close.
• What fails is the norm. Inside C the norm form is multiplicative by hypothesis, so expanding N(xy) = N x N y on x = a + bu, y = c + du yields, after both adjoint identities, ⟪b, (da)c⟫ = ⟪b, d(ac)⟫ for all b ∈ A — and A is nondegenerate, so A is associative. That is forced_assoc, and it is a hypothesis on A extracted from the mere existence of u, not a property of a separately constructed CD A.

★ Finite-dimensionality enters twice, and both times as counting: in exists_unit_orthogonal, to produce the normal at all, and in finrank_double and the chain of the main theorem, for the dimension bookkeeping. It does not enter the algebra: the three structural lemmas forced_assoc, comm_of_assoc_double and le_span_one_of_comm_double are proved without it, as the omit [FiniteDimensional ℝ C] lines above them record. ★ An earlier draft of this paragraph said finite-dimensionality was used "in exactly one place". That was false — finrank_double uses Submodule.finrank_sup_add_finrank_inf_eq and Submodule.equivMapOfInjective, and its own omit line omits only [Nontrivial C].

So the bound is a contrapositive: a composition subalgebra that is not associative has no unit vector orthogonal to it, hence is everything. Two more steps localise the failure: comm_of_assoc_double (if A ⊕ A u is associative then A is commutative) and le_span_one_of_comm_double (if A ⊕ A u is commutative then A ⊆ ℝ ∙ 1). At the fourth doubling these chain to finrank A₁ ≤ 1, contradicting finrank A₁ = 2.

What is not proved here

The classification — that a Euclidean composition algebra is isomorphic to ℝ, ℂ, ℍ or 𝕆 — is not proved here. Only the dimension is. Building the four isomorphisms needs the chain to be identified with the concrete carriers step by step, which is a separate construction: Composition/Classification.lean, hurwitz_classification. ★ That file re-runs the chain below with an embedding carried alongside it; it does not derive the maps from the dimension theorem, which it uses only once, to know the third double is everything.

Scope

This file carries finrank_eq_one_or_two_or_four_or_eight, Hurwitz's theorem in dimension form.

Right multiplication by a unit vector

def CompositionAlgebra.mulRightL {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] (u : C) : C →ₗ[ℝ] C

Right multiplication, as an ℝ-linear map.

Equations

• CompositionAlgebra.mulRightL u = { toFun := fun (x : C) => x * u, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem CompositionAlgebra.mulRightL_apply {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] (u x : C) : (mulRightL u) x = x * u

theorem CompositionAlgebra.mulRight_injective {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {u : C} (hnu : nf u = 1) : Function.Injective ⇑(mulRightL u)

Right multiplication by a unit vector is injective: it is a linear isometry of the norm form.

A proper subspace has a unit normal

theorem CompositionAlgebra.exists_unit_orthogonal {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [FiniteDimensional ℝ C] {A : Submodule ℝ C} (hA : A ≠ ⊤) : ∃ (u : C), (∀ a ∈ A, ip u a = 0) ∧ nf u = 1

Every proper subspace of a Euclidean composition algebra has a unit normal. This is the only place finite-dimensionality is used, and it is where the doubling gets its input.

The doubled subalgebra

def CompositionAlgebra.double {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] (A : Submodule ℝ C) (u : C) : Submodule ℝ C

The Cayley–Dickson double of A inside C, along the unit vector u.

Equations

• CompositionAlgebra.double A u = A ⊔ Submodule.map (CompositionAlgebra.mulRightL u) A

theorem CompositionAlgebra.mem_double_iff {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] {A : Submodule ℝ C} {u x : C} : x ∈ double A u ↔ ∃ a ∈ A, ∃ b ∈ A, x = a + b * u

theorem CompositionAlgebra.le_double {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] (A : Submodule ℝ C) (u : C) : A ≤ double A u

theorem CompositionAlgebra.mem_double_of_mem {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] {A : Submodule ℝ C} {u x : C} (hx : x ∈ A) : x ∈ double A u

theorem CompositionAlgebra.IsCompSubalgebra.unit_mem_double {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {A : Submodule ℝ C} (hA : IsCompSubalgebra A) {u : C} : u ∈ double A u

theorem CompositionAlgebra.IsCompSubalgebra.isCompSubalgebra_double {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [Nontrivial C] {A : Submodule ℝ C} (hA : IsCompSubalgebra A) {u : C} (hu : ∀ a ∈ A, ip u a = 0) (hnu : nf u = 1) : IsCompSubalgebra (double A u)

The doubled subalgebra is again a composition subalgebra. This is exactly the three Cayley–Dickson rules of Composition/Doubling.lean, assembled.

theorem CompositionAlgebra.IsCompSubalgebra.nf_add_mul_unit {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {A : Submodule ℝ C} (hA : IsCompSubalgebra A) {u : C} (hu : ∀ a ∈ A, ip u a = 0) (hnu : nf u = 1) {p : C} (hp : p ∈ A) {q : C} (hq : q ∈ A) : nf (p + q * u) = nf p + nf q

The norm of an element of the doubled algebra splits: N(p + q u) = N p + N q.

theorem CompositionAlgebra.IsCompSubalgebra.forced_assoc {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [Nontrivial C] {A : Submodule ℝ C} (hA : IsCompSubalgebra A) {u : C} (hu : ∀ a ∈ A, ip u a = 0) (hnu : nf u = 1) (x : C) : x ∈ A → ∀ y ∈ A, ∀ z ∈ A, x * y * z = x * (y * z)

Forced associativity. If some unit vector is orthogonal to the composition subalgebra A, then A is associative.

This is where Hurwitz's dimension bound actually comes from. The hypothesis is the existence of u, and the conclusion is a property of A alone: the norm form of C, restricted to A ⊕ A u, is multiplicative for free, and multiplicativity there is equivalent to associativity of A.

Dimension of the double

theorem CompositionAlgebra.IsCompSubalgebra.finrank_double {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [FiniteDimensional ℝ C] {A : Submodule ℝ C} (hA : IsCompSubalgebra A) {u : C} (hu : ∀ a ∈ A, ip u a = 0) (hnu : nf u = 1) : Module.finrank ℝ ↥(double A u) = 2 * Module.finrank ℝ ↥A

The doubling exactly doubles the dimension.

Where the chain stops

theorem CompositionAlgebra.IsCompSubalgebra.comm_of_assoc_double {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [Nontrivial C] {A : Submodule ℝ C} (hA : IsCompSubalgebra A) {u : C} (hu : ∀ a ∈ A, ip u a = 0) (hnu : nf u = 1) (h : ∀ x ∈ double A u, ∀ y ∈ double A u, ∀ z ∈ double A u, x * y * z = x * (y * z)) (x : C) : x ∈ A → ∀ y ∈ A, x * y = y * x

If the doubled algebra is associative, A is commutative.

theorem CompositionAlgebra.IsCompSubalgebra.le_span_one_of_comm_double {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [Nontrivial C] {A : Submodule ℝ C} (hA : IsCompSubalgebra A) {u : C} (hu : ∀ a ∈ A, ip u a = 0) (hnu : nf u = 1) (h : ∀ x ∈ double A u, ∀ y ∈ double A u, x * y = y * x) : A ≤ ℝ ∙ 1

If the doubled algebra is commutative, A is the line through the unit.

The base of the chain

theorem CompositionAlgebra.isCompSubalgebra_spanOne {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [Nontrivial C] : IsCompSubalgebra (ℝ ∙ 1)

The line through the unit is a composition subalgebra.

Hurwitz's theorem

theorem CompositionAlgebra.finrank_eq_one_or_two_or_four_or_eight {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [Nontrivial C] [FiniteDimensional ℝ C] : Module.finrank ℝ C = 1 ∨ Module.finrank ℝ C = 2 ∨ Module.finrank ℝ C = 4 ∨ Module.finrank ℝ C = 8

Hurwitz's theorem (dimension form). A finite-dimensional Euclidean composition algebra has real dimension 1, 2, 4 or 8.

Composition/Instances.lean exhibits ℝ, ℂ, ℍ and 𝕆 at the four values, so each is attained. The classification — that those four are the only algebras, not just the only dimensions — is Composition/Classification.lean's hurwitz_classification, not this theorem.