The double is alternative exactly when the base is associative (GPR 18.14(c))

Cay(B, μ) is alternative if and only if B is associative and the conjugation of B is an involution (GPR 18.14(c)). Both directions are proved here, for every scalar μ and with no hypothesis on B beyond the conic structure.

The direction ⇐ is the one that builds algebras: octonions from quaternions, quaternions from quadratic étale algebras. The direction ⇒ is what stops the tower — it is the source of the rank dichotomy 1, 2, 4, 8 (GPR 19.18), since the fourth double is alternative only if the third is associative, which it is not.

The hypotheses of ⇐

Both are needed, and neither is free:

• B associative, as the explicit hypothesis ∀ a b c : B, a * b * c = a * (b * c) rather than a Ring B instance, so that the same statement serves both directions of the equivalence: the converse produces associativity of a B that is only a NonAssocRing, and cannot produce an instance. ConicAlgebra.isAlternative_cay below is the [Ring B] [Algebra k B] form, which is what the Cayley–Dickson tower consumes.
• The conjugation of B is an involution (ConicAlgebra.ConjIsInvolution). This does not follow from associativity over an arbitrary base — Conic/TraceDefectCounterexample.lean is an associative conic algebra whose conjugation is not an anti-homomorphism — but it does hold as soon as B is finitely generated projective (ConicAlgebra.conjIsInvolution_of_projective) or the base is a field (ConicAlgebra.conj_mul).

μ remains an arbitrary scalar, in both directions. In particular the converse needs no unit hypothesis: it reads off the two conclusions from products in which every μ has already cancelled.

The proof of ⇐

Write x = a + bj, y = c + dj. Expanding the two alternative laws in components and using only

• associativity of B,
• anti-multiplicativity of the conjugation,
• conj z = t(z) · 1 - z (ConicAlgebra.conj_apply), which turns every conjugate into a scalar multiple of 1 minus the element, and
• z² = t(z) · z - n(z) · 1 (ConicAlgebra.mul_self_eq) for z = a and z = b,

turns each of the four component identities into an identity between k-linear combinations of the same products, which module closes. This is GPR's "lengthy but straightforward computation" of GPR 18.13 specialized to u₁ = u₂, v₁ = v₂; here it is a single simp only with a normalizing rewrite set, because eliminating the conjugation first makes all the cancellations linear.

The proof of ⇒

Each conclusion is one component of one instance of one alternative law, so neither uses the other, and neither uses μ.

• Involutivity is the j-component of left alternativity at x = a + j, y = c:

  (conj c) a + conj(ac) = t(a) (conj c),

and t(a) (conj c) - (conj c) a = (conj c) (conj a). The element b multiplying the conjugate in the general computation is here specialized to 1, which is what makes the defect visible without any faithfulness hypothesis: GPR 16.10(a) only places the trace defect in Ann(B), but B is unital, so it vanishes.

• Associativity is the j-component of the linearized right alternative law (IsAlternative.right_alt_linearized) at x = a, y = b, z = cj:

  a(bc) + (ab)(conj c) = (ac)b + (a(conj c))b,

  in which expanding conj c = t(c) · 1 - c cancels both the trace terms and the two products that are not associated, leaving abc = a(bc). Note that this is the linearization, not either alternative law itself: the plain laws applied to elements of these shapes give back only alternativity of B and the commutator identity, never associativity.

Implementation notes

⚠ The elements (a, 1), (0, c) and friends must be introduced opaquely — as local constants of type Cay C μ whose components are fixed by hypotheses — and not as pair literals ascribed to Cay C μ. A literal ((a, 1) : Cay C μ) still elaborates with inferred type B × B, so ConicAlgebra.Cay.fst_mul and ConicAlgebra.Cay.snd_mul, whose implicit C and μ are determined only by that type, no longer unify and every rewrite silently fails.

Main results

