The Cayley–Dickson doubling, internally

Let C be a Euclidean composition algebra, A ⊆ C a composition subalgebra (a submodule containing 1 and closed under multiplication and conjugation), and u ⊥ A a unit vector. This file proves the three multiplication rules that make A ⊕ A u the Cayley–Dickson double of A:

• mul_mul_unit — a (b u) = (b a) u
• unit_mul_mul — (a u) b = (a b*) u
• unit_mul_unit — (a u)(b u) = -(b* a)

together with the orthogonality ip_mul_unit (⟪a u, b⟫ = 0) that makes the sum direct.

Why this file is not the plan's Composition/CayleyDickson.lean

The build plan proposed constructing CD C := C × C as a new algebra and then transporting it into C. That is not what Hurwitz's argument needs and it is the expensive half: it means building a second NonAssocRing instance, a second form, and an isomorphism onto a subalgebra. Everything downstream instead needs the doubling inside C, where the composition law is already available and where A ⊕ A u is a submodule rather than a new type. So the doubling is done internally, and no CD type former is built.

★ The rules need no associativity of A. The plan's §6 flagged the termination step ("the doubling stops at dimension 8 because CD D composes only when D is associative") as the one it had not written out to the level where a Lean gap would show. It was right to flag it, and the shape of the gap is this: the three rules above hold for any composition subalgebra A, associative or not, so closure of A ⊕ A u is not where the dimension bound comes from. What associativity actually gates is the norm on A ⊕ A u, and inside C the norm is multiplicative for free. The bound therefore arrives as a contrapositive — if A is not associative there is no unit vector orthogonal to it at all — which is Composition/Hurwitz.lean, not this file.

Main statements

The named results are the four listed above plus their inputs: cstar_mul_mul (x* (x y) = N x • y) and mul_mul_cstar ((y x) x* = N x • y) with their polarisations cstar_mul_mul_polar / mul_mul_cstar_polar, and the two commutation rules unit_comm (a u = u a*) and unit_mul_left (u (a* y) = a (u y)).

Scope

Substrate for the two Hurwitz theorems. It states neither of them.

The two Kirmse identities and their polarisations

theorem CompositionAlgebra.cstar_mul_mul {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y : C) : cstar x * (x * y) = nf x • y

x* (x y) = N x • y. Immediate from left alternativity and sq_eq.

theorem CompositionAlgebra.mul_mul_cstar {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y : C) : y * x * cstar x = nf x • y

(y x) x* = N x • y. Immediate from right alternativity and sq_eq.

theorem CompositionAlgebra.cstar_mul_mul_polar {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x w y : C) : cstar x * (w * y) + cstar w * (x * y) = (2 * ip x w) • y

Polarisation of cstar_mul_mul: x* (w y) + w* (x y) = 2⟪x,w⟫ • y.

theorem CompositionAlgebra.mul_mul_cstar_polar {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x w y : C) : y * x * cstar w + y * w * cstar x = (2 * ip x w) • y

Polarisation of mul_mul_cstar: (y x) w* + (y w) x* = 2⟪x,w⟫ • y.

Composition subalgebras

structure CompositionAlgebra.IsCompSubalgebra {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (A : Submodule ℝ C) : Prop

A composition subalgebra: a submodule containing the unit and closed under the product and the conjugation. Its own composition law is inherited from C.

• one_mem : 1 ∈ A

  The subalgebra contains the unit.

• mul_mem ⦃a : C⦄ : a ∈ A → ∀ ⦃b : C⦄, b ∈ A → a * b ∈ A

  The subalgebra is closed under multiplication.

• cstar_mem ⦃a : C⦄ : a ∈ A → cstar a ∈ A

  The subalgebra is closed under conjugation.

theorem CompositionAlgebra.IsCompSubalgebra.isPure_unit {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {A : Submodule ℝ C} (hA : IsCompSubalgebra A) {u : C} (hu : ∀ a ∈ A, ip u a = 0) : IsPure u

The doubling vector is imaginary: it is orthogonal to 1 ∈ A.

theorem CompositionAlgebra.IsCompSubalgebra.unit_sq {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {A : Submodule ℝ C} (hA : IsCompSubalgebra A) {u : C} (hu : ∀ a ∈ A, ip u a = 0) (hnu : nf u = 1) : u * u = -1

u * u = -1.

theorem CompositionAlgebra.IsCompSubalgebra.ip_mul_unit {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {A : Submodule ℝ C} (hA : IsCompSubalgebra A) {u : C} (hu : ∀ a ∈ A, ip u a = 0) {a : C} (ha : a ∈ A) {b : C} (hb : b ∈ A) : ip (a * u) b = 0

A ⊥ A u: the doubled part is orthogonal to the original. This is what makes the sum A ⊕ A u direct.

theorem CompositionAlgebra.IsCompSubalgebra.isPure_mul_unit {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {A : Submodule ℝ C} (hA : IsCompSubalgebra A) {u : C} (hu : ∀ a ∈ A, ip u a = 0) {a : C} (ha : a ∈ A) : IsPure (a * u)

Every element of A u is imaginary.

theorem CompositionAlgebra.IsCompSubalgebra.unit_comm {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {A : Submodule ℝ C} (hA : IsCompSubalgebra A) {u : C} (hu : ∀ a ∈ A, ip u a = 0) {a : C} (ha : a ∈ A) : a * u = u * cstar a

a u = u a* for a ∈ A: the doubling vector conjugates A.

theorem CompositionAlgebra.IsCompSubalgebra.unit_mul_left {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) {a : C} (ha : a ∈ A) (y : C) : u * (cstar a * y) = a * (u * y)

u (a* y) = a (u y) for a ∈ A: moving A across the doubling vector on the left.

theorem CompositionAlgebra.IsCompSubalgebra.mul_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) {a : C} (ha : a ∈ A) {b : C} (hb : b ∈ A) : a * (b * u) = b * a * u

First Cayley–Dickson rule: a (b u) = (b a) u.

theorem CompositionAlgebra.IsCompSubalgebra.unit_mul_mul {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) (a : C) {b : C} (hb : b ∈ A) : a * u * b = a * cstar b * u

Second Cayley–Dickson rule: (a u) b = (a b*) u. Note a is arbitrary: only b ∈ A is used.

theorem CompositionAlgebra.IsCompSubalgebra.ip_unit_mul_unit {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {u : C} (hnu : nf u = 1) (b : C) : ip u (b * u) = ip 1 b

⟪u, b u⟫ = ⟪1, b⟫.

theorem CompositionAlgebra.IsCompSubalgebra.unit_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) : a * u * (b * u) = -(cstar b * a)

Third Cayley–Dickson rule: (a u)(b u) = -(b* a).