Hurwitz's theorem, classification form

Composition/Hurwitz.lean proves that a finite-dimensional Euclidean composition algebra has real dimension 1, 2, 4 or 8. This file upgrades that to the classification: such an algebra is isomorphic to ℝ, ℂ, ℍ or 𝕆.

The missing piece, and where it goes

The dimension proof runs a chain of composition subalgebras A₀ ⊆ A₁ ⊆ A₂ ⊆ A₃ inside C, each Aₖ₊₁ = double Aₖ uₖ₊₁, and counts. Every object in it is a Submodule ℝ C; nothing in it is a map to a named algebra. What turns the count into an identification is the transport lemma below: an embedding of D onto Aₖ and a unit u ⊥ Aₖ assemble into an embedding of the external double CD D onto Aₖ₊₁. Running that alongside the chain, and feeding it the three base identifications of Composition/Isomorphisms.lean, names each Aₖ.

Main definitions

• CompositionAlgebra.CompEmb D C — an ℝ-linear map D → C preserving the unit, the product and the norm form. It is automatically injective, and its range is a composition subalgebra.
• CompEmb.double — the transport lemma. CompEmb D C plus a unit normal to its range gives CompEmb (CD D) C, whose range is double (range f) u.

Main results

• CompositionAlgebra.hurwitz_classification — a finite-dimensional Euclidean composition algebra is isomorphic, as a composition algebra, to ℝ, ℂ, ℍ[ℝ] or Octonion.

★ The isomorphism carried is the strong one: IsCompIso of Composition/Isomorphisms.lean preserves the unit, the product and the norm form.

★ Where the chain stops is not re-derived here. The final branch — that a fourth doubling cannot happen — is discharged from finrank_eq_one_or_two_or_four_or_eight together with Octonion.finrank_comp: the third double already has dimension 8, and 8 is the largest value the dimension theorem allows, so it is everything. The exfalso branch of the dimension proof is what makes that true, and it is not repeated.

Scope

This file carries hurwitz_classification, the headline theorem of the development.

Embeddings of composition algebras

structure CompositionAlgebra.CompEmb (D : Type v) (C : Type u) [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] : Type (max u v)

An embedding of composition algebras: an ℝ-linear map preserving the unit, the product and the norm form. Injectivity is not assumed — it follows from map_nf and positive definiteness (CompEmb.injective).

• toLinearMap : D →ₗ[ℝ] C

  The underlying ℝ-linear map.

• map_one : self.toLinearMap 1 = 1

  The unit is preserved.

• map_mul (x y : D) : self.toLinearMap (x * y) = self.toLinearMap x * self.toLinearMap y

  The product is preserved.

• map_nf (x : D) : nf (self.toLinearMap x) = nf x

  The norm form is preserved.

theorem CompositionAlgebra.CompEmb.map_ip {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {D : Type v} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] (f : CompEmb D C) (x y : D) : ip (f.toLinearMap x) (f.toLinearMap y) = ip x y

An embedding preserves the form. This is the polarisation of map_nf, and it is what makes the conjugation transport.

theorem CompositionAlgebra.CompEmb.injective {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {D : Type v} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] (f : CompEmb D C) : Function.Injective ⇑f.toLinearMap

An embedding is injective: it preserves the norm form, which is positive definite.

theorem CompositionAlgebra.CompEmb.map_cstar {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {D : Type v} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] (f : CompEmb D C) (x : D) : f.toLinearMap (cstar x) = cstar (f.toLinearMap x)

An embedding preserves the conjugation. Both sides are (2⟪x,1⟫) • 1 - f x.

theorem CompositionAlgebra.CompEmb.range_isCompSubalgebra {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {D : Type v} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] (f : CompEmb D C) : IsCompSubalgebra f.toLinearMap.range

The range of an embedding is a composition subalgebra.

theorem CompositionAlgebra.CompEmb.finrank_range {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {D : Type v} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] (f : CompEmb D C) : Module.finrank ℝ ↥f.toLinearMap.range = Module.finrank ℝ D

