General implications
We will be interested in seeing which laws imply which other laws, in the sense that magmas satisfying the former law automatically satisfy the latter. We will also be interested in anti-implications showing that one law does not imply another, by producing examples of magmas that satisfy the former law but not the latter. Here is a formal definition.
Note that we view the stronger law as less than or equal to the weaker law. This is because the class of magmas that satisfy the stronger law is a subset of the class of magmas that satisfy the weaker law. It is also consistent with the conventions of Lean's Mathlib.
Implications between the laws from Selected laws are depicted in Figure 1.
Figure 1. Implications between the above equations, displayed as a Hasse diagram. (The picture is not reproduced here.)
LemmaMaximal element#
The law \(0 \simeq 0\) is the maximal element in this pre-order.
Proof
Trivial.
Lean
Stated as Law.MagmaLaw.Equation1_maximal; the blueprint marks no proof of it as formalized.
Sources
LemmaMinimal element#
The law \(0 \simeq 1\) is the minimal element in this pre-order.
Proof
Trivial.
Lean
Stated as Law.MagmaLaw.Equation2_minimal; the blueprint marks no proof of it as formalized.
Sources
Every magma \(G\) has a reversal \(G^{\mathrm{op}}\), formed by by replacing the magma operation \(\diamond\) with its opposite \(\diamond^{\mathrm{op}}:(x,y) \mapsto y \diamond x\). There is a natural isomorphism between these magmas, which induces an involution \(w \mapsto w^{\mathrm{op}}\) on words \(w \in M_X\). Every law \(w \simeq w'\) then has a dual \(w^{\mathrm{op}} \simeq (w')^{\mathrm{op}}\).
For instance, the dual of the law \(0 \diamond 1 = 0 \diamond 2\) is \(1 \diamond 0 = 2 \diamond 0\), which after relabeling is \(0 \diamond 1 = 2 \diamond 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:
LemmaDuality of laws#
The law \(w \simeq w'\) implies \(w''\simeq w'''\), if and only if \(w^{\mathrm{op}} \simeq (w')^{\mathrm{op}}\) implies \(w''^{\mathrm{op}} \simeq (w''')^{\mathrm{op}}\).
Proof
This follows from the fact that a magma \(G\) satisfies a law \(w \simeq w'\) if and only if \(G^{\mathrm{op}}\) satisfies \(w^{\mathrm{op}} \simeq (w')^{\mathrm{op}}\).
Lean
Stated as Law.MagmaLaw.implies_iff_dual; the blueprint marks no proof of it as formalized.
Sources
Used by 1
Thus for instance, E7 \(({x = y \diamond z})\) is equivalent to E2 \(({x = y})\).
TheoremCriterion for implication#
If \(w \simeq w'\) is such that every variable appears the same number of times in both \(w\) and \(w'\), and \(w \simeq w'\) implies another law \(w'' \simeq w'''\), then every variable appears the same number of times in both \(w''\) and \(w'''\).
Proof
Consider the magma \(\mathrm{MS}\) of multisets over an arbitrary set \(A\) (which can be seen as finitely supported maps \(A\rightarrow \mathbb{N}\)), with the multiset addition law \(+\). By hypothesis, this magma satisfies \(w \simeq w'\), and hence \(w'' \simeq w'''\), giving the claim by comparing the orders of the elements of \(A\) appearing in \(w''\) and \(w'''\) in this magma.
Lean
Stated as Law.MagmaLaw.SameCount.derive; the blueprint marks no proof of it as formalized.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.