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#

For finite magmas, equation 906 implies equation 3862,

\[ (x \diamond (x \diamond x)) \diamond x = x \diamond x.\qquad\text{(5)} \]
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

Formalized as Eq906.Finite.Equation906_implies_Equation3862.

Sources

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.