Austin implications
We now broaden the discussion to consider not only the implications to E2 \(({x = y})\), but also between any pair of equational laws. Many implications for finite magmas rely on the fact that if \(f, g:X \to X\) are functions on a finite set \(X\), then \(f \circ g = I\) if and only if \(g \circ f = I\). Two more complicated variants of this are as follows.
Lemmaffg#
Let \(X\) be finite, and let \(f, g: X \to X\) be such that \(f = f \circ f \circ g\). Then \(f = f \circ g \circ f\).
Proof
Call a point \(x \in X\) periodic if \(f^n(x) = x\) for some \(n>0\). Because the forward orbit \(x, f(x), f^2(x), \dots\) in a finite space \(X\) must repeat, we see that for each \(x\) there exists an \(n\) such that \(f^n(x)\) is periodic. Let \(n_x\) be the first \(n\) for which this occurs. If \(n_x > 1\), then \(g(x), f(g(x)), f(f(g(x))\) cannot be periodic (as this would imply \(f(x)\) periodic), and then we can see that \(n_{g(x)} = n_x + 1\). Hence the maximal value of \(n_x\) is at most \(1\), which implies that \(f(x)\) is periodic for every \(x\). Thus there is an \(n > 1\) such that \(f^n = f\). Since \(f = f^2 \circ g\), we have \(f^n = f^{n-2} \circ f \circ f = f^{n-2} \circ (f^2 \circ g) \circ f = f^n \circ g \circ f = f \circ g \circ f\), as desired.
Lean
Formalized as FiniteModel.Finite.f_ffg_implies_f_fgf.
Sources
Lemmagff#
Let \(X\) be finite, and let \(f, g: X \to X\) be such that \(f = g \circ f \circ f\). Then \(f = f \circ g \circ f\).
Proof
By hypothesis, \(f^2(x)\) uniquely determines \(f(x)\). This prevents \(n_x = 2\) for any \(x\) (because if \(n>2\) is such that \(f^{n+2}(x) = f^2(x)\), then \(f^{n+1}(x) \neq f(x)\)), and hence also prevents \(n_x > 2\) for any \(x\). So again we have \(f(x)\) periodic for all \(x\), so \(f^n = f\) for some \(n>1\). Then \(f = f^n = f \circ (g \circ f^2) \circ f^{n-2} = f \circ g \circ f^n = f \circ g \circ f\) as required.
Lean
Formalized as FiniteModel.Finite.f_gff_implies_f_fgf.
Sources
This can be used to obtain a few positive finite magma implications, for instance by setting \(f,g\) to be left and right multiplication operators. Another useful lemma is
LemmaEventual period#
Let \(X\) be finite and \(f: X \to X\). Then there exists \(n \geq 1\) such that \(f^{2n} = f^n\).
Proof
By the pigeonhole principle, there exists \(n \geq 1\), \(m \geq 0\) such that \(f^{m+n} = f^m\), which implies on iteration that \(f^{m+mn} = f^m\) and hence \(f^{2mn} = f^{mn}\), giving the claim.
Lean
Formalized as FiniteModel.Finite.fn_eventually_periodic'.
Sources
Used by 1
As a sample application, we have the following finite implications between laws of order up to \(4\).
Proposition3994 implies 3588 for finite models#
All finite magmas which satisfy E3994 \(({x \diamond y = (z \diamond (x \diamond y)) \diamond z})\) also satisfy E3588 \(({x \diamond y = z \diamond ((x \diamond y) \diamond z)})\).
Proof
For a finite magma \(M\), consider the set \(S = \{x \diamond y | x, y \in M\}\). Now \(f_z : x \mapsto z \diamond x\) and \(g_z : x \mapsto x \diamond z\). They both map \(S\) to \(S\), and due to the hypothesis \(g_z \diamond f_z\) is the identity on \(S\), so because \(S\) is finite \(f_z\) and \(g_z\) must be inverse bijections on it, and therefore they commute.
Lean
Formalized as InfModel.Finite.Equation3994_implies_Equation3588.
Sources
Uses 2
Proposition3994 does not imply 3588 for infinite models#
Proof
Consider \(\mathbb{N}\), with \(x \diamond y\) defined as \(x \oplus y\) (bitwise XOR) if \(x\) and \(y\) are even, \(y+2\) if only \(y\) is even, \(x \dot - 2\) if only \(x\) is even, and \(0\) if both are odd. Note that the range of the operation is the set of even naturals. E3994 is satisfied, because for even \(z\) we get \(z \oplus (x \diamond y) \oplus z = x \diamond y\) and for odd \(z\) we get \((x \diamond y) + 2 \dot - 2 = x \diamond y\). Setting \(x = y = z = 1\), E3588 isn't satisfied.
Lean
Formalized as InfModel.Equation3994_not_implies_Equation3588.
Sources
Uses 2
Proposition3342#
On a finite magma \(M\), equation 3342, \(x \diamond y= y \diamond (x \diamond (x \diamond x))\), implies equation 3522, \(x \diamond y = x \diamond ((y \diamond y) \diamond y)\), as well as equation 4118, \(x \diamond y = ((x \diamond x) \diamond x) \diamond y\).
Proof
Write \(Sx := x \diamond\), \(fx := x \diamond Sx\) and \(Cx = Sx \diamond x\), then we have \(x \diamond y= y \diamond fx\), and our task is to show \(x \diamond y = Cx \diamond y\) and \(x \diamond y = x \diamond Cy\) for finite magmas, giving the four open implications.
Note that \(x \diamond y= y \diamond fx = fx \diamond fy\), hence \(f\) is a homomorphism. By Eventual period, there is \(n \geq 1\) with \(f^n = f^{2n}\). From 3342 we have \(Sx = S fx\) and \(Cx = Sx \diamond x = f^n Sx \diamond f^n x = f^n Sx \diamond f^{2n} x = f^{2n-1} x \diamond f^n Sx = f^{n-1} x \diamond S x = f(f^{n-1} x) = f^n x\). Then
and a similar argument gives \(x \diamond Cy = x \diamond y\).
Lean
Formalized as Eq3342.Finite.Equation3342_implies_Equation3522, Eq3342.Finite.Equation3342_implies_Equation4118.
Sources
Uses 1
Proposition1167 implies 1096#
For finite magmas, Equation 1167,
implies Equation 1096,
Proof
We write 1167 as
hence \(L_y\) is invertible and \(L_{z \diamond Sy} L_y = I\). In particular \(L_{z \diamond Sy} Sy = y\), hence squaring is injective, hence surjective. So 1167 can be rewritten as \(L_{S^{-1} y} L_{z \diamond y} = I\), hence \(L_{z \diamond y}\) is independent of \(z\). In particular
by 1167, hence the right-hand side of 1096 is independent of \(z\). Replacing \(z\) with \(y\), the claim now follows from 1167.
Lean
Formalized as Eq1133.Finite.Equation1167_implies_Equation1096.
Sources
Proposition1133 implies 1167#
For finite magmas, Equation 1133,
implies Equation 1167,
Proof
1133 asserts that \(L_y L_{y \diamond (z \diamond y)} = I\), hence \(L_y\) is invertible and \(L_{y \diamond (z \diamond y)} = L_y^{-1}\) does not depend on \(z\). Setting \(z = y \diamond Sy\) we see from 1133 that \(y \diamond (z \diamond y) = y\) and hence we have left-involution: \(L_y = L_y^{-1}\). Replacing \(y\) with \(L_z y\) in 1133 we now get \(L_{L_z y} L_{L_z y \diamond y} = I\), which since \(L_{L_z y}\) is its own inverse gives
In particular
hence as \(L_{R_y^2 z}\) is its own inverse
Thus squaring is surjective, hence invertible.
Next, by (1) we have \(L_{z \diamond Sy} = L_w\) where \(w = R_{Sy}^2 z\). By (1) and the fact that \(L_w\) is its own inverse, we have
hence \(Sw = L_w w = Sy\). As \(S\) is injective, we have \(L_w = L_y\), and then \(L_y L_{z \diamond Sy} = L_y^2 = I\), giving 1167.
Lean
Formalized as Eq1133.Finite.Equation1133_implies_Equation1167.
Sources
Proposition1441 implies 4067, 1443 implies 3055#
For finite magmas, Equation 1441,
implies Equation 4067,
and equation 1443,
implies Equation 3055,
Proof
Write \(\tilde C x = x \diamond Sx\), then 1441 asserts that \(R_{\tilde Cx} R_y x = x\). Setting
we get \(x = S\tilde Cx\), so by finiteness \(\tilde C Sx = x\). Replacing \(x\) with \(Sx\) in 1441 we conclude \(R_x R_y Sx = Sx\) which is 4067.
Clearly 1443 implies 1441, hence 4067 by the previous implication, so that 3055 simplifies to \(x = Sx \diamond x\). Meanwhile, 1443 also implies \(x = S(x \diamond (x \diamond z))\). On taking square roots and using \(S \tilde C = x\), we obtain \(x \diamond (x \diamond z) = \tilde Cx\). Applying this with \(z = Sx\) we conclude \(L_x \tilde Cx = \tilde Cx\), hence on replacing \(x\) with \(Sx\) we get \(L_{Sx} x = x\) as required.
Lean
Formalized as Eq1441.Finite.Equation1441_implies_Equation4067, Eq1441.Finite.Equation1443_implies_Equation3055.
Sources
Proposition1681 implies 3877, 1701 implies 1035#
For finite magmas, Equation 1681,
implies Equation 3877,
and Equation 1701,
implies Equation 1035,
Proof
This is very similar to the previous proof. Write \(Cx = Sx \diamond x\), then 1681 asserts \(R_{Cx} L_y x = x\). Again setting \(y=Sx\) yields \(x=SCx\) hence \(x = CSx\), and on replacing \(x\) with \(Sx\) in 1681 one obtains 3877.
For the second part, we simplify to \(x = x \diamond Sx\), while 1701 gives \(x = S((z \diamond x) \diamond x)\) hence \((z \diamond x) \diamond x = Cx\), so \(R_x Cx = Cx\), so \(R_{Sx} x = x\) as required.
Lean
Formalized as Eq1441.Finite.Equation1681_implies_Equation3877, Eq1441.Finite.Equation1701_implies_Equation1035.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.