Artin's theorem

Artin's theorem. A non-associative ring is alternative if and only if every subring generated by two elements is associative.

Proof strategy

The hard direction follows Schafer's proof of Theorem 3.1. First prove the result for non-associative monomials in the two generators, by strong induction on the sum of the three degrees. At a fixed induction stage every shorter monomial can be reassociated so that its first letter is exposed. Two of the three monomials begin with the same generator, and Schafer's linearized Moufang identity reduces their associator to associators of smaller total degree.

Finally, every element of NonUnitalSubring.closure {a, b} is an additive combination of such monomials. Trilinearity of the associator therefore extends the monomial result to the closure.

The reduction

The Teichmüller identity, mathlib's associator_cocycle, holds in any non-associative ring:

w * [x,y,z] - [wx, y, z] + [w, xy, z] - [w, x, yz] + [w,x,y] * z = 0

Say n is nuclear in S when [n, y, z] = 0 for all y, z ∈ S. If S is closed under multiplication, then the elements of S nuclear in S are closed under 0, +, - (associator additivity) and under * (Teichmüller — see IsNuclearIn.mul, where every term but [wx, y, z] vanishes). So the nucleus of S is a subring of S.

Consequently, if the generators a, b are nuclear in S = ⟨a, b⟩, the nucleus contains {a, b}, hence contains the whole closure, hence equals S — exactly associativity of S.

⚠ Note that none of this uses alternativity. Alternativity enters in the monomial argument that proves generators_nuclear.

References

• Schafer, An Introduction to Nonassociative Algebras, §3, Theorem 3.1.
• Zhevlakov, Slin'ko, Shestakov, Shirshov, Rings That Are Nearly Associative, ch. 2.
• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, Ch. 13.

Non-associative monomials

inductive NonAssocWord : Type

A nonempty, non-associatively parenthesized word in two letters.

• left : NonAssocWord
• right : NonAssocWord
• mul (p q : NonAssocWord) : NonAssocWord

def NonAssocWord.degree : NonAssocWord → ℕ

The number of letters in a non-associative word.

Equations

• NonAssocWord.left.degree = 1
• NonAssocWord.right.degree = 1
• (p.mul q).degree = p.degree + q.degree

def NonAssocWord.eval {α : Type u} [Mul α] (a b : α) : NonAssocWord → α

Evaluate a non-associative word at two elements.

Equations

• NonAssocWord.eval a b NonAssocWord.left = a
• NonAssocWord.eval a b NonAssocWord.right = b
• NonAssocWord.eval a b (p.mul q) = NonAssocWord.eval a b p * NonAssocWord.eval a b q

def NonAssocWord.ofBool : Bool → NonAssocWord

The one-letter word selected by a Boolean.

Equations

• NonAssocWord.ofBool false = NonAssocWord.left
• NonAssocWord.ofBool true = NonAssocWord.right

def NonAssocWord.letter {α : Type u} (a b : α) : Bool → α

The element selected by a Boolean.

Equations

• NonAssocWord.letter a b false = a
• NonAssocWord.letter a b true = b

@[simp]

theorem NonAssocWord.degree_pos (p : NonAssocWord) : 0 < p.degree

@[simp]

theorem NonAssocWord.degree_ofBool (x : Bool) : (ofBool x).degree = 1

@[simp]

theorem NonAssocWord.eval_ofBool {α : Type u} [Mul α] (a b : α) (x : Bool) : eval a b (ofBool x) = letter a b x

def NonAssocWord.prependEval {α : Type u} [Mul α] (a b : α) (x : Bool) : Option NonAssocWord → α

Evaluation of a word with its first letter exposed.

Equations

• NonAssocWord.prependEval a b x none = NonAssocWord.letter a b x
• NonAssocWord.prependEval a b x (some p) = NonAssocWord.letter a b x * NonAssocWord.eval a b p

def NonAssocWord.prependDegree : Option NonAssocWord → ℕ

Degree of a word with its first letter exposed.

Equations

• NonAssocWord.prependDegree none = 1
• NonAssocWord.prependDegree (some p) = p.degree + 1

def TwoGeneratedAssoc (α : Type u) [NonUnitalNonAssocRing α] : Prop

Two-generated associativity, as a predicate on a ring.

Equations

