The classical tower ℝ, ℂ, ℍ, 𝕆

Specializing the Cayley–Dickson tower of Composition/Octonion.lean to μ₁ = μ₂ = μ₃ = -1 over an ordered field gives the classical chain of composition algebras in which every nonzero element is invertible, of ranks 1, 2, 4, 8 — division algebras in the sense of GPR 8.6, being alternative. Over ℝ these are the reals, the complex numbers, the quaternions and the octonions.

The mechanism is that a negative scalar keeps the norm positive definite: the norm of Cay(B, μ) is n_B(u) - μ n_B(v), and for μ < 0 that is a sum of two non-negative terms which vanishes only when both do. A positive definite form is anisotropic, and an anisotropic norm makes every nonzero element invertible, because x (conj x) = n(x)·1 exhibits n(x)⁻¹ · (conj x) as a two-sided inverse of x.

Note that the inverse is obtained here without alternativity or associativity: the identity x (conj x) = (conj x) x = n(x)·1 holds in every conic algebra, so the inverse is immediate once n(x) is a unit (ConicAlgebra.hasTwoSidedInverses_of_anisotropic). ⚠ That is not yet division in the sense of GPR 8.6 (bijective left and right multiplication by nonzero elements): the real sedenions are anisotropic, so have such inverses, but have zero divisors (GPR Exc. 19.29(e), ConicAlgebra.not_isDivision_realSedenion). Alternativity is what upgrades the inverse to division — (conj x)(xy) = n(x) y — and the four algebras here are alternative (ConicAlgebra.isDivision_of_anisotropic, applied in ConicAlgebra.isDivision_realOctonion).

Main results

• ConicAlgebra.PosDef.cay : μ < 0 preserves positive definiteness under doubling.
• ConicAlgebra.posDef_cay₈, ConicAlgebra.exists_inv_cay₈ : the rank-8 member of the tower at negative scalars is positive definite, hence every nonzero element is invertible.
• ConicAlgebra.RealOctonion : the real octonions 𝕆, with finrank_realOctonion (rank 8), isComposition_realOctonion, isAlternative_realOctonion, exists_inv_realOctonion and isDivision_realOctonion (𝕆 is a division algebra in the sense of GPR 8.6).
• ConicAlgebra.exists_mul_ne_mul_realQuaternion, ConicAlgebra.exists_mul_mul_ne_mul_mul_realOctonion : ℍ is not commutative and 𝕆 is not associative — the explicit witnesses that the tower stops.

Relation to mathlib's ℂ and ℍ

ConicAlgebra.Cay₂ ℝ (-1) and ConicAlgebra.Cay₄ ℝ (-1) (-1) are identified with mathlib's Complex and Quaternion ℝ in Composition/ComplexQuaternion.lean (ConicAlgebra.realComplexAlgEquiv, ConicAlgebra.realQuaternionAlgEquiv), as isometries carrying the conjugation to star. Nothing in this file depends on those identifications.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 19.18, 23.

Positive definiteness under doubling

theorem ConicAlgebra.PosDef.cay {k : Type u} [CommRing k] [LinearOrder k] [IsStrictOrderedRing k] {B : Type v} [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] (C : ConicAlgebra k B) {μ : k} (hμ : μ < 0) (h : QuadraticMap.PosDef C.norm) : QuadraticMap.PosDef (C.cay μ).norm

Doubling at a negative scalar preserves positive definiteness. The norm of Cay(B, μ) is n_B(u) - μ n_B(v); for μ < 0 both terms are non-negative, and at least one is strictly positive unless u = v = 0.

theorem ConicAlgebra.posDef_baseRing (k : Type u) [CommRing k] [LinearOrder k] [IsStrictOrderedRing k] : QuadraticMap.PosDef (baseRing k).norm

The norm of the base ring, x ↦ x², is positive definite.

theorem ConicAlgebra.posDef_cay₂ (k : Type u) [CommRing k] [LinearOrder k] [IsStrictOrderedRing k] {μ₁ : k} (h₁ : μ₁ < 0) : QuadraticMap.PosDef (cay₂ k μ₁).norm

theorem ConicAlgebra.posDef_cay₄ (k : Type u) [CommRing k] [LinearOrder k] [IsStrictOrderedRing k] {μ₁ μ₂ : k} (h₁ : μ₁ < 0) (h₂ : μ₂ < 0) : QuadraticMap.PosDef (cay₄ k μ₁ μ₂).norm

theorem ConicAlgebra.posDef_cay₈ (k : Type u) [CommRing k] [LinearOrder k] [IsStrictOrderedRing k] {μ₁ μ₂ μ₃ : k} (h₁ : μ₁ < 0) (h₂ : μ₂ < 0) (h₃ : μ₃ < 0) : QuadraticMap.PosDef (cay₈ k μ₁ μ₂ μ₃).norm

