Equation 1323

In this chapter we study magmas that satisfy equation 1323,

\[ x = y \diamond (((y \diamond y) \diamond x) \diamond y)\qquad\text{(1)} \]

for all \(x,y\). Using the squaring operator \(Sy := y \diamond y\) and the left and right multiplication operators \(L_y x := y \diamond x\) and \(R_y x = x \diamond y\), this law can be written as

\[ L_y R_y L_{Sy} x = x. \]

In particular, this gives a way to construct these magmas:

LemmaConstruction of 1323 magmas#

Suppose that \(M\) is a magma such that

\[ R_{Sy} L_{Sy} = 1\qquad\text{(2)} \]

and

\[ L_{y} R_{y} = R_{Sy}\qquad\text{(3)} \]

hold. Then the magma satisfies 1323.

Proof

Trivial.

Lean

Stated as Eq1323.eq1323_if_conditions; the blueprint marks no proof of it as formalized.

Sources
LeanEq1323.eq1323_if_conditions

So now we would like to construct magmas satisfying (2) and (3). We need some bijections:

LemmaBijections#

Let \(G\) be a countably infinite abelian torsion group of exponent \(2\). Then there exists a bijection \(\phi_a: G \to \mathbb{Q}^\times\) for each \(a \in G \backslash \{0\}\) such that \(\phi_a(0) = 1\) and \(\phi_a(a+b) = -\phi_a(b)\) for all \(b \in G\), so in particular \(\phi_a(a)=-1\).

Proof

Such a bijection can be easily constructed from the axiom of choice and a greedy algorithm, defining \(\phi_a\) one pair \(\{b,a+b\}\) at a time.

Lean

Stated as Eq1323.ϕ; the blueprint marks no proof of it as formalized.

Sources
LeanEq1323.ϕ
Used by 1
Used byBuilding a magma

LemmaBuilding a magma#

Let \(G\) be a countably infinite abelian torsion group of exponent \(2\), and let \(\phi_a\) be as in the previous lemma. Let \(N\) be the set of pairs \((x,a)\) with \(x \in \mathbb{Q}^\times\) and \(a \in G \backslash \{0\}\), and let \(M = G \uplus N\) be the disjoint union of \(G\) and \(N\). Suppose that we have an operation \(\diamond : M \times M \to M\) satisfying the following axioms:

  • (i) We have

    \[ a \diamond b = a+b\qquad\text{(4)} \]

    for \(a,b \in G\).

  • (ii) We have

    \[ (x,a) \diamond b = (\phi_a(b) x, a)\qquad\text{(5)} \]
    \[ b \diamond (x,a) = (x / \phi_a(b), a)\qquad\text{(6)} \]

    and

    \[ (\phi_a(b) x,a) \diamond (x,a) = a+b\qquad\text{(7)} \]

    for \(x \in \mathbb{Q}^\times\), \(b \in G\), and \(a \in G \backslash \{0\}\).

  • (iii) If \(a,b,0 \in G\) are distinct and \((x,a) \diamond (y,b) = (z,c)\) for some \(x,y,z \in \mathbb{Q}^\times\) and \(c \in G\), then \((y,b) \diamond (z,c) = (\phi_a(b) x,a)\).

Then (2), (3) and hence (1) holds.

Proof

With these rules, \(0\) is a unit, and the squaring operator is given by \(Sa = 0\) and \(S(x,a) = a\), so the set of squares is \(G\). If \(a \in G\) is a square number, we have

\[ L_a b = R_a b = a+b \]

and

\[ L_a (x,b) = (x/\phi_b(a), b); \quad R_a (x,b) = (x \phi_b(a), b) \]

so (2) is satisfied.

Now we verify (3). If \(y\) is a square, then the claim already follows from (2) since \(Sy=0\) is a unit. Otherwise, for \(y \in \mathbb{Q}^\times\) and \(b \in G \backslash \{0\}\), we have to show that

\[ L_{(y,b)} R_{(y,b)} a = R_b a = a+b \]

for \(a \in G\) and

\[ L_{(y,b)} R_{(y,b)} (x,a) = R_b (x,a) = (\phi_a(b) x, a) \]

for \(x \in \mathbb{Q}^\times\) and \(a \in G \backslash \{0\}\). In the first case, we have from (6) that

\[ R_{(y,b)} a = (y/\phi_a(b), b) \]

and then from (7) we have

\[ L_{(y,b)} R_{(y,b)} a = a+b \]

as required. In the second case, if \(a=b\), then by the bijective nature of \(\phi_a\), we can write \(x = \phi_a(c) y\) for some \(c \in G\), then from (7) we have

\[ R_{(y,b)} (x,a) = a+c \]

and then by (5)

\[ L_{(y,b)} R_{(y,b)} (x,a) = (\phi_a(a+c) y, a) \]