• TwoGeneratedAssoc α = ∀ (a b : α) {x y z : α}, x ∈ NonUnitalSubring.closure {a, b} → y ∈ NonUnitalSubring.closure {a, b} → z ∈ NonUnitalSubring.closure {a, b} → x * y * z = x * (y * z)

Nuclearity relative to a set

def IsNuclearIn {α : Type u} [NonUnitalNonAssocRing α] (S : Set α) (n : α) : Prop

n is nuclear in S if the associator vanishes whenever n occupies the first slot and the other two arguments lie in S.

In an alternative ring the associator is alternating, so this single condition is equivalent to nuclearity in any of the three slots (IsAlternative.associator_swap_left, IsAlternative.associator_swap_right). The proofs below need only the first-slot form.

Equations

• IsNuclearIn S n = ∀ y ∈ S, ∀ z ∈ S, associator n y z = 0

theorem IsNuclearIn.zero {α : Type u} [NonUnitalNonAssocRing α] {S : Set α} : IsNuclearIn S 0

theorem IsNuclearIn.add {α : Type u} [NonUnitalNonAssocRing α] {S : Set α} {m n : α} (hm : IsNuclearIn S m) (hn : IsNuclearIn S n) : IsNuclearIn S (m + n)

theorem IsNuclearIn.neg {α : Type u} [NonUnitalNonAssocRing α] {S : Set α} {m : α} (hm : IsNuclearIn S m) : IsNuclearIn S (-m)

theorem IsNuclearIn.mul {α : Type u} [NonUnitalNonAssocRing α] {S : Set α} {m n : α} (hS : ∀ x ∈ S, ∀ y ∈ S, x * y ∈ S) (hm : IsNuclearIn S m) (hn : IsNuclearIn S n) (_hmS : m ∈ S) (hnS : n ∈ S) : IsNuclearIn S (m * n)

The nucleus is closed under multiplication. This is the Teichmüller identity (associator_cocycle): with w = m and x = n, every term but [mn, y, z] vanishes.

Requires S closed under multiplication, and m, n ∈ S (not merely nuclear in S).

Easy direction

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

If every two-generated subring is associative, the left alternative law holds.

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

If every two-generated subring is associative, the right alternative law holds.

theorem IsAlternative.of_two_generated_assoc {α : Type u} [NonUnitalNonAssocRing α] (h : TwoGeneratedAssoc α) : IsAlternative α

Artin's theorem, easy direction: two-generated associativity implies alternativity.

Hard direction

The associator identities used by Schafer's induction