The rank-8 member of the tower at negative scalars has positive definite norm — over ℝ, the sum of eight squares.

theorem ConicAlgebra.exists_inv_cay₈ (K : Type u) [Field K] [LinearOrder K] [IsStrictOrderedRing K] {μ₁ μ₂ μ₃ : K} (h₁ : μ₁ < 0) (h₂ : μ₂ < 0) (h₃ : μ₃ < 0) {x : Cay₈ K μ₁ μ₂ μ₃} (hx : x ≠ 0) : ∃ (y : Cay₈ K μ₁ μ₂ μ₃), x * y = 1 ∧ y * x = 1

In the rank-8 member of the tower at negative scalars over an ordered field, every nonzero element is invertible.

The real octonions

⚠ RealComplex and RealQuaternion are the Cayley–Dickson doubles, not mathlib's Complex and Quaternion ℝ. The identifying AlgEquivs are ConicAlgebra.realComplexAlgEquiv and ConicAlgebra.realQuaternionAlgEquiv, in Composition/ComplexQuaternion.lean.

@[reducible, inline]

abbrev ConicAlgebra.RealComplex : Type

ℂ as a Cayley–Dickson double, Cay(ℝ, -1).

Equations

• ConicAlgebra.RealComplex = ConicAlgebra.Cay₂ ℝ (-1)

@[reducible, inline]

abbrev ConicAlgebra.RealQuaternion : Type

ℍ as a Cayley–Dickson double, Cay(ℂ, -1).

Equations

• ConicAlgebra.RealQuaternion = ConicAlgebra.Cay₄ ℝ (-1) (-1)

@[reducible, inline]

abbrev ConicAlgebra.RealOctonion : Type

The real octonions 𝕆, Cay(ℍ, -1). mathlib has no octonions; this is the definition of record here.

Equations

• ConicAlgebra.RealOctonion = ConicAlgebra.Cay₈ ℝ (-1) (-1) (-1)

@[reducible, inline]

noncomputable abbrev ConicAlgebra.realOctonion : ConicAlgebra ℝ RealOctonion

The conic structure on 𝕆.

Equations

• ConicAlgebra.realOctonion = ConicAlgebra.cay₈ ℝ (-1) (-1) (-1)

theorem ConicAlgebra.finrank_realComplex : Module.finrank ℝ RealComplex = 2

theorem ConicAlgebra.finrank_realQuaternion : Module.finrank ℝ RealQuaternion = 4

theorem ConicAlgebra.finrank_realOctonion : Module.finrank ℝ RealOctonion = 8

𝕆 has dimension 8 over ℝ.

theorem ConicAlgebra.isAlternative_realOctonion : IsAlternative RealOctonion

𝕆 is alternative.

theorem ConicAlgebra.posDef_realOctonion : QuadraticMap.PosDef realOctonion.norm

The norm of 𝕆 is positive definite — the sum of eight squares.

theorem ConicAlgebra.exists_inv_realOctonion {x : RealOctonion} (hx : x ≠ 0) : ∃ (y : RealOctonion), x * y = 1 ∧ y * x = 1

Every nonzero octonion is invertible.

theorem ConicAlgebra.isDivision_realOctonion : IsDivision RealOctonion

𝕆 is a division algebra in the sense of GPR 8.6: it is alternative with anisotropic norm, so GPR 13.8 applies (ConicAlgebra.isDivision_of_anisotropic).

Where the tower breaks

ℍ is not commutative and 𝕆 is not associative, with explicit witnesses. These are what stop the tower: ConicAlgebra.mul_assoc_cay needs its input commutative, so 𝕆 gets no Ring structure, and ConicAlgebra.isMultiplicative_cay and ConicAlgebra.isAlternative_cay need their input associative. These sufficient results cannot be iterated from non-associative 𝕆. This does not imply failure of norm multiplicativity for every parameter: the criterion in GPR Exc. 18.18 is automatic for μ = 0.

theorem ConicAlgebra.conj_i_ne_i : (cay₂ ℝ (-1)).conj (0, 1) ≠ (0, 1)

The conjugation of ℂ moves i, which is what makes ℍ non-commutative.

theorem ConicAlgebra.exists_mul_ne_mul_realQuaternion : ∃ (x : RealQuaternion) (y : RealQuaternion), x * y ≠ y * x

ℍ is not commutative.

theorem ConicAlgebra.exists_mul_mul_ne_mul_mul_realOctonion : ∃ (x : RealOctonion) (y : RealOctonion) (z : RealOctonion), x * y * z ≠ x * (y * z)

𝕆 is not associative.

theorem ConicAlgebra.isComposition_realOctonion : realOctonion.IsComposition

𝕆 is a composition algebra of rank 8 over ℝ.