4 General implications

We will be interested in seeing which laws imply which other laws, in the sense that magmas obeying the former law automatically obey the latter. We will also be interested in anti-implications showing that one law does not imply another, by producing examples of magmas that obey the former law but not the latter. Here is a formal definition.

Definition 4.1 Implication

A law $E$ is said to imply another law $E^{'}$ if ${E} ⊨ E^{'}$ , or equivalently:

G ⊨ w ≃ w^{'} ⟹ G ⊨ w^{″} ≃ w^{‴} for all magmas G

Two laws are said to be equivalent if they imply each other.

Lemma 4.2 Pre-order

✓

If we define $E \leq E^{'}$ if $E$ implies $E^{'}$ , then this is a pre-order on the set of laws, and equivalence is an equivalence relation.

Note that we view the stronger law as less than or equal to the weaker law. This is because the class of magmas that obey the stronger law is a subset of the class of magmas that obey the weaker law. It is also consistent with the conventions of Lean’s Mathlib.

Proof ▶

Implications between the laws from Chapter 2 are depicted in Figure 4.1.

\includegraphics[width=1\linewidth ]{../../images/subgraph.png} — Figure 4.1 Implications between the above equations, displayed as a Hasse diagram.

Lemma 4.3 Maximal element

The law $0 ≃ 0$ is the maximal element in this pre-order.

Proof ▶

Lemma 4.4 Minimal element

The law $0 ≃ 1$ is the minimal element in this pre-order.

Proof ▶

Every magma $G$ has a reversal $G^{op}$ , formed by by replacing the magma operation $⋄$ with its opposite $⋄^{op} : (x, y) \mapsto y ⋄ x$ . There is a natural isomorphism between these magmas, which induces an involution $w \mapsto w^{op}$ on words $w \in M_{X}$ . Every law $w ≃ w^{'}$ then has a dual $w^{op} ≃ (w^{'})^{op}$ .

For instance, the dual of the law $0 ⋄ 1 = 0 ⋄ 2$ is $1 ⋄ 0 = 2 ⋄ 0$ , which after relabeling is $0 ⋄ 1 = 2 ⋄ 1$ . A list of equations and their duals can be found here. Of the 4694 equations under consideration, 84 are self-dual, leaving 2305 pairs of dual equations.

The pre-ordering on laws has a duality symmetry:

Lemma 4.5 Duality of laws

The law $w ≃ w^{'}$ implies $w^{″} ≃ w^{‴}$ , if and only if $w^{op} ≃ (w^{'})^{op}$ implies $w^{″ op} ≃ (w^{‴})^{op}$ .

Proof ▶

This follows from the fact that a magma $G$ satisfies a law $w ≃ w^{'}$ if and only if $G^{op}$ satisfies $w^{op} ≃ (w^{'})^{op}$ .

Some equational laws can be “diagonalized”:

Theorem 4.6 Diagonalization

An equational law of the form

F (x_{1}, \dots, x_{n}) = G (y_{1}, \dots, y_{m}),

where $x_{1}, \dots, x_{n}$ and $y_{1}, \dots, y_{m}$ are distinct elements of the alphabet, implies the diagonalized law

F (x_{1}, \dots, x_{n}) = F (x_{1}^{'}, \dots, x_{n}^{'}) .

where $x_{1}^{'}, \dots, x_{n}^{'}$ are distinct from $x_{1}, \dots, x_{n}$ In particular, if $G (y_{1}, \dots, y_{m})$ can be viewed as a specialization of $F (x_{1}^{'}, \dots, x_{n}^{'})$ , then these two laws are equivalent.

Proof ▶

From two applications of Equation 1 one has

F (x_{1}, \dots, x_{n}) = G (y_{1}, \dots, y_{m})

and

F (x_{1}^{'}, \dots, x_{n}^{'}) = G (y_{1}, \dots, y_{m})

whence the claim.

Thus for instance, Definition 2.7 is equivalent to Definition 2.2.

Theorem 4.7 Laws implied by the constant law

If $w, w^{'}$ each have order at least one, then the law $w ≃ w^{'}$ is implied by the constant law (Definition 2.20). If exactly one of $w, w^{'}$ has order zero, and the law $w ≃ w^{'}$ is not implied by the constant law.

Proof ▶

Theorem 4.8 Criterion for implication

If $w ≃ w^{'}$ is such that every variable appears the same number of times in both $w$ and $w^{'}$ , and $w ≃ w^{'}$ implies another law $w^{″} ≃ w^{‴}$ , then every variable appears the same number of times in both $w^{″}$ and $w^{‴}$ .

Proof ▶

Consider the magma $MS$ of multisets over an arbitrary set $A$ (which can be seen as finitely supported maps $A \to N$ ), with the multiset addition law $+$ . By hypothesis, this magma obeys $w ≃ w^{'}$ , and hence $w^{″} ≃ w^{‴}$ , giving the claim by comparing the orders of the elements of $A$ appearing in $w^{″}$ and $w^{‴}$ in this magma. □