Equation 906
In this chapter we study finite magmas that satisfy equation 906,
\[
x = y \diamond ((y \diamond x) \diamond (x \diamond x))\qquad\text{(1)}
\]
for all \(x,y\). We can write this as
\[
L_y (L_y x \diamond Sx) = x.\qquad\text{(2)}
\]
This implies that \(L_y\) is surjective, hence invertible by finiteness, so
\[
L_y x \diamond Sx = L_y^{-1} x.\qquad\text{(3)}
\]
Setting \(n = N-2\) for \(N>2\) a common period of \(L_y,L_z\) (which exists by finiteness) we conclude that
\[
L_y x = L_z x \implies L_y^2 x = L_z^2 x.\qquad\text{(4)}
\]
Theorem906-3862#
Eq906.Finite.Equation906_implies_Equation3862
For finite magmas, equation 906 implies equation 3862,
\[
(x \diamond (x \diamond x)) \diamond x = x \diamond x.\qquad\text{(5)}
\]
Proof
Proof
Observe from (2) that
\[
L_x S^2 x = L_x (L_x x \diamond Sx) = x
\]
while from (3) we have
\[
L_{L_x Sx} S^2 x = L_x Sx \diamond S S x = L_x^{-1} Sx = x.
\]
Thus
\[
L_x S^2 x = L_{L_x Sx} S^2 x = x
\]
and hence by the \(n=2\) case of Edge disjointness of left cycles
\[
L_x x = L_{L_x Sx} x
\]
giving the claim.
Lean
Lean
Formalized as Eq906.Finite.Equation906_implies_Equation3862.
Sources
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.