The Cayley–Dickson tower: rank 2, 4 and 8 (GPR 19.18)

Iterating the Cayley–Dickson process three times from the base ring produces, for scalars μ₁, μ₂, μ₃ ∈ k, conic algebras of ranks 2, 4 and 8:

Cay₂ k μ₁ = Cay(k, μ₁), Cay₄ k μ₁ μ₂ = Cay(Cay₂, μ₂) — a quaternion algebra, Cay₈ k μ₁ μ₂ μ₃ = Cay(Cay₄, μ₃) — an octonion algebra, which mathlib does not have.

Everything is over an arbitrary commutative ring k, with arbitrary scalars; the hypotheses 2 ∈ kˣ and μᵢ ∈ kˣ appear only on the theorem that the tower consists of composition algebras.

Why the tower stops at 8

Each rung is built by a theorem whose hypothesis is a property of the rung below. ConicAlgebra.mul_comm_cay needs its input's conjugation to be the identity, which holds for the base ring; ConicAlgebra.mul_assoc_cay needs its input commutative; and ConicAlgebra.isMultiplicative_cay (GPR Exc. 18.18) and ConicAlgebra.isAlternative_cay (GPR 18.14(c)) need it associative. So each property may be lost one rung after the property that implies it, and the fourth double — the sedenions — is in general neither alternative nor multiplicative. That is the mechanism behind the rank dichotomy 1, 2, 4, 8 of GPR 19.18.

What is proved positively here is that Cay₂ is commutative, Cay₄ is associative, and Cay₈ is alternative with multiplicative norm — each over an arbitrary base.

⚠ The negative half is genuinely characteristic-dependent and is therefore not stated in this file. Over a base in which 2 = 0 the conjugation of Cay₂ is again the identity, so ConicAlgebra.mul_comm_cay applies once more and the tower stays commutative — the ranks still double, but the algebras do not become non-commutative and then non-associative in the classical way. The explicit witnesses that ℍ is not commutative and 𝕆 is not associative are proved over ℝ in Composition/Examples.lean, from the general ConicAlgebra.exists_mul_ne_mul_cay and ConicAlgebra.exists_mul_mul_ne_mul_mul_cay.

Once such a witness is in hand for a rung, ConicAlgebra.not_isAlternative_cay_of_mul_mul_ne — the converse half of GPR 18.14(c) — turns it into the failure of alternativity one rung up, with no hypothesis on the scalar. That is the route to the sedenions of GPR 19.23.

Main definitions

• ConicAlgebra.Cay₂, ConicAlgebra.Cay₄, ConicAlgebra.Cay₈ : the underlying modules.
• ConicAlgebra.cay₂, ConicAlgebra.cay₄, ConicAlgebra.cay₈ : their conic structures.
• ConicAlgebra.Octonion, ConicAlgebra.octonion : notation for the rank-8 case.

Main results

• ConicAlgebra.isMultiplicative_cay₈ : the octonion norm permits composition.
• ConicAlgebra.isAlternative_cay₈ : octonion algebras are alternative (directly, from GPR 18.14(c), without going through GPR 19.3).
• ConicAlgebra.isComposition_cay₈ : for 2 ∈ kˣ and μᵢ units, the octonion algebra is a composition algebra; likewise isComposition_cay₂ and isComposition_cay₄.
• ConicAlgebra.finrank_cay₂, .finrank_cay₄, .finrank_cay₈ : the ranks are 2, 4, 8.

Implementation notes

The Ring, CommRing and Algebra structures on the rungs are declared as genuine instances here, unlike the defs they come from in Conic/CayleyDicksonAssociative.lean: at each rung the side conditions are discharged by theorems (ConicAlgebra.baseRing_conj_apply at the bottom, ConicAlgebra.ConjIsInvolution.cay above it) rather than assumed, so there is nothing for instance search to guess. This is what makes the tower usable without letI at every step.

⚠ Cay₄ is not mathlib's QuaternionAlgebra, and the two are incomparable in general — see overview trap 3. QuaternionAlgebra takes arbitrary structure constants and always produces a free module; Cay₄ produces a composition algebra exactly under the hypotheses below. Relating them is the job of a later file.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 18.14, Exc. 18.18, 19.18.

Rank 2

@[reducible, inline]

abbrev ConicAlgebra.Cay₂ (k : Type u) [CommRing k] (μ₁ : k) : Type u

The rank-2 Cayley–Dickson algebra Cay(k, μ₁), as a k-module.

Equations

• ConicAlgebra.Cay₂ k μ₁ = (ConicAlgebra.baseRing k).Cay μ₁

@[reducible, inline]

noncomputable abbrev ConicAlgebra.cay₂ (k : Type u) [CommRing k] (μ₁ : k) : ConicAlgebra k (Cay₂ k μ₁)