• ConicAlgebra.isAlternative_cay_iff : GPR 18.14(c), the equivalence.
• ConicAlgebra.isAlternative_cay_of_mul_assoc, ConicAlgebra.isAlternative_cay : the direction ⇐, the second in the [Ring B] form the tower uses.
• ConicAlgebra.mul_assoc_of_isAlternative_cay, ConicAlgebra.conjIsInvolution_of_isAlternative_cay : the two halves of ⇒.
• ConicAlgebra.not_isAlternative_cay_of_mul_mul_ne : the contrapositive, in the form a non-associativity witness for B consumes.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 18.13, 18.14(c).

The double of an associative algebra is alternative

theorem ConicAlgebra.isAlternative_cay_of_mul_assoc {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] (C : ConicAlgebra k B) (μ : k) (hassoc : ∀ (a b c : B), a * b * c = a * (b * c)) (hconj : C.ConjIsInvolution) : IsAlternative (C.Cay μ)

GPR 18.14(c), ⇐. If B is associative and its conjugation is an involution, then Cay(B, μ) is alternative, for every scalar μ.

Stated with associativity as a hypothesis rather than an instance, so that it can be paired with ConicAlgebra.mul_assoc_of_isAlternative_cay into the equivalence ConicAlgebra.isAlternative_cay_iff. For an associative B use ConicAlgebra.isAlternative_cay, which takes mul_assoc from the instance.

The base of an alternative double is associative with involutive conjugation

theorem ConicAlgebra.conjIsInvolution_of_isAlternative_cay {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] (C : ConicAlgebra k B) (μ : k) (h : IsAlternative (C.Cay μ)) : C.ConjIsInvolution

GPR 18.14(c), ⇒, first half. If Cay(B, μ) is alternative then the conjugation of B is an involution.

The j-component of left alternativity at x = a + j and y = c reads (conj c) a + conj(ac) = t(a) (conj c), and t(a) (conj c) - (conj c) a is (conj c) (conj a) by ConicAlgebra.conj_apply. No hypothesis on μ, and no associativity of B: taking the j-part of x to be 1 removes every product in which μ or a reassociation could appear.

theorem ConicAlgebra.mul_assoc_of_isAlternative_cay {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] (C : ConicAlgebra k B) (μ : k) (h : IsAlternative (C.Cay μ)) (a b c : B) : a * b * c = a * (b * c)

GPR 18.14(c), ⇒, second half. If Cay(B, μ) is alternative then B is associative.

The j-component of the linearized right alternative law at x = a, y = b, z = cj reads a(bc) + (ab)(conj c) = (ac)b + (a(conj c))b; expanding conj c = t(c) · 1 - c cancels the trace terms against the two products that are not associated. No hypothesis on μ: every product below has a zero component where μ would enter.

theorem ConicAlgebra.isAlternative_cay_iff {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] (C : ConicAlgebra k B) (μ : k) : IsAlternative (C.Cay μ) ↔ (∀ (a b c : B), a * b * c = a * (b * c)) ∧ C.ConjIsInvolution

GPR 18.14(c). The Cayley–Dickson double Cay(B, μ) is alternative exactly when B is associative and its conjugation is an involution — for every scalar μ.

theorem ConicAlgebra.not_isAlternative_cay_of_mul_mul_ne {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] (C : ConicAlgebra k B) (μ : k) {a b c : B} (hne : a * b * c ≠ a * (b * c)) : ¬IsAlternative (C.Cay μ)

The double of a non-associative algebra is not alternative. The contrapositive of ConicAlgebra.mul_assoc_of_isAlternative_cay, in the form that a single witness to the failure of associativity in B consumes: this is what makes the fourth Cayley–Dickson rung — the sedenions, GPR 19.23 — fail to be alternative, and hence fail to be a composition algebra.

The associative case

The form the Cayley–Dickson tower consumes: B associative as an instance, which is what Conic/CayleyDicksonAssociative.lean supplies for a double.

theorem ConicAlgebra.isAlternative_cay {k : Type u} {B : Type v} [CommRing k] [Ring B] [Algebra k B] (C : ConicAlgebra k B) (μ : k) (hconj : C.ConjIsInvolution) : IsAlternative (C.Cay μ)

GPR 18.14(c), ⇐, for an associative B. If the conjugation of an associative conic algebra B is an involution, then Cay(B, μ) is alternative, for every scalar μ.