Alternative rings and algebras

An alternative multiplication satisfies the two alternative laws

• left alternative a * (a * b) = (a * a) * b
• right alternative (b * a) * a = b * (a * a)

Every associative multiplication is alternative; the octonions are the standard non-associative example. Alternativity is the structural hypothesis under which composition algebras live (GPR 19.3: every composition algebra is alternative).

Implementation notes

IsAlternative is a Prop-valued mixin on [Mul α], following IsJordan in Mathlib.Algebra.Jordan.Basic. It deliberately does not bundle the ring structure:

• the axioms are multiplicative equations and need neither addition nor negation, so [Mul α] is the honest hypothesis;
• bundling would fuse "is a non-associative ring" with "satisfies the alternative laws", which overview §2 forbids — algebra structure, norm regularity and module regularity are independent axes;
• a bundled class carrying its own NonAssocRing parent diamonds against ConicAlgebra's [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] (mathlib's Algebra requires an associative Semiring), making IsComposition → IsAlternative awkward to state.

One instance (Semigroup.isAlternative) covers every associative case, mirroring CommSemigroup.isCommJordan.

The associator characterizations live below [NonUnitalNonAssocRing α], where subtraction exists.

⚠ The linearizations are proved using additivity only — no Invertible 2 — so they hold in characteristic 2. Do not "simplify" them by halving.

Main results

• IsAlternative : the mixin.
• IsAlternative.associator_self_left/right/mid : the associator vanishes on repeated arguments.
• IsAlternative.associator_swap_left/right : the associator is alternating.
• IsAlternative.flexible : (a * b) * a = a * (b * a).
• IsAlternative.left_alt_linearized, right_alt_linearized : the linearized laws.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 13.2.
• Schafer, An Introduction to Nonassociative Algebras, §3.
• Zhevlakov et al., Rings That Are Nearly Associative, Ch. 2.

class IsAlternative (α : Type u) [Mul α] : Prop

An alternative multiplication: the associator vanishes whenever two adjacent arguments coincide. Stated on [Mul α] as a Prop mixin, following IsJordan.

• left_alt (a b : α) : a * (a * b) = a * a * b

  Left alternative law: a * (a * b) = (a * a) * b.

• right_alt (a b : α) : b * a * a = b * (a * a)

  Right alternative law: (b * a) * a = b * (a * a).

theorem IsAlternative.mul_mul_self_left {α : Type u} [Mul α] [IsAlternative α] (a b : α) : a * (a * b) = a * a * b

theorem IsAlternative.mul_self_mul_right {α : Type u} [Mul α] [IsAlternative α] (a b : α) : b * a * a = b * (a * a)

@[instance 100]

instance Semigroup.isAlternative (α : Type u) [Semigroup α] : IsAlternative α

Every associative multiplication is alternative. This single instance replaces what a bundled hierarchy would need four instances for.

theorem IsAlternative.associator_self_left {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (a b : α) : associator a a b = 0

The associator vanishes when the first two arguments coincide.

theorem IsAlternative.associator_self_right {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (a b : α) : associator b a a = 0

The associator vanishes when the last two arguments coincide.

The associator is alternating

Linearizations of the two alternative laws. Additivity only — valid in characteristic 2.

theorem IsAlternative.associator_add_swap_left {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (a b c : α) : associator a b c + associator b a c = 0

Linearized left alternative law: ⁅a, b, c⁆ + ⁅b, a, c⁆ = 0.

theorem IsAlternative.associator_swap_left {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (a b c : α) : associator a b c = -associator b a c

Swapping the first two arguments negates the associator.

theorem IsAlternative.associator_add_swap_right {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (a b c : α) : associator a b c + associator a c b = 0

Linearized right alternative law: ⁅a, b, c⁆ + ⁅a, c, b⁆ = 0.

theorem IsAlternative.associator_swap_right {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (a b c : α) : associator a b c = -associator a c b

Swapping the last two arguments negates the associator.

theorem IsAlternative.associator_self_mid {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (a b : α) : associator a b a = 0

The associator vanishes when the first and third arguments coincide.

theorem IsAlternative.flexible {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (a b : α) : a * b * a = a * (b * a)

Flexible law: (a * b) * a = a * (b * a).

Linearized alternative laws, multiplicative form

theorem IsAlternative.left_alt_linearized {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (a b x : α) : a * (b * x) + b * (a * x) = a * b * x + b * a * x

a * (b * x) + b * (a * x) = (a * b) * x + (b * a) * x.

theorem IsAlternative.right_alt_linearized {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (x a b : α) : x * a * b + x * b * a = x * (a * b) + x * (b * a)

(x * a) * b + (x * b) * a = x * (a * b) + x * (b * a).

instance IsAlternative.instMulOpposite {α : Type u} [Mul α] [IsAlternative α] : IsAlternative αᵐᵒᵖ

The opposite of an alternative multiplication is alternative: the two laws swap.