The Moufang identities and Artin's theorem for the double of the quaternions #

The Cayley–Dickson double CayleyDickson ℍ[R] of the quaternions over a commutative ring R, the octonions when R = ℝ, is not associative, but it is alternative: the left and right alternative laws and the flexible law of TauCeti.Algebra.CayleyDickson.Quaternion say that the associator (a * b) * c - a * (b * c) vanishes whenever two of its arguments are equal. This file proves the two standard consequences of alternativity for this algebra.

The three Moufang identities (z * x * z) * y = z * (x * (z * y)), x * (z * y * z) = ((x * z) * y) * z and (z * x) * (y * z) = (z * (x * y)) * z.
Artin's theorem: any two elements x and y generate an associative subalgebra. Here the subalgebra generated by x and y is NonUnitalAlgebra.adjoin R {1, x, y}, the smallest subalgebra containing the unit, x and y. It is the span of 1, x, y and x * y, and it is closed under conjugation by TauCeti.CayleyDickson.star_mem_of_one_mem.

Main results #

TauCeti.CayleyDickson.moufang_left, TauCeti.CayleyDickson.moufang_right and TauCeti.CayleyDickson.moufang_middle: the Moufang identities.
TauCeti.CayleyDickson.associator_swap_left and TauCeti.CayleyDickson.associator_swap_right: the associator is alternating, so it changes sign when two arguments are swapped.
TauCeti.CayleyDickson.adjoin_toSubmodule_eq_span: the subalgebra generated by x and y is the span of 1, x, y and x * y.
TauCeti.CayleyDickson.mul_assoc_of_mem_adjoin: Artin's theorem, the subalgebra generated by two elements is associative.

Implementation notes #

Nothing here is proved in coordinates beyond the alternative laws and the rank-two equation of TauCeti.Algebra.CayleyDickson.Quaternion: expanding a Moufang identity into the eight coordinates gives polynomials of degree four that are expensive to normalize. Instead the antisymmetry of the associator is the linearization of the alternative laws, and the Moufang identities come from the Teichmüller identity associator_cocycle of Mathlib. At z, z, x, y it gives associator z (z * x) y = star z * associator z x y, because z * z is a combination of z and 1. The left Moufang identity is the sum of two such terms with opposite signs, the middle one follows in the same way after y * z is traded for z * y, and the right one is the left one read through the involution, which reverses products.

For Artin's theorem, the span of 1, x, y and x * y is closed under multiplication because every element is a root of its rank-two equation a * a = T a • a - N a • 1. This equation reduces x * x and y * y, and at x + y it writes y * x in terms of x * y; the alternative and flexible laws then reduce the products of x * y with x and y. The associator is linear in each argument (TauCeti.associator_eq_zero_of_mem_span), so it is enough that it vanishes on triples from 1, x, y and x * y. Being alternating, it vanishes on a triple with a repeated entry, and the only remaining triples are the permutations of (x, x * y, y). On that one the left and right alternative laws give (x * (x * y)) * y = (x * x) * (y * y) = x * ((x * y) * y).

References #

R. D. Schafer, An Introduction to Nonassociative Algebras, Academic Press (1966), Chapter III, for alternative algebras, the Moufang identities and Artin's theorem.
T. A. Springer and F. D. Veldkamp, Octonions, Jordan Algebras and Exceptional Groups, Springer (2000), Chapter 1, for the Moufang identities in composition algebras.