The three base identifications

CD ℝ ≃ ℂ, CD ℂ ≃ ℍ and CD ℍ ≃ 𝕆, each as an isomorphism of composition algebras.

These are item (3) of the three things that turning Hurwitz's dimension theorem into Hurwitz's classification needs: (1) the external CD functor, built in Composition/CayleyDickson.lean; (2) a transport lemma identifying CD D with the internal double double A u of Composition/Doubling.lean; and (3) these three. ★ Item (2) is not in this file: it is CompEmb.double in Composition/Classification.lean, which also assembles all three items into hurwitz_classification. This file proves only the base cases.

Main definitions

• CompositionAlgebra.IsCompIso — an isomorphism of composition algebras: an ℝ-linear equivalence preserving the unit, the product and the norm form.
• cdRealEquiv : CD ℝ ≃ₗ[ℝ] ℂ, cdComplexEquiv : CD ℂ ≃ₗ[ℝ] ℍ[ℝ], cdQuaternionEquiv : CD ℍ[ℝ] ≃ₗ[ℝ] Octonion.

The octonion identification

★ The third is the only one that needed searching. This tree's Octonion is built from a hard-coded Fano multiplication table (Octonions.lean, Octonion.mul), not from a doubling, so matching it against CD ℍ[ℝ] means choosing a correspondence between the doubled basis 1, i, j, k, ℓ, iℓ, jℓ, kℓ and e₀, …, e₇ and then checking all 8 × 8 basis products.

The correspondence used below is

(a, b) ↦ (a.re, a.imI, a.imJ, b.re, a.imK, b.imJ, -b.imK, b.imI)

i.e. 1 ↦ e₀, i ↦ e₁, j ↦ e₂, k ↦ e₄, ℓ ↦ e₃, iℓ ↦ e₇, jℓ ↦ e₅, kℓ ↦ -e₆. It was found by enumerating the signed correspondences determined by the images of i, j and ℓ and testing each against the table; 1344 of the 2744 candidates work, and none of them is sign-free. The one above is among the 147 that flip exactly one sign.

★ Read the scope of that count exactly. The enumeration ranges over the monomial correspondences — those sending each of 1, i, j, k, ℓ, iℓ, jℓ, kℓ to a signed basis vector — and it is complete for those, since multiplicativity determines the other five images from the images of i, j and ℓ, and each of those has 14 possibilities. It says nothing about isomorphisms CD ℍ[ℝ] ≃ 𝕆 in general: Aut(𝕆) = G₂ is 14-dimensional, so almost none of them are monomial. "No sign-free correspondence" means no sign-free monomial one.

★ Note what this does not say: the search establishes that the two products agree, not that the labelling is canonical. A different Fano convention would produce a different correspondence, and nothing downstream depends on which one is used.

Scope

Substrate for the classification: it supplies the three base identifications the doubling chain is renamed along.

structure CompositionAlgebra.IsCompIso {C : Type u} {D : Type v} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] (f : C ≃ₗ[ℝ] D) : Prop

An isomorphism of composition algebras: an ℝ-linear equivalence preserving the unit, the product and the norm form.

★ The norm clause is not redundant bookkeeping — it is carried because everything downstream needs it and because sq_eq's argument that the product already determines N is not formalized in this tree. Carrying it makes every statement below strictly stronger than the unit-and-product-only notion.

• map_one : f 1 = 1

  The unit is preserved.

• map_mul (x y : C) : f (x * y) = f x * f y

  The product is preserved.

• map_nf (x : C) : nf (f x) = nf x

  The norm form is preserved.

The conjugation on the three associative carriers

@[simp]

theorem Real.cstar_eq (r : ℝ) : CompositionAlgebra.cstar r = r

@[simp]

theorem Complex.cstar_eq (z : ℂ) : CompositionAlgebra.cstar z = { re := z.re, im := -z.im }

theorem Quaternion.cstar_eq (q : Quaternion ℝ) : CompositionAlgebra.cstar q = { re := q.re, imI := -q.imI, imJ := -q.imJ, imK := -q.imK }

The four components of the quaternionic conjugation, and not Quaternion.cstar_eq, are what carries the simp normal form.

★ This is not a stylistic choice. Mathlib's Quaternion.re_mul and its three companions are simp lemmas keyed on (a * b).re, and they fail to fire when the first factor is a structure literal. With Quaternion.cstar_eq marked @[simp], these two behave differently —