theorem IsAlternative.associator_mul_right_self {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (y x c : α) : associator y (x * c) x = -associator y x c * x

A form of the right Moufang identity used in the proof of Artin's theorem [Schafer, (3.7)].

theorem IsAlternative.associator_mul_right_self_linearized {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (y x z c : α) : associator y (x * c) z + associator y (z * c) x = -associator y x c * z - associator y z c * x

The linearization of associator_mul_right_self [Schafer, (3.8)].

theorem IsAlternative.associator_cyclic {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (x y z : α) : associator x y z = associator y z x

A cyclic permutation does not change an associator in an alternative ring.

theorem IsAlternative.associator_swap_outer {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (x y z : α) : associator x y z = -associator z y x

Swapping the outside arguments negates an associator.

theorem IsAlternative.exists_head {α : Type u} [NonUnitalNonAssocRing α] (a b : α) {n : ℕ} (h : ∀ (p q r : NonAssocWord), p.degree + q.degree + r.degree < n → associator (NonAssocWord.eval a b p) (NonAssocWord.eval a b q) (NonAssocWord.eval a b r) = 0) (w : NonAssocWord) (hw : w.degree < n) : ∃ (x : Bool) (t : Option NonAssocWord), NonAssocWord.eval a b w = NonAssocWord.prependEval a b x t ∧ w.degree = NonAssocWord.prependDegree t

If all associators of words of total degree less than n vanish, then every word of degree less than n can be reassociated to expose its first letter.

theorem IsAlternative.associator_prepend_same_head {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (a b : α) {n : ℕ} (h : ∀ (p q r : NonAssocWord), p.degree + q.degree + r.degree < n → associator (NonAssocWord.eval a b p) (NonAssocWord.eval a b q) (NonAssocWord.eval a b r) = 0) (p : NonAssocWord) (x : Bool) (qTail rTail : Option NonAssocWord) (hdegree : p.degree + NonAssocWord.prependDegree qTail + NonAssocWord.prependDegree rTail = n) : associator (NonAssocWord.eval a b p) (NonAssocWord.prependEval a b x qTail) (NonAssocWord.prependEval a b x rTail) = 0

Schafer's induction step when the last two words start with the same letter.

theorem IsAlternative.associator_word {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (a b : α) (p q r : NonAssocWord) : associator (NonAssocWord.eval a b p) (NonAssocWord.eval a b q) (NonAssocWord.eval a b r) = 0

The associator of three non-associative monomials in two elements vanishes. This is the monomial form of Artin's theorem [Schafer, Theorem 3.1].

From monomials to the additive closure

inductive IsAlternative.WordSpan {α : Type u} [NonUnitalNonAssocRing α] (a b : α) : α → Prop

Additive combinations of non-associative monomials in a and b.

• word {α : Type u} [NonUnitalNonAssocRing α] {a b : α} (p : NonAssocWord) : WordSpan a b (NonAssocWord.eval a b p)
• zero {α : Type u} [NonUnitalNonAssocRing α] {a b : α} : WordSpan a b 0
• add {α : Type u} [NonUnitalNonAssocRing α] {a b x y : α} : WordSpan a b x → WordSpan a b y → WordSpan a b (x + y)
• neg {α : Type u} [NonUnitalNonAssocRing α] {a b x : α} : WordSpan a b x → WordSpan a b (-x)

theorem IsAlternative.WordSpan.mul {α : Type u} [NonUnitalNonAssocRing α] {a b x y : α} (hx : WordSpan a b x) (hy : WordSpan a b y) : WordSpan a b (x * y)

The additive span of words is closed under multiplication.

theorem IsAlternative.WordSpan.of_mem_closure {α : Type u} [NonUnitalNonAssocRing α] (a b : α) {x : α} (hx : x ∈ NonUnitalSubring.closure {a, b}) : WordSpan a b x

Every element of the non-associative ring closure is an additive combination of words.

theorem IsAlternative.WordSpan.word_nuclear {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (a b : α) (p : NonAssocWord) : IsNuclearIn {x : α | WordSpan a b x} (NonAssocWord.eval a b p)

A word is nuclear relative to the additive span of all words.

theorem IsAlternative.WordSpan.nuclear {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] {a b x : α} (hx : WordSpan a b x) : IsNuclearIn {y : α | WordSpan a b y} x

Every additive combination of words is nuclear relative to the span.

theorem IsAlternative.associator_of_mem_pair {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (a b : α) {x y z : α} (hx : x ∈ {a, b}) (hy : y ∈ {a, b}) (hz : z ∈ {a, b}) : associator x y z = 0

The associator vanishes on any triple drawn from {a, b}: two of the three arguments coincide by pigeonhole, and the associator is alternating.

This is the base case of generators_nuclear.

theorem IsAlternative.generators_nuclear {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (a b : α) : IsNuclearIn (↑(NonUnitalSubring.closure {a, b})) a ∧ IsNuclearIn (↑(NonUnitalSubring.closure {a, b})) b

Each generator is nuclear in the non-associative subring generated by the pair.

theorem IsAlternative.nuclear_of_mem_closure {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] (a b : α) {x : α} (hx : x ∈ NonUnitalSubring.closure {a, b}) : IsNuclearIn (↑(NonUnitalSubring.closure {a, b})) x

Every element of the closure is nuclear in the closure.

Pure nucleus bookkeeping on top of generators_nuclear: the nuclear elements form a subring (IsNuclearIn.zero/add/neg/mul), so they contain the closure of the generators.

theorem IsAlternative.artin_two_generated_assoc {α : Type u} [NonUnitalNonAssocRing α] [IsAlternative α] : TwoGeneratedAssoc α

Artin's theorem, hard direction: in an alternative ring, the subring generated by any two elements is associative.

theorem IsAlternative.isAlternative_iff_two_generated_assoc {α : Type u} [NonUnitalNonAssocRing α] : IsAlternative α ↔ TwoGeneratedAssoc α

Artin's theorem.