The four Euclidean composition algebras

ℝ, ℂ, ℍ and 𝕆 carry CompositionAlgebra structures, of real dimensions 1, 2, 4, 8. Hurwitz's theorem says there are no others.

★ Why this file exists at all. Composition/Defs.lean states a class. A class with no witness proves nothing, and every theorem quantified over it is vacuously true — the exact defect shape this development has been bitten by before. These four instances are what makes the class non-vacuous, and they are also the targets of the classification: the statement "C is one of the four" is only meaningful once the four are objects.

The instances

• Real.instCompositionAlgebra — N x = x².
• Complex.instCompositionAlgebra — N z = |z|²; the composition law is the Diophantus two-square identity.
• Quaternion.instCompositionAlgebra — N q = ‖q‖²; Euler's four-square identity, taken from Mathlib's Quaternion.normSq as a MonoidWithZeroHom.
• Octonion.instCompositionAlgebra — Degen's eight-square identity, taken from the tree's Octonion.norm_multiplicative.

★ The octonion instance is the sharpest cross-check available on Composition/Defs.lean: norm_multiplicative was proved in Octonions.lean from the hard-coded Fano multiplication table, with no reference to composition algebras at all, and it discharges B_comp after one rewrite — octIp_self_eq_norm_sq, which is ∑ xᵢxᵢ = ∑ xᵢ² and nothing more. So the class field really is the composition property and not a mis-transcription of it. ★ An earlier draft of this paragraph said "discharges B_comp verbatim". It does not: the simp only [ipBilin_apply, octIp_self_eq_norm_sq] in front of it is load-bearing, because the class is stated on the bilinear form and Octonions.lean states the identity on normSq.

★ 𝕆 needs NonAssocRing Octonion, One Octonion, IsScalarTower and SMulCommClass, none of which were in the tree — Octonions.lean has a bare Mul instance and a def one. They are assembled here from the distributivity and unit lemmas already proved there.

Scope

Substrate, and the non-vacuity witness for Composition/Defs.lean's class.

ℝ

@[instance_reducible]

instance Real.instCompositionAlgebra : CompositionAlgebra ℝ

ℝ is a Euclidean composition algebra with N x = x².

Equations

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

theorem Real.nf_eq (x : ℝ) : CompositionAlgebra.nf x = x * x

ℂ

def Complex.ipBilin : ℂ →ₗ[ℝ] ℂ →ₗ[ℝ] ℝ

The real inner product on ℂ.

Equations

• Complex.ipBilin = LinearMap.mk₂ ℝ (fun (x y : ℂ) => x.re * y.re + x.im * y.im) Complex.ipBilin._proof_1 Complex.ipBilin._proof_2 Complex.ipBilin._proof_3 Complex.ipBilin._proof_4

@[simp]

theorem Complex.ipBilin_apply (x y : ℂ) : (ipBilin x) y = x.re * y.re + x.im * y.im

@[instance_reducible]

instance Complex.instCompositionAlgebra : CompositionAlgebra ℂ

ℂ is a Euclidean composition algebra with N z = |z|². The composition law is the two-square identity.

Equations

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

theorem Complex.nf_eq (z : ℂ) : CompositionAlgebra.nf z = z.re * z.re + z.im * z.im

ℍ

★ ℍ carries its own componentwise SMul ℝ ℍ[ℝ] (Quaternion.instSMul), which shadows Algebra.toSMul. So IsScalarTower.right and Algebra.to_smulCommClass do not apply — they are stated for Algebra.toSMul — and the two bilinearity classes have to be proved against the componentwise action.

instance Quaternion.instIsScalarTowerSelf : IsScalarTower ℝ (Quaternion ℝ) (Quaternion ℝ)

instance Quaternion.instSMulCommClassSelf : SMulCommClass ℝ (Quaternion ℝ) (Quaternion ℝ)

noncomputable def Quaternion.ipBilin : Quaternion ℝ →ₗ[ℝ] Quaternion ℝ →ₗ[ℝ] ℝ

The real inner product on ℍ.

Equations

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

@[simp]

theorem Quaternion.ipBilin_apply (x y : Quaternion ℝ) : (ipBilin x) y = x.re * y.re + x.imI * y.imI + x.imJ * y.imJ + x.imK * y.imK

theorem Quaternion.ipBilin_self (x : Quaternion ℝ) : (ipBilin x) x = normSq x

@[instance_reducible]

noncomputable instance Quaternion.instCompositionAlgebra : CompositionAlgebra (Quaternion ℝ)

ℍ is a Euclidean composition algebra. The composition law is Euler's four-square identity, which Mathlib supplies as multiplicativity of Quaternion.normSq.

Equations

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

𝕆

@[instance_reducible]

instance Octonion.instOne : One Octonion

The unit of 𝕆. Octonions.lean has only a def one.

Equations

• Octonion.instOne = { one := Octonion.one }

theorem Octonion.one_def : 1 = one

@[instance_reducible]

instance Octonion.instNonAssocRing : NonAssocRing Octonion

Equations

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

instance Octonion.instIsScalarTower : IsScalarTower ℝ Octonion Octonion

instance Octonion.instSMulCommClass : SMulCommClass ℝ Octonion Octonion

instance Octonion.instNontrivial : Nontrivial Octonion

def Octonion.ipBilin : Octonion →ₗ[ℝ] Octonion →ₗ[ℝ] ℝ

The Euclidean inner product on 𝕆, as a bilinear map.

Equations

• Octonion.ipBilin = LinearMap.mk₂ ℝ Octonion.octIp ⋯ Octonion.ipBilin._proof_1 ⋯ Octonion.ipBilin._proof_2

@[simp]

theorem Octonion.ipBilin_apply (x y : Octonion) : (ipBilin x) y = x.octIp y

theorem Octonion.octIp_self_eq_norm_sq (x : Octonion) : x.octIp x = x.normSq

@[instance_reducible]

instance Octonion.instCompositionAlgebra : CompositionAlgebra Octonion

𝕆 is a Euclidean composition algebra. The composition law is Degen's eight-square identity, supplied by Octonion.norm_multiplicative — proved from the Fano multiplication table with no reference to composition algebras — after octIp_self_eq_norm_sq matches the bilinear form against normSq.

Equations

• Octonion.instCompositionAlgebra = { B := Octonion.ipBilin, B_symm := ⋯, B_pos := Octonion.instCompositionAlgebra._proof_1, B_comp := Octonion.instCompositionAlgebra._proof_2 }

The four dimensions

1, 2, 4, 8. Hurwitz's theorem is the statement that these are the only ones.

theorem Real.finrank_comp : Module.finrank ℝ ℝ = 1

theorem Complex.finrank_comp : Module.finrank ℝ ℂ = 2

theorem Quaternion.finrank_comp : Module.finrank ℝ (Quaternion ℝ) = 4

theorem Octonion.finrank_comp : Module.finrank ℝ Octonion = 8