The conic structure on Cay₂, i.e. GPR 18.4 applied to the base ring.

Equations

• ConicAlgebra.cay₂ k μ₁ = (ConicAlgebra.baseRing k).cay μ₁

@[instance_reducible]

noncomputable instance ConicAlgebra.instCommRingCay₂ (k : Type u) [CommRing k] (μ₁ : k) : CommRing (Cay₂ k μ₁)

Cay₂ is commutative: the conjugation of the base ring is the identity (ConicAlgebra.baseRing_conj_apply), which is exactly the hypothesis of ConicAlgebra.mul_comm_cay. This is the last commutative rung.

Equations

• ConicAlgebra.instCommRingCay₂ k μ₁ = ConicAlgebra.Cay.commRing (ConicAlgebra.baseRing k) μ₁ ⋯

@[instance_reducible]

noncomputable instance ConicAlgebra.instAlgebraCay₂ (k : Type u) [CommRing k] (μ₁ : k) : Algebra k (Cay₂ k μ₁)

Equations

• ConicAlgebra.instAlgebraCay₂ k μ₁ = ConicAlgebra.Cay.algebra (ConicAlgebra.baseRing k) μ₁ ⋯

theorem ConicAlgebra.conjIsInvolution_cay₂ (k : Type u) [CommRing k] (μ₁ : k) : (cay₂ k μ₁).ConjIsInvolution

theorem ConicAlgebra.isMultiplicative_cay₂ (k : Type u) [CommRing k] (μ₁ : k) : (cay₂ k μ₁).IsMultiplicative

The rank-2 norm is multiplicative: GPR Exc. 18.18 applied to the base ring, which is associative with multiplicative norm.

Rank 4

@[reducible, inline]

abbrev ConicAlgebra.Cay₄ (k : Type u) [CommRing k] (μ₁ μ₂ : k) : Type u

The rank-4 Cayley–Dickson algebra Cay(Cay(k, μ₁), μ₂) — a quaternion algebra.

⚠ Not mathlib's QuaternionAlgebra; see the module docstring.

Equations

• ConicAlgebra.Cay₄ k μ₁ μ₂ = (ConicAlgebra.cay₂ k μ₁).Cay μ₂

@[reducible, inline]

noncomputable abbrev ConicAlgebra.cay₄ (k : Type u) [CommRing k] (μ₁ μ₂ : k) : ConicAlgebra k (Cay₄ k μ₁ μ₂)

The conic structure on Cay₄.

Equations

• ConicAlgebra.cay₄ k μ₁ μ₂ = (ConicAlgebra.cay₂ k μ₁).cay μ₂

@[instance_reducible]

noncomputable instance ConicAlgebra.instRingCay₄ (k : Type u) [CommRing k] (μ₁ μ₂ : k) : Ring (Cay₄ k μ₁ μ₂)

Cay₄ is associative, by GPR 18.14(b) applied to the commutative Cay₂. It is the last associative rung, which is why the tower produces composition algebras only up to rank 8.

Equations

• ConicAlgebra.instRingCay₄ k μ₁ μ₂ = ConicAlgebra.Cay.ring (ConicAlgebra.cay₂ k μ₁) μ₂ ⋯

@[instance_reducible]

noncomputable instance ConicAlgebra.instAlgebraCay₄ (k : Type u) [CommRing k] (μ₁ μ₂ : k) : Algebra k (Cay₄ k μ₁ μ₂)

Equations

• ConicAlgebra.instAlgebraCay₄ k μ₁ μ₂ = ConicAlgebra.Cay.algebra (ConicAlgebra.cay₂ k μ₁) μ₂ ⋯

theorem ConicAlgebra.conjIsInvolution_cay₄ (k : Type u) [CommRing k] (μ₁ μ₂ : k) : (cay₄ k μ₁ μ₂).ConjIsInvolution

theorem ConicAlgebra.isMultiplicative_cay₄ (k : Type u) [CommRing k] (μ₁ μ₂ : k) : (cay₄ k μ₁ μ₂).IsMultiplicative

Rank 8: octonion algebras

@[reducible, inline]

abbrev ConicAlgebra.Cay₈ (k : Type u) [CommRing k] (μ₁ μ₂ μ₃ : k) : Type u

The rank-8 Cayley–Dickson algebra Cay(Cay(Cay(k, μ₁), μ₂), μ₃): an octonion algebra. mathlib has no octonions, so this is the definition of record here.

Equations

• ConicAlgebra.Cay₈ k μ₁ μ₂ μ₃ = (ConicAlgebra.cay₄ k μ₁ μ₂).Cay μ₃

@[reducible, inline]

noncomputable abbrev ConicAlgebra.cay₈ (k : Type u) [CommRing k] (μ₁ μ₂ μ₃ : k) : ConicAlgebra k (Cay₈ k μ₁ μ₂ μ₃)

