Equation 854
In this chapter we study magmas that satisfy E854, thus
for all \(x,y,z\). In particular we have
substituting \(z = (x \diamond x)^2\) we have in particular that
We then have
and thus by another application of (1) we conclude the useful law
(equation 378). We introduce the notation \(y \to x\) to denote the relation that \(x = z \diamond y\) for some \(z\), then from (3) we see that
From (1) we have
for all \(x,y,z\).
Now let \(X\) be an alphabet, and \(M_X\) the free magma. We let \(\Gamma\) be the theory consisting just of the law (1), then as in Existence and uniqueness of free magmas we have the equivalence relation \(\sim\) on \(M_X\) defined by setting \(w \sim w'\) iff \(\Gamma \models w \simeq w'\), then \(M_X/\sim\) is a free magma for \(\Gamma\). We can then also define a directed graph on \(M_X\) by declaring \(w' \to w\) if \(w \sim w'' \diamond w'\) for some \(w''\), or equivalently (by applying (4) to \(M_X/\sim\)) that \(w \sim w \diamond w'\).
Call a word \(w\) irreducible if it is not of the form \(w = w_1 \diamond w_2\) with \(w_2 \to w_1\), and reducible otherwise. Clearly if a word \(w = w_1 \diamond w_2\) is reducible, then it is equivalent to the shorter word \(w_1\). Iterating, we conclude that every word is equivalent to an irreducible word. Such a word is either a generator in \(X\), or else a product \(w_1 \to w_2\) with \(w_2 \not \to w_1\).
We have two useful corollaries:
CorollaryUnique factorization#
Two irreducible words \(w, w'\) are equivalent if and only if they are either the same generator of \(X\), or are of the form \(w = w_1 \diamond w_2\), \(w' = w'_1 \diamond w'_2\) with \(w_1 \sim w'_1\) and \(w_2 \sim w'_2\).
Proof
Immediate from Description of equivalence.
Lean
Formalized as Refutation_854.unique_factorization.
Sources
We can now prove some anti-implications.
Theorem854 does not imply 3316, 3925#
The laws
and
are not implied by E854.
Proof
We work in the free group \(M_X\) on two generators \(X = \{x,y\}\). It suffices to show that
and
We begin with the first claim. Suppose this were not the case, then by Unique factorization one of the following statements must hold:
-
(i)
\[ y \to x. \] -
(ii)
\[ (y \diamond (x \diamond y)) \to x. \] -
(iii)
\[ y \diamond (x \diamond y) \sim y. \]
If (i) holds, then we have \(x \diamond y = x\) (Equation 4) in \(M_X/\sim\), hence in every magma satisfying E854. But we have examples of such magmas in which this fails.
Similarly, if (iii) holds, then \(y \diamond (x \diamond y) = y\) (Equation 10) holds in \(M_X/\sim\), hence in every magma satisfying E854. But we have examples of such magmas in which this fails.
Finally, if (ii) holds, then the claim
to refute simplifies to
and we are back to (i), which we already know not to be the case.
For the latter equation, we similarly have the cases
-
(iv)
\[ y \to x. \] -
(v)
\[ y \to x \diamond (y \diamond x). \] -
(vi)
\[ x \sim x \diamond (y \diamond x). \]
(iv) is (i), which was already ruled out, and (vi) is similarly a relabeled version of (iii). In case (v) holds, the claim to refute simplifies to
and using Unique factorization we reduce to either \(y \sim y \diamond x\), \(y \to x\), or \(y \diamond x \to x\), and each of these is already known to fail.
Lean
Stated as Refutation_854.not_3316_3925; the blueprint marks no proof of it as formalized.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.