Documentation

LeanPool.CompositionAlgebrasOverRings.Conic.CayleyDicksonMultiplicative

The double of an associative multiplicative conic algebra is multiplicative (GPR Exc. 18.18) #

If B is associative with a multiplicative norm, then Cay(B, μ) has a multiplicative norm. This is the associative special case of GPR Exc. 18.18: for multiplicative B, the sharp criterion is μ[B, B, B] ⊆ Rad(Dn_B), which is not proved here. In particular, μ = 0 does not require associativity. The sufficient case proved here carries n(xy) = n(x)n(y) up the usual tower k → k[√·] → ℍ → 𝕆. The sedenion non-example is treated separately (GPR 19.23, Layer 8).

The computation #

Write x = u₁ + v₁ j, y = u₂ + v₂ j. Expanding

n(xy) = n_B(u₁u₂ + μ (conj v₂)v₁) - μ n_B(v₂u₁ + v₁(conj u₂))

with n_B multiplicative and n_B(conj z) = n_B(z) leaves exactly the terms of n(x)n(y) = (n_B(u₁) - μ n_B(v₁))(n_B(u₂) - μ n_B(v₂)), plus

μ · [ n_B(u₁u₂, (conj v₂)v₁) - n_B(v₂u₁, v₁(conj u₂)) ].

So everything reduces to the vanishing of that bracket, polar_shuffle below. That is where associativity of B is spent, and it is spent exactly once: the two polar terms are moved onto a common form by the two halves of norm-associativity (ConicAlgebra.IsMultiplicative.polar_mul_left and .polar_mul_right), and what stands between them is v₂(u₁u₂) = (v₂u₁)u₂.

⚠ No hypothesis is needed on the conjugation of B — unlike ConicAlgebra.isAlternative_cay, which needs it to be an involution. Only conj (conj z) = z is used, and that holds in every conic algebra (ConicAlgebra.conj_conj). Nor is anything needed on μ, on 2, or on the module underlying B.

Main results #

References #

source
theorem ConicAlgebra.isMultiplicative_cay {k : Type u} {B : Type v} [CommRing k] [Ring B] [Algebra k B] (C : ConicAlgebra k B) (μ : k) (h : C.IsMultiplicative) :
(C.cay μ).IsMultiplicative

GPR Exc. 18.18, ⇐. If B is associative and its norm is multiplicative, then the norm of Cay(B, μ) is multiplicative, for every scalar μ.

This sufficient result constructs multiplicative norms on ℍ and 𝕆 from associative inputs. It gives no converse for a non-associative input: further norm multiplicativity is governed by the radical criterion of GPR Exc. 18.18, which is automatic for μ = 0. Multiplicativity alone does not establish that the double is a composition algebra.