17 Equation 1516

In this chapter we study magmas that obey equation 1516,

x = (y ⋄ y) ⋄ (x ⋄ (x ⋄ y))

for all $x, y$ . Using the squaring operator $S y := y ⋄ y$ and the left and right multiplication operators $L_{y} x := y ⋄ x$ and $R_{y} x = x ⋄ y$ , this law can be written as

L_{S y} L_{x} L_{x} y = x .

We begin by studying a greedily constructed translation invariant model

x ⋄ y = x + f (y - x)

on the carrier $Z$ with some function $f : Z \to Z$ with $f (0) = 0$ . This ensures that $S x = x$ . If $y = x + h$ , then $L_{x} y = x + f (h)$ , $L_{x}^{2} y = x + f^{2} (h)$ , and $L_{y} L_{x}^{2} y = y + f (f^{2} (h) - h)$ , so the law Equation 1 simplifies to

f (f^{2} (h) - h) = - h .

Thus, if we let $E = {(h, f (h))}$ be the graph of $f$ , then we have the following property: if $(a, b), (b, c) \in E$ , then $(c - a, - a) \in E$ . This helps motivate the following definition.

Definition 17.1 1516 seed

A 1516 seed is a finite collection $E$ of pairs $(a, b)$ with $a, b \in Z$ obeying the following axioms:

Axiom 1: $(0, 0) \in E$ .
Axiom 2: If $(a, b) \in E$ and $a \neq 0$ , then $b \neq 0, - a$ .
Axiom 3: If $(a, b), (a, b^{'}) \in E$ , then $b = b^{'}$ .
Axiom 4: If $(a, b), (b, c) \in E$ , then $(c - a, - a) \in E$ .
Axiom 5: If $(b, a), (b^{'}, a), (- b, d), (- b^{'}, d^{'}) \in E$ with $b \neq b^{'}$ , then $b + d \neq d^{'}, b^{'} + d^{'}$ .

An extension of a 1516 seed $E$ is a 1516 seed $E^{'}$ that contains $E$ .

This definition has an extension property:

Lemma 17.2 1516 extension

Let $E$ be a 1516 seed, and let $a_{0} \in Z$ . Then there exists an extension $E^{'}$ of $E$ that contains $(a_{0}, c_{0})$ for some $c_{0}$ .

Proof ▶

We may assume that $E$ does not already contain any pair of the form $(a_{0}, c)$ , since we are done otherwise. By Axiom 1 implies that $a_{0} \neq 0$ . Let $b_{1}, \dots, b_{n}$ denote all the integers $b_{i}$ such that $(b_{i}, a) \in E$ , then $n \geq 0$ is finite, and by Axiom 2 all the $b_{i}$ are non-zero and not equal to $- a$ . Let $c_{0}$ be a sufficiently large integer to be chosen later. We then add the pairs $(a_{0}, c_{0})$ and $(c - b_{i}, - b_{i})$ to $E$ for all $i$ . Furthermore, if $i$ is such that $(- b_{i}, d_{i}) \in E$ for some (necessarily unique and non-zero) $d_{i}$ , we also add $(d_{i} + b + i - c_{0}, b_{i} - c_{0})$ to $E$ . Let $E^{'}$ be the resulting set of pairs. Axioms 4, 5 for $E$ ensure that (for $c_{0}$ large enough) the addition of these pairs do not cause a violation of Axioms 2 or 3 for $E^{'}$ , and of course Axiom 1 for $E^{'}$ will also be retained. As for Axiom 4, one can check that the only new pairs of pairs $(^{'}, b), (b, c)$ that would trigger these axioms either take the form $(b_{i}, a_{0}), (a_{0}, c_{0})$ or $(c_{0} - b_{i}, - b_{i}), (- b_{i}, d_{i})$ , and in either case we see from construction that Axiom 4 remains in effect for $E^{'}$ . Finally, the new quadruples of pairs $(b, a), (b^{'}, a), (- b, d), (- b^{'}, d^{'}) \in E^{'}$ only arise when either $(- b, d)$ , $(- b^{'}, d^{'})$ is equal to $(a_{0}, c_{0})$ and the other three pairs in the quadruple were already in $E$ , and for $c_{0}$ large enough we see that Axiom 5 remains valid.

For technical reasons (which will be helpful later when we expand the magma) we also give a variant that will ensure a useful “double surjectivity” property:

Lemma 17.3 1516 extension variant

Let $E$ be a 1516 seed, and let $h \in Z$ be non-zero. Then there exists an extension $E^{'}$ of $E$ that contains $(a_{i}, a_{i} + h)$ for $i = 1, 2, 3, 4$ , for some distinct $a_{1}, a_{2}, a_{3}, a_{4}$ .

Proof ▶

If we choose $a$ sufficiently large, and set $a_{i} = i a$ (say) for $i = 1, 2, 3, 4$ , the claim simply follows by adding $(a_{i}, a_{i} + h)$ to $E$ and verifying that none of the axioms are violated.

Corollary 17.4 Base magma

There exists a 1516 magma with carrier $Z$ with the properties that

(i) $S a = a$ for all $a$ .
(ii) For any distinct $a, b \in Z$ , the equation $R_{a} c = b$ has at least four solutions $c$ .
(iii) For each $a \in Z$ , there exist at least two $b \neq a$ such that $L_{a} R_{a} b = b$ .

Note from Equation 1 and the hypothesis $S a = a$ that $R_{a} c = a$ if and only if $c = a$ . Thus, the requirement that $a, b$ be distinct in (ii) is necessary.

Proof ▶

By Lemma 17.2, Lemma 17.3 and the greedy algorithm starting with the seed consisting of $(0, 0)$ , $(- 1, 2)$ , $(3, 1)$ , $(- 10, 20)$ , $(30, 10)$ , we obtain a graph ${(a, f (a)) : a \in Z}$ of a function $f : Z \to Z$ with $f (0) = 0$ , $f (- 1) = 2$ , $f (3) = 1$ , $f (- 10) = 20$ , $f (30) = 10$ and the property that if $f (a) = b$ and $f (b) = c$ , then $f (c - a) = - a$ , and also with the property that for every non-zero $h$ there are distinct $a_{h, 1}, a_{h, 2}, a_{h, 3}, a_{h, 4}$ with $f (a_{h, i}) = a_{h, i} + h$ for $i = 1, 2, 3, 4$ . We then have that Equation 3 holds. If we then define the magma operation $⋄$ by Equation 2, we obtain Equation 1, and since $f (0) = 0$ we have (i). Also, from construction we see that $R_{d} (d - a_{h, i}) = d + h$ for any $d, h, i$ , giving (ii). Finally, from construction we have $R_{a} (a + 1) = a + 1 + f (- 1) = a + 3$ , so $L_{a} R_{a} (a + 1) = a + f (3) = a + 1$ , and similarly $L_{a} R_{a} (a + 10) = a + 10$ , giving (iii).

Let us denote by $A$ the free group over $N$ . Note that a magma with the same properties as in Corollary 17.4 but having carrier $A$ can be constructed similarly. The same thing is true for the following results. In fact, the Lean implementation has $A$ whenever $Z$ is; this has been done to reuse some preexisting code.

Now we construct a more complex 1516 magma, whose carrier $G$ is $Z \cup G^{'}$ , where

G^{'} := {(a, c, n) \in Z \times Z \times N : a \neq c} .

The first component $Z$ will represent the squares, and the second component $G^{'}$ will represent the non-squares. The most important coordinate of an element $(a, c, n)$ of $G^{'}$ is $a$ ; the other two components $c, n$ are technical, with $n$ being needed to ensure a certain infinite surjectivity property, and $c$ being such that $L_{c} (a, c, n)$ remains at one’s disposal to select at certain stages of the inductive process.

The 1516 magma constructed in Corollary 17.4 will be the restriction of $G$ to $Z$ ; thus $a ⋄ b$ is already defined in $G$ for $a, b \in Z$ , but the rest of the multiplication table is not currently defined. By construction, $S$ is already defined and equal to the identity on $Z$ , and we have the 1516 equation

L_{S a} L_{b} L_{b} a = b

for $a, b \in Z$ , with the left multiplication operators $L_{b}$ currently only defined as maps from $Z$ to $Z$ . Among other things, this means that $L_{a} = L_{S a}$ is surjective as a map from $Z$ to $Z$ for any $a \in Z$ .

We extend the squaring map $S$ to all of $G$ by declaring $S (a, c, n) := a$ , thus $S$ maps $G$ to $Z$ . To create a 1516 magma structure on all of $G$ , we need to extend the left multiplication operators $L_{b}$ , $b \in Z$ as maps from $G$ to $G$ , and also introduce additional maps $L_{x} : G \to G$ for $x \in G^{'}$ , obeying the following axioms:

Axiom A: For any $x \in G^{'}$ , $L_{x} x = S x$ .
Axiom B: For any $x \in G^{'}$ and $b \in Z$ , $L_{S x} L_{b} L_{b} x = b$ .
Axiom C: For any $x \in G$ and $y \in G^{'}$ , $L_{S x} L_{y} L_{y} x = y$ .

We first address Axiom B, which purely concerns how to extend the $L_{b}$ operators for $b \in Z$ , and also impose an additional technical “infinitely surjective” requirement that will help us satisfy Axiom C later. We first need some preparatory lemmas. We begin by locating some useful elements $c_{y, b}$ of $Z$ for all $y \in G^{'}$ and $b \in Z$ .

Lemma 17.5 Useful elements

One can assign $c_{y, b} \in Z$ for each $y = (a, c, n) \in G^{'}$ and $b \in Z$ with the following properties:

(i) For all $y = (a, c, n) \in G^{'}$ and $b \in Z$ , $c_{y, b} \neq a, b, c$ and $L_{a} L_{c_{y, b}} b = c_{y, b}$ .
(ii) For all $y \in G^{'}$ , the map $b \mapsto c_{y, b}$ is injective.

Proof ▶

Let $y = (a, c, n)$ . By Corollary 17.4 (iii), we can find $c_{y, a} \neq a, c$ such that $L_{a} R_{a} c_{y, a} = c_{y, a}$ , or equivalently $L_{a} L_{c_{y, a}} a = c_{y, a}$ . Next, for any $b \neq a$ , we can apply Corollary 17.4 (ii) to find $c_{y, b} \neq b, c, c_{y, a}$ such that $R_{a} c_{y, b} = b$ ; note that as $R_{a} a = S a = a \neq b$ , this also implies that $c_{y, b} \neq a$ , and that the $c_{y, b}$ are distinct as $b$ variables. We now have $L_{a} L_{c_{y, b}} b = L_{S a} L_{c_{y, b}} L_{c_{y, b}} a = c_{y, b}$ for such $b$ , giving the claim.

Let $c_{y, b}$ be as above. Define a partial solution to be a partial assignment of $L_{c^{'}} y \in G$ for $c^{'} \in Z$ and $y \in G$ that obeys the following properties:

(a) If $y \in Z$ , then $L_{c^{'}} y$ agrees with the operation defined in Corollary 17.4.
(b) If $y = (a, c, 0) \in G^{'}$ , then $L_{a} y = a$ .
(c) If $y = (a, c, n) \in G^{'}$ and $n \neq 0$ , then $L_{a} y = (a, c, 0)$ .
(d) If $y = (a, c, n) \in G^{'}$ and $b \in Z$ , then $L_{c_{y, b}} y = b$ .
(e) For any $a, c$ , $L_{c} (a, c, n)$ is only defined for finitely many $n$ .
(f) If $y = (a, c, n) \in G^{'}$ and $c^{'} \in Z$ are such that $L_{c^{'}} y$ is defined, then $L_{c^{'}} L_{c^{'}} y$ and $L_{a} L_{c^{'}} L_{c^{'}} y$ are defined, with $L_{a} L_{c^{'}} L_{c^{'}} y$ equal to $c^{'}$ .
(g) If $y = (a, c, n) \in G^{'}$ and $c^{'} \in Z$ are such that $c^{'} \neq a$ and $L_{c^{'}} y$ is defined, then $L_{c^{'}} y \neq c^{'}$ .

Lemma 17.6 Existence of partial solution

A partial solution exists.

Proof ▶

We define $L_{c^{'}} y$ for $y = (a, c, n) \in G^{'}$ as follows:

(i) If $c^{'} = a$ and $n = 0$ , then $L_{c^{'}} y := a$ .
(ii) If $c^{'} = a$ and $n \neq 0$ , then $L_{c^{'}} y := (a, c, 0)$ .
(iii) If $c^{'} = c_{y, b}$ for some $b$ , then $L_{c^{'}} y := b$ .
(iv) In all other cases, $L_{c^{'}} y$ is undefined.

We of course also define $L_{c^{'}} y$ for $y \in Z$ using Corollary 17.4.

From Lemma 17.5 we see that this is a well-defined operation, with $L_{c} y$ undefined for any $y = (a, c, n) \in G^{'}$ . So properties (a)-(e) and (g) are clear from construction. Property (e) is also clear from construction in each of the three cases (i), (ii), (iii) (for (i), (ii) we also use the fact that $L_{a} a = a$ ).

We can make $L_{c^{'}} y$ defined in a partial solution:

Lemma 17.7 First extension

Suppose we have a partial solution for which $L_{c^{'}} y$ is currently undefined for some $c^{'} \in Z$ and $y \in G$ . Then one can extend this partial solution in such a manner that $L_{c^{'}} y$ is now defined.

Proof ▶

Write $y = (a, c, n)$ . Because $L_{a} : Z \to Z$ and $L_{c^{'}} : Z \to Z$ are surjective, we can find $b \in Z$ such that $L_{a} L_{c^{'}} b = c^{'}$ . If we had $b = c^{'}$ , then $L_{a} c^{'} = c^{'}$ , which from 1 (and $S c^{'} = c^{'}$ ) implies that $a = c^{'}$ , which contradicts the undefined nature of $L_{c^{'}} y$ thanks to properties (b), (c) of a partial solution. Hence, $b \neq c^{'}$ . We then set $L_{c^{'}} y := b$ . It is then clear that all the properties (a)-(g) of a partial solution are maintained.

We can also insert inverses of $L_{c^{'}}$ :

Lemma 17.8 Second extension

Suppose we have a partial solution, and let $c^{'} \in Z$ and $y = (a, c, n) \in G$ . Then, unless one is in the case when $c^{'} = a$ and $n = 0$ , then one can find $z \in G$ such that $L_{c^{'}} z$ is currently undefined, but for which one can find an extension of the partial solution for which $L_{c^{'}} z$ is now equal to $y$ .

Proof ▶

Write $y = (a, c, n)$ . There are several cases.

Case 1: $L_{c^{'}} y = w$ for some $w \in G^{'}$ . By Lemma 17.5, $c_{w, c^{'}}$ is distinct from $c^{'}$ , and from property (d) of a partial solution, $L_{c_{w, c^{'}}} w = c^{'}$ . By property (e) of a partial solution, we can find $z = (c_{w, c^{'}}, c^{'}, n^{'})$ such that $L_{c^{'}} z$ is currently undefined. Then set $L_{c^{'}} z := y$ , so that we have $L_{c_{w, c^{'}}} L_{c^{'}} L_{c^{'}} z = c^{'}$ . One then verifies that all the axioms (a)-(g) of a partial solution are valid in this case.
Case 2: $c^{'} \neq a$ and $L_{c^{'}} y = b$ for some $b \in Z$ . By property (g) of a partial solution, $c^{'} \neq b$ . By Corollary 17.4, we can find $a^{'}$ such that $L_{a^{'}} b = R_{b} a^{'} = c^{'}$ and $a^{'} \neq c^{'}$ . By property (e) of a partial solution, we can find $z = (a^{'}, c^{'}, n^{'})$ such that $L_{c^{'}} z$ is currently undefined. Then set $L_{c^{'}} z = y$ , so that we have $L_{a^{'}} L_{c^{'}} L_{c^{'}} z = c^{'}$ . One then verifies that all the axioms (a)-(g) of a partial solution are valid in this case.
Case 3: $c^{'} \neq a$ and $L_{c^{'}} y$ is currently undefined. Use Lemma 17.7 set $L_{c^{'}} y$ equal to some $b \in Z$ , then apply the Case 2 analysis.
Case 4: $c^{'} = a$ . Because we are excluding the case $n = 0$ , we are now in Case 1 thanks to property (c) of a partial solution.

Now we can establish Axiom B.

Proposition 17.9 Obtaining Axiom B

There exists a way to extend $L_{b} : Z \to Z$ to $L_{b} : G \to G$ for all $b \in Z$ , in such a way that Axiom B holds, and furthermore for each $b \in Z$ and $x \in G^{'}$ , the set ${y \in G^{'} : L_{b} y = x}$ is infinite. Also, we can ensure that $L_{b} x \neq x$ for any $b \in Z$ and $x \in G^{'}$ .

Proof ▶

By iterating Lemma 17.7 and Lemma 17.8 in alternation, we can find an increasing chain of partial solutions with the property that for any $y = (a, c, n) \in G^{'}$ and $c^{'} \in Z$ and any natural number $k$ , excluding the case where $c^{'} = a$ and $n = 0$ , that one can find a partial solution on this chain for which $L_{c^{'}} y$ is defined, and such that $L_{c^{'}} z = y$ for at least $k$ distinct choices of $z \in G^{'}$ . Taking the limit of this chain, we can then find a fully defined operation $L_{c^{'}} y$ for $c^{'} \in Z$ and $y \in G$ obeying the properties (a)-(d), (f), (g) (but not (e)) of a partial solution, with the property that $y = (a, c, n) \in G^{'}$ and $c^{'} \in Z$ , excluding the case $c^{'} = a$ and $n = 0$ , that there are infinitely many $z \in G^{'}$ such that $L_{c^{'}} z = y$ . The excluded case $c^{'} = a, n = 0$ is also covered by property (b) of a partial solution. The claim follows.

Finally, we construct the remaining $L_{x}$ .

Proposition 17.10 Obtaining Axioms A, C

One can find maps $L_{x} : G \to G$ for each “non-square” $x \in G^{'}$ , such that Axioms A, C hold.

Proof ▶

We can work with a single $x \in G^{'}$ . Our task is to find a function $L_{x}$ for which

L_{x} x = S x

and

L_{S y} L_{x} L_{x} y = x

for all $y \in G$ (note that $L_{S y}$ is already fully constructed).

Define a seed to be an injective partial function $L_{x}$ defined on finitely many values and obeying Equation 4, as well as Equation 5 whenever $L_{x} L_{x} y$ is defined. If there is a $y \in G$ for which $L_{x} y$ is currently undefined, then by hypothesis $y$ is equal to $L_{x} z$ for at most one $z$ . If such a $z$ exists, we set $L_{x} y$ to be an element of ${w : L_{S z} w = x}$ different from $y$ that is not already in the domain or range of $L_{x}$ ; we are able to do so thanks to the infinite surjectivity (Corollary 17.4 (ii)) and the fact that the domain and the range of $L_{x}$ are finite. If no such $z$ exists, we set $L_{x} y$ to be arbitrary element of $G$ not already in the domain or range. In either case, we see that the seed property is preserved. Starting from the seed in which $L_{x}$ is only defined on $x$ and maps it to $S x$ , we obtain the claim.

Corollary 17.11

There exists a 1516 magma that does not obey the 255 equation

x = ((x ⋄ x) ⋄ x) ⋄ x .

Proof ▶

Let us define the element $x_{0} := (0, 1, 0) \in G^{'}$ . Since $S x_{0} = 0$ , we know that $0 ⋄ x_{0} = 0$ (see the first part of the proof of Proposition 17.9). Therefore, $x_{0}$ does not obey the 255 equation, as we have □

((x_{0} ⋄ x_{0}) ⋄ x_{0}) ⋄ x_{0} = (0 ⋄ x_{0}) ⋄ x_{0} = 0 ⋄ x_{0} = 0 \neq x_{0} .