The conic structure on Cay₈.

Equations

• ConicAlgebra.cay₈ k μ₁ μ₂ μ₃ = (ConicAlgebra.cay₄ k μ₁ μ₂).cay μ₃

@[reducible, inline]

abbrev ConicAlgebra.Octonion (k : Type u) [CommRing k] (μ₁ μ₂ μ₃ : k) : Type u

The underlying module of an octonion algebra, under its usual name.

Equations

• ConicAlgebra.Octonion k μ₁ μ₂ μ₃ = ConicAlgebra.Cay₈ k μ₁ μ₂ μ₃

@[reducible, inline]

noncomputable abbrev ConicAlgebra.octonion (k : Type u) [CommRing k] (μ₁ μ₂ μ₃ : k) : ConicAlgebra k (Octonion k μ₁ μ₂ μ₃)

An octonion algebra, under its usual name.

Equations

• ConicAlgebra.octonion k μ₁ μ₂ μ₃ = ConicAlgebra.cay₈ k μ₁ μ₂ μ₃

theorem ConicAlgebra.conjIsInvolution_cay₈ (k : Type u) [CommRing k] (μ₁ μ₂ μ₃ : k) : (cay₈ k μ₁ μ₂ μ₃).ConjIsInvolution

instance ConicAlgebra.isAlternative_cay₈ (k : Type u) [CommRing k] (μ₁ μ₂ μ₃ : k) : IsAlternative (Cay₈ k μ₁ μ₂ μ₃)

Octonion algebras are alternative — GPR 18.14(c) applied to the associative Cay₄.

This is a direct proof, independent of GPR 19.3: it needs no regularity of the norm, no hypothesis on 2, and no hypothesis on the μᵢ, whereas the general ConicAlgebra.IsComposition.isAlternative needs the norm's radical to vanish.

theorem ConicAlgebra.isMultiplicative_cay₈ (k : Type u) [CommRing k] (μ₁ μ₂ μ₃ : k) : (cay₈ k μ₁ μ₂ μ₃).IsMultiplicative

The octonion norm permits composition, n(xy) = n(x)n(y) — GPR Exc. 18.18 applied to the associative Cay₄. Again no hypothesis on 2 or on the μᵢ.

This is the last rung covered uniformly by the associative-input theorem used here. For a further double, GPR Exc. 18.18 gives the sharp criterion μ₄[B, B, B] ⊆ Rad(Dn_B). Non-associativity alone does not force failure of norm multiplicativity; the criterion is automatic when μ₄ = 0.

The ranks are 2, 4, 8

ConicAlgebra.Cay.finrank_cay doubles the rank at each step, starting from finrank k k = 1. These need k nontrivial (otherwise finrank is 0 throughout) but nothing else — no unit scalars, no hypothesis on 2, and no composition.

@[simp]

theorem ConicAlgebra.finrank_cay₂ (k : Type u) [CommRing k] (μ₁ : k) [Nontrivial k] : Module.finrank k (Cay₂ k μ₁) = 2

@[simp]

theorem ConicAlgebra.finrank_cay₄ (k : Type u) [CommRing k] (μ₁ μ₂ : k) [Nontrivial k] : Module.finrank k (Cay₄ k μ₁ μ₂) = 4

@[simp]

theorem ConicAlgebra.finrank_cay₈ (k : Type u) [CommRing k] (μ₁ μ₂ μ₃ : k) [Nontrivial k] : Module.finrank k (Cay₈ k μ₁ μ₂ μ₃) = 8

An octonion algebra has rank 8.

The tower consists of composition algebras

Here, and only here, the scalars must be units and 2 must be invertible. The hypothesis on 2 is what turns non-singularity of each norm into the regularity that ConicAlgebra.IsComposition.cay consumes; without it the very first rung already fails, since Cay(k, μ) in characteristic 2 is inseparable and not a composition algebra.

theorem ConicAlgebra.isComposition_cay₂ (k : Type u) [CommRing k] (μ₁ : k) [Invertible 2] (h₁ : IsUnit μ₁) : (cay₂ k μ₁).IsComposition

theorem ConicAlgebra.isComposition_cay₄ (k : Type u) [CommRing k] (μ₁ μ₂ : k) [Invertible 2] (h₁ : IsUnit μ₁) (h₂ : IsUnit μ₂) : (cay₄ k μ₁ μ₂).IsComposition

theorem ConicAlgebra.isComposition_cay₈ (k : Type u) [CommRing k] (μ₁ μ₂ μ₃ : k) [Invertible 2] (h₁ : IsUnit μ₁) (h₂ : IsUnit μ₂) (h₃ : IsUnit μ₃) : (cay₈ k μ₁ μ₂ μ₃).IsComposition

An octonion algebra with unit scalars, over a base in which 2 is invertible, is a composition algebra.