generated from pitmonticone/LeanProject
-
Notifications
You must be signed in to change notification settings - Fork 66
/
Copy path1729.tex
209 lines (173 loc) · 17.5 KB
/
1729.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
\chapter{Equation 1729}\label{1729-chapter}
In this chapter we study magmas that obey equation 1729,
\begin{equation}\label{1729}
x = (y \op y) \op ((y \op x) \op y).
\end{equation}
for all $x,y$. Using the squaring operator $Sy := y \op y$ and the left and right multiplication operators $L_y x := y \op x$ and $R_y x = x \op y$, this law can be written as
$$ L_{Sy} R_y L_{y} x = x.$$
This implies that $L_y$ is injective and $L_{Sy}$ is surjective, hence $L_{Sy}$ is invertible. If $y$ is a square (i.e., $y \in SM$), then $L_y$ and $L_{Sy}$ are both invertible, hence now $R_y$ is also invertible, with inverse $R_y^{-1} = L_y L_{Sy}$. We rewrite this as
\begin{equation}\label{lys}
L_y = R_y^{-1} L_{Sy}^{-1}
\end{equation}
for all $y \in SM$.
We have the following procedure for extending a small magma $SM$ obeying \Cref{1729} to a larger one $M$:
\begin{theorem}[Extending a 1729 magma]\label{mag} Let $SM$ be a magma obeying 1729, and let $N$ be another set disjoint from $SM$, and set $M := SM \uplus N$. Suppose that we have a squaring map $S: N \to SM$, and bijections $L_a, R_a: N \to N$ for all $a \in SM$ (which, by abuse of notation, we will denote with the same symbols as the squaring map $S$ and left and right multiplication operators $L_a,R_a$ on $SM$), obeying the following axioms:
\begin{itemize}
\item (i) For all $a \in SM$, we have $L_a = R_a^{-1} L_{Sa}^{-1}$.
\item (ii) For all $y \in N$, the elements $R_a y \in N$ are distinct from each other and from $y$ as $a \in SM$ varies.
\item (iii) If $R_a x = y$ for some $a \in SM$ and some $x,y \in N$, then $L_{Sy} L_{R_{Sx}^{-1} a} y = x$.
\item (iv) For all $x \in N$, we have $L_{Sx}^2 x = x$.
\end{itemize}
Suppose also that we have an operation $\op': N \times N \to M$ obeying the following axioms:
\begin{itemize}
\item (v) For all $x \in N$, we have $x \op' x = Sx$.
\item (vi) For all $y \in N$ and $a \in SM$, we have $R_a y \op' y = L_{Sy}^{-1} a$.
\item (vii) For all $x,y \in N$ with $x \op' y$ not already covered by rules (iv) or (v), we have $x \op' y = z$ for some $z \in N$. Furthermore, $z \op' x = L_{Sx}^{-1} y$.
\end{itemize}
Then one can endow $M$ with an operation $\op'': M \times M \to M$ obeying 1729 defined as follows:
\begin{itemize}
\item If $a,b \in SM$, then $a \op'' b = a \op b$.
\item If $a \in SM$ and $x \in N$, then $a \op'' b := L_a b$.
\item If $x \in N$ and $a \in SM$, then $b \op'' a := R_a b$.
\item If $x,y \in N$, then $x \op'' y := x \op' y$.
\end{itemize}
Furthermore, the 817 law $S^2 x \op'' x = x$ fails for any $x \in N$.
\end{theorem}
\begin{proof} We need to show that $\op''$ verifies the law \Cref{1729}. In the case when $x,y \in SM$, then the claim follows from the fact that $SM$ already obeyed this equation. If $x$ was equal to an element $a \in SM$ and $y \in N$, then by construction the law is equivalent to $L_{Sa} R_a S_a y = y$, which follows from axiom (i).
Now suppose that $x \in N$ and $y$ is equal to some element $a$ of $SM$. From axiom (v) we have $x \op'' x = Sx$, and then this case of \Cref{1729} becomes
$$L_{Sx} ( R_a x \op' x ) = a$$
which follows from axiom (vi). So the only remaining case is when $x,y \in N$. Using axiom (ii), we can divide into cases:
\begin{itemize}
\item Case 1: $x=y$. Then by (v) we need to show that $L_{Sx} L_{Sx} x = x$, which follows from axiom (iv).
\item Case 2: $y = R_a x$ for some $a \in SM$. Then by axiom (vi), we need to show that $L_{Sy} L_{L_{Sx}^{-1} a} y = x$, which follows from axiom (iii).
\item Case 3: We are not in case 1 or case 2. Then by axiom (vii), we have $y \op'' x = z$ for some $z \in N$ with $z \op'' y = L_{Sy}^{-1} x$. But this implies $L_{Sy} (z \op'' y) = x$, which is \Cref{1729}.
\end{itemize}
We have now verified that $\op''$ obeys 1729. For any $x \in N$, we have $x \op'' S^2 x = R_{S^2 x} x$, and so the final claim follows from axiom (ii).
\end{proof}
To build a magma obeying 1729 but not 817, it thus suffices to produce
\begin{itemize}
\item a 1729 magma $SM$;
\item a set $N$ of ``non-squares'';
\item a squaring map $S: N \to SM$;
\item bijections $L_a, R_a: N \to N$ for all $a \in SM$ obeying the axioms (i)-(iv); and
\item an operation $\op': N \times N \to M$ obeying the axioms (v)-(vii).
\end{itemize}
We will take $SM$ to be a countably infinite abelian group of exponent $4$, generated by generators $E_n$ for $n \in \N$ subject to the relations $4E_n=0$. Here the squaring operation $S$ is just the doubling map $Sa = 2a$, and the double squaring map is constant: $S^2 a = 0$.
We take $N$ to be the free non-abelian group with one generator $e_a$ for each $a \in SM$, then this is a countable set that we view as disjoint from $SM$. We do not attempt to define the squaring map $S: N \to SM$ at this point, but we define the right multiplication operators $R_a$ using the group action, setting
\begin{equation}\label{ra-def}
R_a x = e_a x
\end{equation}
for all $a \in SM$ and $x \in N$. Note that this automatically satisfies axiom (ii). We view $N$ as an infinite Cayley graph rooted at the identity $1$, with all other elements of $N$ obtainable uniquely from $1$ by a finite path with edges $x \mapsto e_a x$.
What about left multiplication? From two applications of \Cref{lys} and the exponent 4 hypothesis we have
$$ L_a = e_a^{-1} L_{2a}^{-1} = e_a L_0 e_{2a}^{-1}.$$
(Here we abuse notation by identifying $e_a$ with the operation of left-multiplication by $e_a$.) Thus, once $L_0$ is specified, we can \emph{define} $L_a$ for all other $a \in SM$ by the rule
\begin{equation}\label{la0}
L_a := e_a L_0 e_{2a}^{-1}.
\end{equation}
Furthermore, from the $a=0$ case of \Cref{lys} we must also have the axiom
\begin{itemize}
\item (i') $L_0^2 = e_0^{-1}$,
\end{itemize}
which also implies the $a=0$ case of \Cref{la0} (note that it implies $L_0$ commutes with $e_0$); note also that this axiom and the bijectivity of $e_0$ forces $L_0$ to be a bijection, and hence by \Cref{la0} all of the $L_a$ are bijections, so we can now drop the bijectivity requirements here. We leave the function $L_0: N \to N$ unspecified for now, but observe that if axiom (i') is obeyed, one can use \Cref{la0} as a definition of $L_a$ for all other $a$, so that axiom (i) is now a consequence of axiom (i'). We also observe from \Cref{la0} and (i') that
\begin{equation}\label{la1}
L_a^{-1} := e_{2a} L_0 e_0 e_{a}^{-1}.
\end{equation}
We now write the other remaining axioms in terms of $L_0$ rather than $L_a$ using \Cref{la0}, \Cref{la1}, \Cref{ra-def}, and the magma law on $SM$:
\begin{itemize}
\item (iii') If $e_a x = y$ for some $a \in SM$ and some $x,y \in N$, then $e_{Sy} L_0 e_{2Sy}^{-1} e_{a - Sx} L_0 e_{2(R_{Sx}^{-1} a)}^{-1} y = x$.
\item (iv') For all $x \in N$, we have $e_{Sx} L_0 e_{2Sx}^{-1} e_{Sx} L_0 e_{2Sx} x = x$.
\item (v) For all $x \in N$, we have $x \op' x = Sx$.
\item (vi') For all $y \in N$ and $a \in SM$, we have $e_a y \op' y = a - Sy$.
\item (vii') For all $x,y \in N$ with $x \op' y$ not already covered by rules (iv) or (v), we have $x \op' y = z$ for some $z \in N$. Furthermore, $z \op' x = e_{2Sx} L_0 e_0 e_{Sx} y$.
\end{itemize}
Our task is now to find a function $L_0: N \to N$ and an operation $\op': N \times N \to M$ obeying axioms (i'), (iii'), (iv'), (v), (vi'), (vii').
We will again use a greedy construction for this, but with some modifications. Firstly, the axiom (i') means that we cannot restrict $L_0$ to be partially defined on just finitely many values: any relation of the form
$$ L_0 x = y$$
for some $x,y \in N$ would automatically imply that
\begin{equation}\label{itero}
L_0 e_0^n x = e_0^n y
\end{equation}
and also
\begin{equation}\label{itero-2}
L_0 e_0^n y = e_0^{n-1} x
\end{equation}
for all $n \in \Z$. Thus, $L_0$ becomes defined on two right cosets $\langle e_0 \rangle x$, $\langle e_0 \rangle y$ of $N$, where $\langle e_0 \rangle := \{ e_0^n: n \in \Z\}$ is an infinite cyclic subgroup of $N$. In general, we will require that $L_0$ is defined on a finite union of cosets of $\langle e_0\rangle$.
In a somewhat similar vein, axiom (vii'), if iterated naively, would mean that a given entry $x \op' y = z$ of the multiplication table could potentially generate an infinite sequence of further entries, which unfortunately do not have as regular a pattern as the iterations \Cref{itero}, \Cref{itero-2} of axiom (i'). So we will need to truncate this iteration by creating an addition category of ``pending'' identities of the form ``$z \op' x = e_{2Sx} L_0 e_0 e_{Sx} y$'' for some $x,y,z \in N$, which will be temporarily undefined because $Sx$ is undefined.
More precisely, we define a \emph{partial solution} to consist of the following data:
\begin{itemize}
\item A partially defined function $L_0: N \to N$, defined on a finite union of right cosets of $\langle R_0\rangle$;
\item A partially defined operation $\op': N \times N \to M$, defined on a finite set;
\item A partially defined function $S: N \to SM$, defined on a finite set;and
\item A finite collection of ``pending identities'', which are strings of the form ``$z \op' x = e_{2Sx} L_0 e_0 e_{Sx} y$'' for some $x,y,z \in N$.
\end{itemize}
Furthermore, the following axioms are satisfied:
\begin{itemize}
\item (i'') $L_0 x$ is defined and equal to $y$, then we have the identities \Cref{itero}, \Cref{itero-2} for all $n\in \Z$.
\item (S) If $Sx$ is defined for some $x \in N$, then $Sy$ is defined for all $y$ on the path in the Cayley graph connecting $1$ to $x$.
\item (iii'') If $e_a x = y$ for some $a \in SM$ and some $x,y \in N$, and $Sx, Sy$ are defined, then $e_{Sy} L_0 e_{2Sy}^{-1} e_{a-Sx} L_0 e_{2(a-Sx)}^{-1} y$ is defined and equal to $x$.
\item (iv'') If $x \in N$ is such that $Sx$ is defined, then $e_{Sx} L_0 e_{2Sx}^{-1} e_{Sx} L_0 e_{2Sx} x$ is defined and equal to $x$.
\item (v'') If $x \in N$ and $x \op' x$ is defined, then $Sx$ is defined and equal to $x \op' x$.
\item (vi'') For all $y \in N$ and $a \in SM$, if $e_a y \op' y$ is defined, then $a - Sy$ is defined and equal to $e_a y \op' y$.
\item (vii'') For all $x,y \in N$ and $x$ is not equal to $y$ or $e_a y$ for any $a \in SM$, and $x \op' y$ is defined, then it is equal to some $z \in N$. Furthermore, either ``$z \op' x = e_{2Sx} L_0 e_0 e_{Sx} y$'' is a pending identity, or else $z \op' x$ and $e_{2Sx} L_0 e_0 e_{Sx} y$ are defined and equal to each other.
\item (P) If ``$z \op' x = e_{2Sx} L_0 e_0 e_{Sx} y$'' is a pending identity, then $x,y,z \in N$, and $Sx$ and $z \op' x$ are undefined. Furthermore, $z$ is not equal to $x$ or $e_a x$ for any $a \in SM$.
\end{itemize}
A trivial example of a partial solution is obtained by setting $L_0, \op', S$ to be empty functions, and to have an empty set pending identities.
Now we seek to enlarge a partial solution. We first make an easy observation:
\begin{proposition}[Enlarging $L_0$]\label{enlarge-l0} Suppose one has a partial solution in which $L_0 x$ is undefined for some $x \in N$. Then one can extend the partial solution so that $L_0 x$ is now defined.
\end{proposition}
\begin{proof} By axiom (i''), $L_0 e_0^n x$ is undefined for every integer $n$. Let $d = E_m$ be a generator of $SM$ that does not appear as a component of any index of any of the generators $e_a$ appearing anywhere in the partial solution; such a $d$ exists due to the finiteness hypotheses. We set $L_0 x := e_d$, and then extend by \Cref{itero}, \Cref{itero-2}, thus
$$L_0 e_0^n x := e_0^n e_d$$
and
$$L_0 e_0^n e_d := e_0^{n-1} x.$$
Because of the new nature of $d$, no collisions in the partial function $L_0$ are created by this operation. It is then easy to check that axiom (i'') is preserved by this operation, whereas none of the other axioms (S), (iii''), (iv''), (v''), (vi''), (vii''), (P) are affected by this extension.
\end{proof}
Next, we provide a tool for enlarging the domain of definition of $S$:
\begin{proposition}[Enlarging $S$]\label{enlarge-S} Suppose one has a partial solution in which $Sx$ is undefined for some $x \in N$. Then one can extend the partial solution so that $Sx$ is now defined.
\end{proposition}
\begin{proof} By iteration we may assume inductively that $Sy$ is already defined for all $y$ on the unique path in the Cayley graph from $1$ to $x$. (This hypothesis is vacuous if $x=1$.) Let $y_0$ be the parent of $x$, that is to say the unique neighbor of $x$ in the path to $1$ (this is only defined for $x \neq 1$), then by axiom (i'') $y_0$ is the unique neighbor for which $Sy_0$ is defined, and we either have $x = e_a y_0$ or $e_a x = y_0$ for some $a \in SM$.
Let $d_0, d_1, d_2 \in SM$ be distinct generators $E_{n_0}, E_{n_1}, E_{n_2}$ of $SM$ that do not appear in the index $a$ of any $e_a$ that currently appears in the partial solution (of which there are only finitely many). We also set some further distinct generators $d'_{y,z}, d''_{y,z} \in SM$ for $y,z \in SM$ that are distinct from each other and all previous generators (this is possible as we have infinitely many generators). We set $Sx := e_{d_0}$; this preserves axiom (S). In order to retain axiom (iv''), we now also set
$$ L_0 e_{2d_0} x := e_{d_1}$$
$$ L_0 e_{2e_{d_0}}^{-1} e_{Sx} e_{d_1} := e_{-d_0} x$$
and then extend these choices using \Cref{itero}, \Cref{itero-2} to recover axiom (i'), thus for instance
$$ L_0 e_0^n e_{2d_0} x := e_0^n e_{d_1}$$
and
$$ L_0 e_0^n e_{d_1} x := e_0^{n-1} e_{2d_0}$$
for all $n \in \Z$. To retain axiom (iii''), we perform the following actions:
\begin{itemize}
\item If $y_0$ is undefined, do nothing.
\item If $e_a x = y_0$ for some $a \in SM$, set $L_0 e_{2(a-d_0)}^{-1} y_0 := e_{d_2}$ and $L_0 e_{2Sy_0}^{-1} e_{a-d_0} e_{d_2} := e_{Sy_0}^{-1} x$. Then extend using \Cref{itero}, \Cref{itero-2}.
\item If $x = e_a y_0$ for some $a \in SM$, and $L_0 e_{2(a-Sy_0)}^{-1} x$ is already defined, set $L_0 e_{2d_0}^{-1} e_{a-Sy_0} L_0 e_{2(a-Sy_0)}^{-1} x :=e_{d_0}^{-1} x$, and extend using \Cref{itero}, \Cref{itero-2}.
\item If $x = e_a y_0$ for some $a \in SM$, and $L_0 e_{2(a-Sy_0)}^{-1} x$ is not yet defined, set $L_0 e_{2(a-Sy_0)}^{-1} x := e_{d_2}$ and $L_0 e_{2d_0}^{-1} e_{a-Sy_0} e_{d_2} := e_{d_0}^{-1} x$, and extend using \Cref{itero}, \Cref{itero-2}.
\end{itemize}
To retain axiom (P), we perform the following actions for each pending identity of the form ``$z \op' x = e_{2Sx} L_0 e_0 e_{Sx} y$'' for some $y,z$, executed in some arbitrary order.
\begin{itemize}
\item Remove this identity from the list of pending identities.
\item Set $L_0 e_0 e_{d_0} y := e_{d'_{y,z}}$, and $x' \op y' = z'$, where $(x',y',z') := (z, x, e_{2d_0} e_{d'_{y,z}})$.
\item If $Sx'$ is undefined, add ``$z' \op' x' = e_{2Sx'} L_0 e_0 e_{Sx'} y'$'' as a pending identity.
\item If instead $Sx'$ is defined, but $L_0 e_0 e_{Sx'} y'$ is undefined, set $L_0 e_0 e_{Sx'} y' = e_{d''_{y,z}}$. Then set $x'' \op y'' = z''$, where $(x'',y'',z'') := (z', x', e_{2Sx'} e_{d''_{y,z}})$. Then add ``$z'' \op' x'' = e_{2Sx''} L_0 e_0 e_{Sx''} y''$'' as a pending identity.
\item If instead $L_0 e_0 e_{Sx'} y'$ is defined, set $x'' \op y'' = z''$, where $(x'',y'',z'') := (z', x', e_{2Sx'} L_0 e_0 e_{Sx'} y')$. Then add ``$z'' \op' x'' = e_{2Sx''} L_0 e_0 e_{Sx''} y''$'' as a pending identity.
\item Extend all the new definitions of $L_0$ using \Cref{itero}, \Cref{itero-2}.
\end{itemize}
One can check that these definitions do not cause any collisions in the partial function $L_0$, and that axioms (i'), (iii'), (iv''), (vii'), (P) are preserved; the remaining axioms (v''), (vi') are unaffected by this extension.
\end{proof}
Finally, we give a tool for enlarging $\op$:
\begin{proposition}[Enlarging $\op$]\label{enlarge-op} Suppose one has a partial solution in which $x \op' y$ is undefined for some $x,y \in N$. Then one can extend the partial solution so that $x \op' y$ is now defined.
\end{proposition}
\begin{proof} By applying \Cref{enlarge-S} as needed, we may assume without loss of generality that $Sx$ and $Sy$ are already defined (among other things, this removes the possibility that $x \op' y$ is part of a pending identity). If this makes $x \op' y$ defined, then we are done, so we may assume that this is not the case.
We now divide into cases:
Case 1: $x=y$. In this case we set $x \op' y := Sx$. It is clear that this preserves axiom (v''), and no other axiom is impacted.
Case 2: If $x = e_a y$ for some $a \in SM$, then we set $x \op' y := a - Sy$. This preserves axiom (vi''), and no other axiom is impacted.
Case 3: If $x$ is not equal to $y$ or $e_a y$ for any $a \in SM$. Let $d_0, d_1 \in SM$ be a generator that does not appear as a component of any index of any of the generators $e_a$ appearing anywhere in the partial solution. We set $x \op' y := z$ with $z := e_{d_0}$.
This temporarily disrupts axiom (vii''). To recover it, we perform the following actions.
\begin{itemize}
\item If $L_0 e_0 e_{Sx} y$ is not currently defined, we set it equal to $e_{d_1}$, and extend by \Cref{itero}, \Cref{itero-2}.
\item Set $x' \op y' = z'$, where $(x',y',z') := (z, x, e_{2Sx} L_0 e_0 e_{Sx} y)$.
\item Add ``$z' \op' x' = e_{2Sx'} L_0 e_0 e_{Sx'} y'$'' as a pending identity.
\end{itemize}
One can check that these definitions do not cause any collisions in the partial function $L_0$, and that axioms (i'), (vii'), (P) are preserved; the remaining axioms (S), (iii''), (iv''), (v''), (vi'') are unaffected by this extension.
\end{proof}
\begin{theorem}[1729 does not imply 817]\label{1729_refute_817} There exists a magma that obeys equation 1729 but not equation 817.
\end{theorem}
\begin{proof}
Applying the above propositions alternatingly, we can end up with a situation in which $S, \op', L_0$ are all total functions, which by axiom (P) ensures that no pending identities remain. Invoking \Cref{mag}, we conclude the claim.
\end{proof}