example (a b : ℍ[ℝ]) : (a * b).re = a.re*b.re - a.imI*b.imI - a.imJ*b.imJ - a.imK*b.imK := by
  simp
example (a b : ℍ[ℝ]) : (cstar a * b).re = a.re*b.re + a.imI*b.imI + a.imJ*b.imJ + a.imK*b.imK := by
  simp; ring

— the first closes, and the second leaves ({ re := a.re, imI := -a.imI, … } * b).re for ring, which cannot touch it. Rewriting cstar componentwise keeps the product's arguments atomic, so the four Mathlib lemmas fire and the octonion map_mul below reduces to coordinates.

@[simp]

theorem Quaternion.cstar_re (q : Quaternion ℝ) : (CompositionAlgebra.cstar q).re = q.re

@[simp]

theorem Quaternion.cstar_imI (q : Quaternion ℝ) : (CompositionAlgebra.cstar q).imI = -q.imI

@[simp]

theorem Quaternion.cstar_imJ (q : Quaternion ℝ) : (CompositionAlgebra.cstar q).imJ = -q.imJ

@[simp]

theorem Quaternion.cstar_imK (q : Quaternion ℝ) : (CompositionAlgebra.cstar q).imK = -q.imK

The norm forms of ℍ and 𝕆, in coordinates

Composition/Instances.lean supplies Real.nf_eq and Complex.nf_eq; these are the two missing companions.

theorem Quaternion.nf_eq (q : Quaternion ℝ) : CompositionAlgebra.nf q = q.re * q.re + q.imI * q.imI + q.imJ * q.imJ + q.imK * q.imK

theorem Octonion.nf_eq (o : Octonion) : CompositionAlgebra.nf o = o.coords 0 * o.coords 0 + o.coords 1 * o.coords 1 + o.coords 2 * o.coords 2 + o.coords 3 * o.coords 3 + o.coords 4 * o.coords 4 + o.coords 5 * o.coords 5 + o.coords 6 * o.coords 6 + o.coords 7 * o.coords 7

CD ℝ ≃ ℂ

def CompositionAlgebra.cdRealEquiv : CD ℝ ≃ₗ[ℝ] ℂ

The double of ℝ is ℂ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompositionAlgebra.cdRealEquiv_re (x : CD ℝ) : (cdRealEquiv x).re = x.fst

@[simp]

theorem CompositionAlgebra.cdRealEquiv_im (x : CD ℝ) : (cdRealEquiv x).im = x.snd

theorem CompositionAlgebra.cdRealEquiv_isCompIso : IsCompIso cdRealEquiv

CD ℂ ≃ ℍ

def CompositionAlgebra.cdComplexEquiv : CD ℂ ≃ₗ[ℝ] Quaternion ℝ

The double of ℂ is ℍ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompositionAlgebra.cdComplexEquiv_re (x : CD ℂ) : (cdComplexEquiv x).re = x.fst.re

@[simp]

theorem CompositionAlgebra.cdComplexEquiv_imI (x : CD ℂ) : (cdComplexEquiv x).imI = x.fst.im

@[simp]

theorem CompositionAlgebra.cdComplexEquiv_imJ (x : CD ℂ) : (cdComplexEquiv x).imJ = x.snd.re

@[simp]

theorem CompositionAlgebra.cdComplexEquiv_imK (x : CD ℂ) : (cdComplexEquiv x).imK = x.snd.im

theorem CompositionAlgebra.cdComplexEquiv_isCompIso : IsCompIso cdComplexEquiv

CD ℍ ≃ 𝕆

def CompositionAlgebra.cdQuaternionEquiv : CD (Quaternion ℝ) ≃ₗ[ℝ] Octonion

The double of ℍ is 𝕆, along the correspondence found by the basis search described in the module docstring.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompositionAlgebra.cdQuaternionEquiv_coords (x : CD (Quaternion ℝ)) : (cdQuaternionEquiv x).coords = ![x.fst.re, x.fst.imI, x.fst.imJ, x.snd.re, x.fst.imK, x.snd.imJ, -x.snd.imK, x.snd.imI]

theorem CompositionAlgebra.cdQuaternionEquiv_isCompIso : IsCompIso cdQuaternionEquiv