% Problem: The Circle Operation in Strongly Right Alternative Rings % Status: Open Problem % % In a strongly right alternative ring R, the "circle" operation is defined % by x o y = x + y - x*y (just as in associative rings). The magma (R,o) is % has 0 as its identity element and also satisfies the Bol identity % ((xoy)oz)oy = xo((yoz)oy). % An element of R is quasi-invertible if it has an inverse in (R,o). % % Problem: Let R be a strongly right alternative ring, and let Q(R) be the % set of all quasi-invertible elements. Is Q(R) a Bol loop? % % It is sufficient to check: Is Q(R) closed under o ? % In fact, if aob = boa = 0 and cod = doc = o, then aoc has a complicated % looking right inverse: (aoc) o ((do((bo(coa))ob))od) = o. % If aoc has a left inverse at all, then it must be this thing, which % explains the form of the denial below. % % The associator is included below since many proofs in nonassociative % rings are easier when it is used. % % One can certainly load up the input with various facts about right % alternative rings, such as Mikheev's identity. % % Below the main input file are special cases in which result is is known. op(450,infix,"o"). formulas(assumptions). % (R,+) abelian group 0 + x = x. -x + x = 0. x + y = y + x. (x + y) + z = x + (y + z). % (R,*) strongly right alternative (x * y) * y = x * (y * y). ((x * y) * z) * y = x * ((y * z) * y). % distributive (x * y) + (x * z) = x * (y + z). (y * x) + (z * x) = (y + z) * x. 0 * x = 0. x * 0 = 0. % associator -(x * (y * z)) + ((x * y) * z) = A(x,y,z). % circle operation x o y = x + (y + (-(x * y))). % a, c in Q(R) with inverses b, d a o b = 0. b o a = 0. c o d = 0. d o c = 0. % goal ((d o ((b o (c o a)) o b)) o d) o (a o c) != 0. end_of_list. %% %% Extra Assumptions %% % left alternative % (x * x) * y = x * (x * y). % (-1,1)-ring % A(x,y,z) + (A(y,z,x) + A(z,x,y)) = 0. % Join of alternative rings and (-1,1)-rings %A(x * y,z,x) + (A(z,x,x * y) + A(x,x * y,z)) = (A(x,y,z) + (A(y,z,x) + A(z,x,y))) * x. %A(x,y,z * x) + (A(y,z * x,x) + A(z * x,x,y)) = x * (A(x,y,z) + (A(y,z,x) + A(z,x,y))). %A(A(x,y,z) + (A(y,z,x) + A(z,x,y)),u,w) = -A(u,A(x,y,z) + (A(y,z,x) + A(z,x,y)),w).