but from construction we have \(\phi_a(a+c)=-\phi_a(c) = \phi_a(b)\phi_a(c)\) and hence \(\phi_a(a+c) y = \phi_a(b) x\) as required.

It remains to handle the case when \(a,b\) are distinct elements of \(G \backslash \{0\}\). But this follows from (iii).

Lean

Stated as Eq1323.op_Ly_Ry_eq_LSy; the blueprint marks no proof of it as formalized.

Sources
LeanEq1323.op_Ly_Ry_eq_LSy
Uses 1 · Used by 1
Proof usesBijections
Used byIterated greedy extension

LemmaGreedy extension#

If \(\diamond\) is defined by a partial solution, and \((x,a) \diamond (y,b)\) is undefined for some \(x,y \in \mathbb{Q}^\times\) and distinct \(a,b \in G \backslash \{0\}\), then it is possible to extend the partial solution so that \((x,a) \diamond (y,b)\) is now defined.

Proof

We select a \(c \in G \backslash \{0\}\) that has not previously been used by the partial solution, let \(z \in \mathbb{Q}^\times\) be arbitrary, (e.g., one could take \(z=1\) if desired), and add \((x,y,z,a,b,c)\) to \({\mathcal F}\), thus we now also assign

\[ (\phi_a(b)^n x,a) \diamond (\phi_b(c)^n y,b) = (\phi_c(a)^n z,c) \]
\[ (\phi_b(c)^n y,b) \diamond (\phi_c(a)^n z,c) = (\phi_a(b)^{n+1} x, a) \]
\[ (\phi_c(a)^n z,c) \diamond (\phi_a(b)^{n+1} x, a) = (\phi_b(c)^{n+1} y,b) \]

for all natural numbers \(n\). As the \(a,b,c\) are distinct, the \(\phi_a(b), \phi_b(c), \phi_c(a)\) are not equal to \(\pm 1\), and the members of this infinite sequence do not collide with each other. The second and third equations in this family cannot collide with previous assignments because \(c\) is novel. If we arrange matters so that \(\phi_b(c)\) involves primes in the numerator or denominator that do not appear in any previous \(\phi_a(b), \phi_b(c), \phi_c(a), x, y, z\) used by the greedy algorithm, or the current \(x,y,z\), then we also see that the first infinite sequence does not collide with any previously assigned value of \(\diamond\) either.

Lean

Stated as Eq1323.extend; the blueprint marks no proof of it as formalized.

Sources
LeanEq1323.extend
Used by 1
Used byIterated greedy extension

CorollaryIterated greedy extension#

Every partial solution can be extended to a complete solution that satisfies (2) and (3), and hence 1323.

Proof

Apply the usual greedy algorithm.

Lean

Stated as Eq1323.exists_complete_function; the blueprint marks no proof of it as formalized.

Sources
LeanEq1323.exists_complete_function
Uses 2 · Used by 1
Proof usesGreedy extension · Building a magma
Used by1323 does not imply 2744

Corollary1323 does not imply 2744#

There exists a 1323 magma which does not satisfy the 2744 equation \(R_y L_{Sy} L_y x = x\).

Proof

It suffices to produce a partial solution in which \(L_y\) is not injective. Pick distinct \(a, b, b', c\) with \(\phi_a(b)\), \(\phi_a(b')\) having no prime factors in common in the numerator or denominator. We take the partial solution consisting of \((1,1,1,a,b,c)\) and \((1,1,1,a,b',c)\), that is to say we impose the conditions

\[ (\phi_a(b)^n,a) \diamond (\phi_b(c)^n,b) = (\phi_c(a)^n,c) \]
\[ (\phi_b(c)^n,b) \diamond (\phi_c(a)^n,c) = (\phi_a(b)^{n+1}, a) \]
\[ (\phi_c(a)^n,c) \diamond (\phi_a(b)^{n+1}, a) = (\phi_b(c)^{n+1},b) \]

and

\[ (\phi_a(b)^n,a) \diamond (\phi_{b'}(c)^n,b') = (\phi_c(a)^n,c) \]
\[ (\phi_{b'}(c)^n,b') \diamond (\phi_c(a)^n,c) = (\phi_a(b')^{n+1}, a) \]
\[ (\phi_c(a)^n,c) \diamond (\phi_{a}(b')^{n+1}, a) = (\phi_b(c)^{n+1},b'). \]

One can check that no collisions occur; on the other hand, as \(L_{(1,a)} (1,b) = L_{(1,a)} (1,b') = (1,c)\), we already have a violation of left injectivity. Completing this seed to a full magma using Iterated greedy extension, we obtain the claim.

Lean

Stated as Eq1323.Equation1323_not_implies_Equation2744; the blueprint marks no proof of it as formalized.

Sources
LeanEq1323.Equation1323_not_implies_Equation2744
Uses 1
Proof usesIterated greedy extension

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.