generated from pitmonticone/LeanProject
-
Notifications
You must be signed in to change notification settings - Fork 66
/
Copy pathequations.tex
293 lines (181 loc) · 15.8 KB
/
equations.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
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
\chapter{Selected laws}\label{subgraph-eq}
In this project we study the 4694 laws (up to symmetry and relabeling) of total order at most $4$.
Selected laws of interest are listed below, as well as in \href{https://github.com/teorth/equational_theories/blob/main/equational_theories/Equations/Basic.lean}{this file}.
\begin{definition}[Equation 1]\label{eq1}\lean{Equation1}\leanok\uses{magma-def} Equation 1 is the law $0 \formaleq 0$ (or the equation $x=x$).
\end{definition}
This is the trivial law, satisfied by all magmas. It is self-dual.
\begin{definition}[Equation 2]\label{eq2}\lean{Equation2}\leanok\uses{magma-def} Equation 2 is the law $0 \formaleq 1$ (or the equation $x=y$).
\end{definition}
This is the singleton law, satisfied only by the empty and singleton magmas. It is self-dual.
\begin{definition}[Equation 3]\label{eq3}\lean{Equation3}\leanok\uses{magma-def} Equation 3 is the law $0 \formaleq 0 \op 0$ (or the equation $x = x \op x$).
\end{definition}
This is the idempotence law. It is self-dual.
\begin{definition}[Equation 4]\label{eq4}\lean{Equation4}\leanok\uses{magma-def} Equation 4 is the law $0 \formaleq 0 \op 1$ (or the equation $x = x \op y$).
\end{definition}
This is the left absorption law.
\begin{definition}[Equation 5]\label{eq5}\lean{Equation5}\leanok\uses{magma-def} Equation 5 is the law $0 \formaleq 1 \op 0$ (or the equation $x = y \op x$).
\end{definition}
This is the right absorption law (the dual of \Cref{eq4}).
\begin{definition}[Equation 6]\label{eq6}\lean{Equation6}\leanok\uses{magma-def} Equation 6 is the law $0 \formaleq 1 \op 1$ (or the equation $x = y \op y$).
\end{definition}
This law is equivalent to the singleton law.
\begin{definition}[Equation 7]\label{eq7}\lean{Equation7}\leanok\uses{magma-def} Equation 7 is the law $0 \formaleq 1 \op 2$ (or the equation $x = y \op z$).
\end{definition}
This law is equivalent to the singleton law.
\begin{definition}[Equation 8]\label{eq8}\lean{Equation8}\leanok\uses{magma-def} Equation 8 is the law $0 \formaleq 0 \op (0 \op 0)$ (or the equation $x = x \op (x \op x)$).
\end{definition}
\begin{definition}[Equation 14]\label{eq14}\lean{Equation14}\leanok\uses{magma-def} Equation 14 is the law $0 \formaleq 1 \op (0 \op 1)$ (or the equation $x = y \op (x \op y))$.
\end{definition}
Appears in Problem A1 from Putnam 2001. See \Cref{29_equiv_14}.
\begin{definition}[Equation 16]\label{eq16}\lean{Equation16}\leanok\uses{magma-def} Equation 16 is the law $0 \formaleq 1 \op (1 \op 0)$ (or the equation $x = y \op (y \op x))$.
\end{definition}
\begin{definition}[Equation 23]\label{eq23}\lean{Equation23}\leanok\uses{magma-def} Equation 23 is the law $0 \formaleq (0 \op 0) \op 0$ (or the equation $x = (x \op x) \op x$).
\end{definition}
This is the dual of \Cref{eq8}.
\begin{definition}[Equation 29]\label{eq29}\lean{Equation29}\leanok\uses{magma-def} Equation 29 is the law $0 \formaleq (1 \op 0) \op 1$ (or the equation $x = (y \op x) \op y)$.
\end{definition}
Appears in Problem A1 from Putnam 2001. Dual to \Cref{eq14}. See \Cref{29_equiv_14}.
\begin{definition}[Equation 38]\label{eq38}\lean{Equation38}\leanok\uses{magma-def} Equation 38 is the law $0 \op 0 \formaleq 0 \op 1$ (or the equation $x \op x = x \op y$).
\end{definition}
This law asserts that the magma operation is independent of the second argument.
\begin{definition}[Equation 39]\label{eq39}\lean{Equation39}\leanok\uses{magma-def} Equation 39 is the law $0 \op 0 \formaleq 1 \op 0$ (or the equation $x \op x = y \op x$).
\end{definition}
This law asserts that the magma operation is independent of the first argument (the dual of \Cref{eq38}).
\begin{definition}[Equation 40]\label{eq40}\lean{Equation40}\leanok\uses{magma-def} Equation 40 is the law $0 \op 0 \formaleq 1 \op 1$ (or the equation $x \op x = y \op y$).
\end{definition}
This law asserts that all squares are constant. It is self-dual.
\begin{definition}[Equation 41]\label{eq41}\lean{Equation41}\leanok\uses{magma-def} Equation 41 is the law $0 \op 0 \formaleq 1 \op 2$ (or the equation $x \op x = y \op z$).
\end{definition}
This law is equivalent to the constant law, \Cref{eq46}.
\begin{definition}[Equation 42]\label{eq42}\lean{Equation42}\leanok\uses{magma-def} Equation 42 is the law $0 \op 1 \formaleq 0 \op 2$ (or the equation $x \op y = x \op z$).
\end{definition}
Equivalent to \Cref{eq38}.
\begin{definition}[Equation 43]\label{eq43}\lean{Equation43}\leanok\uses{magma-def} Equation 43 is the law $0 \op 1 \formaleq 1 \op 0$ (or the equation $x \op y = y \op x$).
\end{definition}
The commutative law. It is self-dual.
\begin{definition}[Equation 45]\label{eq45}\lean{Equation45}\leanok\uses{magma-def} Equation 45 is the law $0 \op 1 \formaleq 2 \op 1$ (or the equation $x \op y = z \op y$).
\end{definition}
This is the dual of \Cref{eq42}.
\begin{definition}[Equation 46]\label{eq46}\lean{Equation46}\leanok\uses{magma-def} Equation 46 is the law $0 \op 1 \formaleq 2 \op 3$ (or the equation $x \op y = z \op w$).
\end{definition}
The constant law: all products are constant. It is self-dual.
\begin{definition}[Equation 63]\label{eq63}\lean{Equation63}\leanok\uses{magma-def} Equation 63 is the law $0 \formaleq 1 \op (0 \op (0 \op 1))$ (or the equation $x = y \op (x \op (x \op y))$).
\end{definition}
The ``Dupont'' law, studied further in \Cref{dupont-section}.
\begin{definition}[Equation 65]\label{eq65}\lean{Equation65}\leanok\uses{magma-def} Equation 65 is the law $0 \formaleq 1 \op (0 \op (1 \op 0))$ (or the equation $x = y \op (x \op (y \op x))$).
\end{definition}
The ``Asterix'' law, studied further in \Cref{asterix-section}.
\begin{definition}[Equation 168]\label{eq168}\lean{Equation168}\leanok\uses{magma-def} Equation 168 is the law $0 \formaleq (1 \op 0) \op (0 \op 2)$ (or the equation $x = (y \op x) \op (x \op z)$).
\end{definition}
The law of a central groupoid. It is self-dual.
\begin{definition}[Equation 206]\label{eq206}\lean{Equation206}\leanok\uses{magma-def} Equation 206 is the law $0 \formaleq (0 \op (0 \op 1)) \op 1$ (or the equation $x = (x \op (x \op y)) \op y$).
\end{definition}
Our project located this law as one member of an ``Austin pair''; see \Cref{infinite-model-chapter}. The infinite counterexample is constructed using the infinite 3-regular tree.
\begin{definition}[Equation 381]\label{eq381}\lean{Equation381}\leanok\uses{magma-def} Equation 381 is the law $0 \op 1 \formaleq (0 \op 2) \op 1$ (or the equation $x \op y = (x \op z) \op y$).
\end{definition}
Appears in Putnam 1978, Problem A4, part (b).
\begin{definition}[Equation 387]\label{eq387}\lean{Equation387}\leanok\uses{magma-def} Equation 387 is the law $0 \op 1 \formaleq (1 \op 1) \op 0$ (or the equation $x \op y = (y \op y) \op x$).
\end{definition}
Introduced in \href{https://mathoverflow.net/a/450905/766}{MathOverflow}. See \Cref{387_implies_43}
\begin{definition}[Equation 477]\label{eq477}\lean{Equation477}\leanok\uses{magma-def} Equation 477 is the law $0 \formaleq 1 \op (0 \op (1 \op (1 \op 1)))$ (or the equation $x = y \op (x \op (y \op (y \op y)))$).
\end{definition}
An example of a confluent law; see \Cref{477-confl}.
\begin{definition}[Equation 854]\label{eq854}\lean{Equation953}\leanok\uses{magma-def} Equation 854 is the law $0 = 0 \op ((1 \op 2) \op (0 \op 2))$ (or the equation $x = x \op ((y \op z) \op (x \op z))$).
\end{definition}
Studied in \Cref{854-chapter}
\begin{definition}[Equation 953]\label{eq953}\lean{Equation953}\leanok\uses{magma-def} Equation 953 is the law $0 = 1 \op ((2 \op 0) \op (2 \op 2))$ (or the equation $x = y \op ((z \op x) \op (z \op z))$).
\end{definition}
An example of a trivial law; see \Cref{953_equiv_2}.
\begin{definition}[Equation 1485]\label{eq1485}\lean{Equation1491}\leanok\uses{magma-def} Equation 1485 is the law $0 \formaleq (1 \op 0) \op (0 \op (2 \op 1))$ (or the equation $x = (y \op x) \op (x \op (z \op y))$).
\end{definition}
The ``Obelix'' law, studied further in \Cref{asterix-section}.
\begin{definition}[Equation 1491]\label{eq1491}\lean{Equation1491}\leanok\uses{magma-def} Equation 1491 is the law $0 \formaleq (1 \op 0) \op (1 \op (1 \op 0))$ (or the equation $x = (y \op x) \op (y \op (y \op x))$).
\end{definition}
The ``Obelix'' law, studied further in \Cref{asterix-section}.
\begin{definition}[Equation 1571]\label{eq1571}\lean{Equation1571}\leanok\uses{magma-def} Equation 1571 is the law $0 \formaleq (1 \op 2) \op (1 \op (0 \op 2))$ (or the equation $x = (y \op z) \op (y \op (x \op z))$).
\end{definition}
Introduced in \cite{mendelsohn-padmanabhan}. As shown in \Cref{1571_impl}, this law characterizes abelian groups of exponent two.
\begin{definition}[Equation 1648]\label{eq1648}\lean{Equation1648}\leanok\uses{magma-def} Equation 1648 is the law $0 \formaleq (0 \op 1) \op ((0 \op 1) \op 1)$ (or the equation $x = (x \op y) \op ((x \op y) \op y)$).
\end{definition}
The golden ratio is a coefficient of the linearization of this law.
\begin{definition}[Equation 1657]\label{eq1657}\lean{Equation1657}\leanok\uses{magma-def} Equation 1657 is the law $0 \formaleq (0 \op 1) \op ((1 \op 1) \op 0)$ (or the equation $x = (x \op y) \op ((y \op y) \op x)$).
\end{definition}
\begin{definition}[Equation 1659]\label{eq1659}\lean{Equation1659}\leanok\uses{magma-def} Equation 1659 is the law $0 \formaleq (0 \op 1) \op ((1 \op 1) \op 2)$ (or the equation $x = (x \op y) \op ((y \op y) \op z)$).
\end{definition}
\begin{definition}[Equation 1661]\label{eq1661}\lean{Equation1661}\leanok\uses{magma-def} Equation 1661 is the law $0 \formaleq (0 \op 1) \op ((1 \op 2) \op 1)$ (or the equation $x = (x \op y) \op ((y \op z) \op y)$).
\end{definition}
These two laws admit infinite models on the natural numbers arising from the modified base model construction. See \Cref{infinite-examples-section}.
\begin{definition}[Equation 1689]\label{eq1689}\lean{Equation1689}\leanok\uses{magma-def} Equation 1689 is the law $0 \formaleq (1 \op 0) \op ((0 \op 2) \op 2)$ (or the equation $x = (y \op x) \op ((x \op z) \op z)$).
\end{definition}
Mentioned in \cite{Kisielewicz2}. See \Cref{1689_equiv_2}.
\begin{definition}[Equation 1701]\label{eq1701}\lean{Equation1701}\leanok\uses{magma-def} Equation 1701 is the law $0 \formaleq (1 \op x) \op ((2 \op 0) \op 0)$ (or the equation $x = (y \op x) \op ((z \op x) \op x)$).
\end{definition}
This law admits infinite models on the natural numbers arising from the modified base model construction. See \Cref{infinite-examples-section}.
\begin{definition}[Equation 2662]\label{eq2662}\lean{Equation2662}\leanok\uses{magma-def} Equation 2662 is the law $0 \formaleq ((0 \op 1) \op (0 \op 1)) \op 0$ (or the equation $x = ((x \op y) \op (x \op y)) \op x$).
\end{definition}
Appears in \cite{mendelsohn-padmanabhan}.
\begin{definition}[Equation 3167]\label{eq3167}\lean{Equation3167}\leanok\uses{magma-def} Equation 3167 is the law $0 \formaleq (((1 \op 1) \op 2) \op 2) \op 0$ (or the equation $x = (((y \op y) \op z) \op z) \op x$).
\end{definition}
\begin{definition}[Equation 3588]
\label{eq3588}\lean{Equation3588}\leanok\uses{magma-def}
Equation 3588 is the law $0 \op 1 \formaleq 2 \op ((0 \op 1) \op 2)$ (or the equation $x \op y = z \op ((x \op y) \op z)$).
\end{definition}
Our project located this law as one member of an ``Austin pair''; see \Cref{infinite-model-chapter}.
\begin{definition}[Equation 3722]\label{eq3722}\lean{Equation3722}\leanok\uses{magma-def} Equation 3722 is the law $0 \op 1 \formaleq (0 \op 1) \op (0 \op 1)$ (or the equation $x \op y = (x \op y) \op (x \op y)$).
\end{definition}
Appears in Putnam 1978, Problem A4, part (a). It is self-dual.
\begin{definition}[Equation 3744]\label{eq3744}\lean{Equation3744}\leanok\uses{magma-def} Equation 3744 is the law $0 \op 1 \formaleq (0 \op 2) \op (3 \op 1)$ (or the equation $x \op y = (x \op z) \op (w \op y)$).
\end{definition}
This law is called a ``bypass operation'' in Putnam 1978, Problem A4. It is self-dual. See \Cref{3744_implies_3722_381}.
\begin{definition}[Equation 3994]
\label{eq3994}\uses{magma-def}
Equation 3994 is the law $0 \op 1 \formaleq (2 \op (0 \op 1)) \op 2$ (or the equation $x \op y = (z \op (x \op y)) \op z$).
\end{definition}
Our project located this law as one member of an ``Austin pair''; see \Cref{infinite-model-chapter}.
\begin{definition}[Equation 4315]\label{eq4315}\lean{Equation4315}\leanok\uses{magma-def} Equation 4315 is the law $0 \op (1 \op 0) \formaleq 0 \op (1 \op 2)$ (or the equation $x \op (y \op x) = x \op (y \op z)$).
\end{definition}
\begin{definition}[Equation 4512]\label{eq4512}\lean{Equation4512}\leanok\uses{magma-def} Equation 4512 is the law $0 \op (1 \op 2) \formaleq (0 \op 1) \op 2$ (or the equation $x \op (y \op z) = (x \op y) \op z$).
\end{definition}
The associative law. It is self-dual.
\begin{definition}[Equation 4513]\label{eq4513}\lean{Equation4513}\leanok\uses{magma-def} Equation 4513 is the law $0 \op (1 \op 2) \formaleq (0 \op 1) \op 3$ (or the equation $x \op (y \op z) = (x \op y) \op w$).
\end{definition}
\begin{definition}[Equation 4522]\label{eq4522}\lean{Equation4522}\leanok\uses{magma-def} Equation 4522 is the law $0 \op (1 \op 2) \formaleq (0 \op 3) \op 4$ (or the equation $x \op (y \op z) = (x \op w) \op u$).
\end{definition}
Dual to \Cref{eq4579}.
\begin{definition}[Equation 4564]\label{eq4564}\lean{Equation4564}\leanok\uses{magma-def} Equation 4564 is the law $0 \op (1 \op 2) \formaleq (3 \op 1) \op 2$ (or the equation $x \op (y \op z) = (w \op y) \op z$).
\end{definition}
Dual to \Cref{eq4513}.
\begin{definition}[Equation 4579]\label{eq4579}\lean{Equation4579}\leanok\uses{magma-def} Equation 4579 is the law $0 \op (1 \op 2) \formaleq (3 \op 4) \op 2$ (or the equation $x \op (y \op z) = (w \op u) \op z$).
\end{definition}
Dual to \Cref{eq4522}.
\begin{definition}[Equation 4582]\label{eq4582}\lean{Equation4582}\leanok\uses{magma-def} Equation 4582 is the law $0 \op (1 \op 2) \formaleq (3 \op 4) \op 5$ (or the equation $x \op (y \op z) = (w \op u) \op v$).
\end{definition}
This law asserts that all triple constants (regardless of bracketing) are constant.
\section{Equations of order greater than \texorpdfstring{$4$}{4}}
We note some selected laws of order more than $5$, which are used in some later chapters of the blueprint.
\begin{definition}[Equation 5093]
\label{eq5093}\uses{magma-def}\lean{Equation5093}\leanok
Equation 5093 is the law $0 \formaleq 1 \op (1 \op (1 \op (0 \op (2 \op 1))))$ (or the equation $x = y \op (y \op (y \op (x \op (z \op y))))$).
\end{definition}
This law of order $5$ was mentioned in \cite{Kisielewicz2}. See \Cref{5093-nontrivial}.
\begin{definition}[Equation 26302]
\label{eq26302}\uses{magma-def}
Equation 26302 is the law $0 \formaleq (1 \op ((2 \op 0) \op 3)) \op (0 \op 3)$ (or the equation $x = (y \op ((z \op x) \op w)) \op (x \op w)$).
\end{definition}
A law that characterizes natural central groupoids; see \Cref{natural-central-groupoid}.
\begin{definition}[Equation 28770]
\label{eq28770}\uses{magma-def}\lean{Equation28770}\leanok
Equation 28770 is the law $0 \formaleq (((1 \op 1) \op 1) \op 0) \op (1 \op 2)$ (or the equation $x = (((y \op y) \op y) \op x) \op (y \op z)$).
\end{definition}
This law of order $5$ was introduced by Kisielewicz \cite{Kisielewicz}. See \Cref{kis-thm2}.
\begin{definition}[Equation 345169]
\label{eq345169}\uses{magma-def}
Equation 345169 is the law $0 \formaleq (1 \op ((0 \op 1) \op 1)) \op (0 \op (2 \op 1))$ (or the equation $x = (y \op ((x \op y) \op y)) \op (x \op (z \op y))$).
\end{definition}
This law of order $6$ was shown in \cite{mccune_et_al} to characterize the Sheffer stroke in a boolean algebra; see \Cref{sheffer}.
\begin{definition}[Equation 374794]
\lean{Equation374794}\leanok
\label{eq374794}\uses{magma-def}
Equation 374794 is the law $0 \formaleq (((1 \op 1) \op 1) \op 0) \op ((1 \op 1) \op 2)$ (or the equation $x = (((y \op y) \op y) \op x) \op ((y \op y) \op z)$).
\end{definition}
This law of order $6$ was introduced by Kisielewicz \cite{Kisielewicz}; see \Cref{kis-thm}.