Documentation

LeanPool.CompositionAlgebrasOverRings.Composition.Sedenion

The sedenions: a conic algebra that is not a composition algebra (GPR 19.23) #

The fourth rung of the Cayley–Dickson tower, Cay(𝕆, μ) of rank 16, is a conic algebra — the doubling construction has no hypotheses at all — but it is not a composition algebra. This is the example that shows the tower really does stop, rather than merely resisting the theorems that built it.

Three separate statements are proved, in increasing strength:

Two independent routes #

The first two statements go through alternativity: 𝕆 is not associative (ConicAlgebra.exists_mul_mul_ne_mul_mul_realOctonion), so Cay(𝕆, μ) is not alternative (ConicAlgebra.not_isAlternative_cay_of_mul_mul_ne), and over a field every composition algebra is alternative (GPR 19.3). This is the route GPR takes.

The third goes through the rank: 16 ∉ {1, 2, 4, 8}. It is strictly stronger — it rules out every conic norm on the underlying module at once, rather than the one that doubling produces — and it needs no witness and no computation with associators.

Inverses without division #

Separately, the sedenions are the example of GPR Exc. 19.29(e): their norm is positive definite, so every nonzero sedenion has a two-sided inverse, yet they have explicit zero divisors and so are not a division algebra in the sense of GPR 8.6. This separates ConicAlgebra.HasTwoSidedInverses from IsDivision, and shows that the alternativity hypothesis of GPR 13.8 cannot be dropped.

That the norm is non-singular is what makes the second statement sharp. A conic algebra can fail to be a composition algebra because its norm is degenerate (GPR 19.4 in characteristic two is that example, with an identically zero polar form); the sedenions fail for the opposite reason. Their norm is the sixteen-fold orthogonal sum of ⟨1⟩ over ℝ, as non-singular as a form can be, and what fails is n(xy) = n(x)n(y). This is the converse half of GPR Exc. 18.18 in this one instance, obtained without proving that converse in general.

Main results #

References #

The general statement over a field #

source
theorem ConicAlgebra.IsComposition.not_cay_of_mul_mul_ne {F : Type u} {B : Type v} [Field F] [NonAssocRing B] [Module F B] [SMulCommClass F B B] [IsScalarTower F B B] [Module.Finite F B] [Module.Projective F B] (C : ConicAlgebra F B) (μ : F) {a b c : B} (hne : a * b * c ≠ a * (b * c)) :
¬(C.cay μ).IsComposition

The double of a non-associative conic algebra over a field is not a composition algebra.

ConicAlgebra.not_isAlternative_cay_of_mul_mul_ne — the converse half of GPR 18.14(c) — says the double is not alternative, and over a field every composition algebra is alternative (GPR 19.3, ConicAlgebra.IsComposition.isAlternative). No hypothesis on μ.

The sedenions over ℝ #

source
@[reducible, inline]
abbrev ConicAlgebra.RealSedenion :
Type

The real sedenions, Cay(𝕆, -1): the fourth rung of the Cayley–Dickson tower over ℝ, of dimension 16.

Equations
Instances For
    source
    @[reducible, inline]
    noncomputable abbrev ConicAlgebra.realSedenion :
    ConicAlgebra ℝ RealSedenion

    The conic structure on the sedenions. Doubling needs no hypotheses, so this exists exactly as the earlier rungs do; what fails is everything after GPR 18.4.

    Equations
    Instances For
      source
      theorem ConicAlgebra.finrank_realSedenion :
      Module.finrank ℝ RealSedenion = 16

      The sedenions have dimension 16.

      source
      theorem ConicAlgebra.not_isAlternative_realSedenion :
      ¬IsAlternative RealSedenion

      The sedenions are not alternative. 𝕆 is not associative, and by the converse half of GPR 18.14(c) that is exactly the obstruction.

      source
      theorem ConicAlgebra.isGPRNonsingular_realSedenion :
      realSedenion.norm.IsGPRNonsingular

      The sedenion norm is non-singular. It is n_𝕆 ⊥ ⟨1⟩ n_𝕆, and GN (C.8.3) builds non-singularity of an orthogonal sum out of regularity of the first summand — which the octonion norm has, since 2 is invertible in ℝ.

      This is what makes ConicAlgebra.not_isMultiplicative_realSedenion sharp: the sedenions are not a composition algebra because composition fails, not because the norm degenerates.

      source
      theorem ConicAlgebra.not_isMultiplicative_realSedenion :
      ¬realSedenion.IsMultiplicative

      GPR 19.23. The sedenion norm does not permit composition: n(xy) = n(x)n(y) fails.

      Its norm is non-singular, so were it multiplicative the sedenions would be a composition algebra of dimension 16, which GPR 19.18 forbids. This is the converse half of GPR Exc. 18.18 in this instance, obtained without proving that converse in general.

      source
      theorem ConicAlgebra.not_isComposition_realSedenion :
      ¬realSedenion.IsComposition

      The sedenions are not a composition algebra, for the conic structure the Cayley–Dickson process gives them.

      source
      theorem ConicAlgebra.not_isComposition_conicAlgebra_realSedenion (C : ConicAlgebra ℝ RealSedenion) :
      ¬C.IsComposition

      No conic structure on the sedenions is a composition algebra. The rank dichotomy GPR 19.18 rules out dimension 16 outright, for every choice of conic norm at once — this looks at the underlying module only, never at the multiplication.

      GPR Exc. 19.29(e): inverses without division #

      The sedenion norm is positive definite, so every nonzero sedenion x has the two-sided inverse n(x)⁻¹ (conj x); yet the sedenions have zero divisors, so they are not a division algebra in the sense of GPR 8.6. This is the example separating ConicAlgebra.HasTwoSidedInverses from IsDivision, and it is why GPR 13.8 needs alternativity.

      The zero divisors are explicit. Write e₀, …, e₁₅ for the coordinate basis of Cay(Cay(Cay(Cay(ℝ, -1), -1), -1), -1), numbering the two components u, v of u + v j at each level as the lower and upper half; then (e₄ + e₉)(e₇ + e₁₀) = 0.

      source
      theorem ConicAlgebra.posDef_realSedenion :
      QuadraticMap.PosDef realSedenion.norm

      The norm of the real sedenions is positive definite — the sum of sixteen squares. Doubling at a negative scalar preserves positive definiteness (ConicAlgebra.PosDef.cay).

      source
      theorem ConicAlgebra.hasTwoSidedInverses_realSedenion :
      realSedenion.HasTwoSidedInverses

      Every nonzero sedenion has a two-sided inverse, n(x)⁻¹ (conj x), since the norm is anisotropic.

      source
      theorem ConicAlgebra.exists_mul_eq_zero_realSedenion :
      ∃ (x : RealSedenion) (y : RealSedenion), x ≠ 0 ∧ y ≠ 0 ∧ x * y = 0

      The real sedenions have zero divisors: (e₄ + e₉)(e₇ + e₁₀) = 0, in the coordinates described above. The product is checked coordinate by coordinate.

      source
      theorem ConicAlgebra.not_isDivision_realSedenion :
      ¬IsDivision RealSedenion

      GPR Exc. 19.29(e): the real sedenions are not a division algebra in the sense of GPR 8.6, although their norm is anisotropic and every nonzero sedenion has a two-sided inverse (ConicAlgebra.hasTwoSidedInverses_realSedenion). So HasTwoSidedInverses is strictly weaker than IsDivision, and the alternativity hypothesis of GPR 13.8 (ConicAlgebra.isDivision_iff_hasTwoSidedInverses) cannot be dropped.