The Structure of Left Cheban Loops

Abstract: One natural way to study nonassociative loops is to consider those satisfying identities generalizing associativity. For example, the most well-known class are Moufang loops, which can be defined as those satisfying the identity $(xy)(zx)=x((yz)x)$ or other equivalent identities. In 1976 and 1980, A.M. Cheban studied 19 identities of a certain prescribed type. Among these were $x((xy)z) = (yx)(xz)$, $(z(yx))x = (zx)(xy)$, and $x((xy)z) = (y(zx))x$. These are now known as the left Cheban, right Cheban, and Cheban identities, respectively. Cheban gave some examples and showed that a loop satisfies the first two identities if and only if it satisfies the third. There matters stood until 2010 when J.D. Phillips and V. Shcherbacov published a short paper examining the structure of Cheban loops, with all proofs given by the automated theorem prover Prover9. By a mix of human and automated reasoning, Ale\v{s} Dr\'{a}pal and I have studied left Cheban loops in detail and now have a good understanding of their structure. In this talk I will describe that structure. Since an audience member outside of loop theory (and many within loop theory!) will probably not care very much, I will also use the opportunity to talk about how much responsibility we do or do not have to ``humanize'' proofs generated by automated theorem provers.

quantum algebrarings and algebras

Audience: researchers in the topic

European Non-Associative Algebra Seminar