The range of an embedding has the dimension of its source.

Precomposition with an isomorphism

def CompositionAlgebra.CompEmb.congr {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {D : Type v} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] {E : Type w} [NonAssocRing E] [Module ℝ E] [IsScalarTower ℝ E E] [SMulCommClass ℝ E E] [CompositionAlgebra E] (e : E ≃ₗ[ℝ] D) (he : IsCompIso e) (f : CompEmb D C) : CompEmb E C

Rename the source of an embedding along an isomorphism of composition algebras.

Equations

• CompositionAlgebra.CompEmb.congr e he f = { toLinearMap := f.toLinearMap ∘ₗ ↑e, map_one := ⋯, map_mul := ⋯, map_nf := ⋯ }

@[simp]

theorem CompositionAlgebra.CompEmb.congr_apply {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {D : Type v} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] {E : Type w} [NonAssocRing E] [Module ℝ E] [IsScalarTower ℝ E E] [SMulCommClass ℝ E E] [CompositionAlgebra E] (e : E ≃ₗ[ℝ] D) (he : IsCompIso e) (f : CompEmb D C) (x : E) : (congr e he f).toLinearMap x = f.toLinearMap (e x)

theorem CompositionAlgebra.CompEmb.range_congr {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {D : Type v} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] {E : Type w} [NonAssocRing E] [Module ℝ E] [IsScalarTower ℝ E E] [SMulCommClass ℝ E E] [CompositionAlgebra E] (e : E ≃ₗ[ℝ] D) (he : IsCompIso e) (f : CompEmb D C) : (congr e he f).toLinearMap.range = f.toLinearMap.range

Renaming the source does not move the range.

From a surjective embedding to an isomorphism

noncomputable def CompositionAlgebra.CompEmb.toEquiv {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {D : Type v} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] (f : CompEmb D C) (h : f.toLinearMap.range = ⊤) : D ≃ₗ[ℝ] C

An embedding whose range is everything is an isomorphism D ≃ C.

Equations

• f.toEquiv h = LinearEquiv.ofBijective f.toLinearMap ⋯

@[simp]

theorem CompositionAlgebra.CompEmb.toEquiv_apply {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {D : Type v} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] (f : CompEmb D C) (h : f.toLinearMap.range = ⊤) (x : D) : (f.toEquiv h) x = f.toLinearMap x

theorem CompositionAlgebra.CompEmb.toEquiv_isCompIso {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {D : Type v} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] (f : CompEmb D C) (h : f.toLinearMap.range = ⊤) : IsCompIso (f.toEquiv h)

Inverting an isomorphism

theorem CompositionAlgebra.IsCompIso.symm {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {D : Type v} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] {e : C ≃ₗ[ℝ] D} (h : IsCompIso e) : IsCompIso e.symm

The inverse of an isomorphism of composition algebras is one.

The transport lemma

theorem CompositionAlgebra.IsCompSubalgebra.mul_add_mul_unit {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) {a : C} (ha : a ∈ A) {b : C} (hb : b ∈ A) {c : C} (hc : c ∈ A) {d : C} (hd : d ∈ A) : (a + b * u) * (c + d * u) = a * c - cstar d * b + (d * a + b * cstar c) * u

The product of two elements of A ⊕ A u, in Cayley–Dickson form. This is the computation inside IsCompSubalgebra.isCompSubalgebra_double, pulled out because the transport lemma needs it as an equation rather than as a closure statement.

def CompositionAlgebra.CompEmb.doubleMap {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {D : Type v} [Ring D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] [Nontrivial D] (f : CompEmb D C) {u : C} : CD D →ₗ[ℝ] C

The underlying map of the transport lemma: (a, b) ↦ f a + (f b) u.

Equations

• f.doubleMap = { toFun := fun (x : CompositionAlgebra.CD D) => f.toLinearMap x.fst + f.toLinearMap x.snd * u, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem CompositionAlgebra.CompEmb.doubleMap_apply {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {D : Type v} [Ring D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] [Nontrivial D] (f : CompEmb D C) {u : C} (x : CD D) : f.doubleMap x = f.toLinearMap x.fst + f.toLinearMap x.snd * u

def CompositionAlgebra.CompEmb.double {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [Nontrivial C] {D : Type v} [Ring D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] [Nontrivial D] (f : CompEmb D C) {u : C} (hu : ∀ a ∈ f.toLinearMap.range, ip u a = 0) (hnu : nf u = 1) : CompEmb (CD D) C

The transport lemma. An embedding of D into C and a unit vector orthogonal to its range assemble into an embedding of the external Cayley–Dickson double CD D.

Multiplicativity is exactly the three Cayley–Dickson rules of Composition/Doubling.lean; norm preservation is IsCompSubalgebra.nf_add_mul_unit.

Equations

• f.double hu hnu = { toLinearMap := f.doubleMap, map_one := ⋯, map_mul := ⋯, map_nf := ⋯ }

@[simp]

theorem CompositionAlgebra.CompEmb.double_apply {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [Nontrivial C] {D : Type v} [Ring D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] [Nontrivial D] (f : CompEmb D C) {u : C} (hu : ∀ a ∈ f.toLinearMap.range, ip u a = 0) (hnu : nf u = 1) (x : CD D) : (f.double hu hnu).toLinearMap x = f.toLinearMap x.fst + f.toLinearMap x.snd * u

theorem CompositionAlgebra.CompEmb.range_double {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [Nontrivial C] {D : Type v} [Ring D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] [Nontrivial D] (f : CompEmb D C) {u : C} (hu : ∀ a ∈ f.toLinearMap.range, ip u a = 0) (hnu : nf u = 1) : (f.double hu hnu).toLinearMap.range = CompositionAlgebra.double f.toLinearMap.range u

The transported embedding lands exactly on the internal double of the range.

The base of the chain

def CompositionAlgebra.realCompEmb {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [Nontrivial C] : CompEmb ℝ C

ℝ embeds as the line through the unit.

Equations

• CompositionAlgebra.realCompEmb = { toLinearMap := LinearMap.toSpanSingleton ℝ C 1, map_one := ⋯, map_mul := ⋯, map_nf := ⋯ }

@[simp]

theorem CompositionAlgebra.realCompEmb_apply {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [Nontrivial C] (x : ℝ) : realCompEmb.toLinearMap x = x • 1

theorem CompositionAlgebra.range_realCompEmb {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [Nontrivial C] : realCompEmb.toLinearMap.range = ℝ ∙ 1

The range of the base embedding is the line through the unit, the A₀ of the dimension proof.

Hurwitz's theorem, classification form

theorem CompositionAlgebra.hurwitz_classification {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [Nontrivial C] [FiniteDimensional ℝ C] : (∃ (f : C ≃ₗ[ℝ] ℝ), IsCompIso f) ∨ (∃ (f : C ≃ₗ[ℝ] ℂ), IsCompIso f) ∨ (∃ (f : C ≃ₗ[ℝ] Quaternion ℝ), IsCompIso f) ∨ ∃ (f : C ≃ₗ[ℝ] Octonion), IsCompIso f

Hurwitz's theorem (classification form). A finite-dimensional Euclidean composition algebra is isomorphic, as a composition algebra, to ℝ, ℂ, ℍ or 𝕆.

The isomorphism preserves the unit, the product and the norm form (IsCompIso).

The proof runs the doubling chain of finrank_eq_one_or_two_or_four_or_eight with an embedding carried alongside it: realCompEmb starts at A₀, CompEmb.double steps it along each Aₖ ↦ double Aₖ uₖ₊₁, and the three base identifications of Composition/Isomorphisms.lean rename the source at each step, CD ℝ ↦ ℂ, CD ℂ ↦ ℍ, CD ℍ ↦ 𝕆. Each branch of the chain ends when the range is everything; the last branch cannot fail to, because its range already has dimension 8.