IsarMathLib 1.19.0: Loops

This release adds a theory file about loops. Loops (the kind we talk about here, not to be confused with for example loop algebras) are algebraic structures that are almost like groups, except that we don’t require the operation to be associative. Wikipedia has a nice picture illustrating dependencies between various algebraic structures between magmas and groups which I copy below:

As the picture shows we get a loop when we take a quasigroup and require that an identity (a neutral element of the operation) exists. It can be shown that that identity is unique in the loop. If we denote the loop identity as e, then we can define the left and right inverses of a loop element a as the only solutions to the equations x\cdot a = e and a\cdot x = e. In a loop these inverses do not have to be the same in general. If the loop operation is associative then we get a group and the left and right inverses unify to become the group inverse.


Tags: ,

One Response to “IsarMathLib 1.19.0: Loops”

  1. IsarMathLib 1.20.0: Ordered loops and loop valued metrics | Formalized Mathematics Says:

    […] Just another weblog « IsarMathLib 1.19.0: Loops […]

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.

%d bloggers like this: