IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Quasigroup_ZF imports func1
begin

A quasigroup is an algebraic structure that that one gets after adding (sort of) divsibility to magma. Quasigroups differ from groups in that they are not necessarily associative and they do not have to have the neutral element.

Definitions and notation

According to Wikipedia there are at least two approaches to defining a quasigroup. One defines a quasigroup as a set with a binary operation, and the other, from universal algebra, defines a quasigroup as having three primitive operations. We will use the first approach.

A quasigroup operation does not have to have the neutral element. The left division is defined as the only solution to the equation ax=b (using multiplicative notation). The next definition specifies what does it mean that an operation A has a left division on a set G.

definition

Has LeftDiv(G,A)aG. bG. !x. (xGAa,x=b)

An operation A has the right division if for all elements a,bG the equation xa=b has a unique solution.

definition

Has RightDiv(G,A)aG. bG. !x. (xGAx,a=b)

An operation that has both left and right division is said to have the Latin square property.

definition

A has Latin square property on GHas LeftDiv(G,A)Has RightDiv(G,A)

A quasigroup is a set with a binary operation that has the Latin square property.

definition

IsAquasigroup(G,A)A:G×GGA has Latin square property on G

The uniqueness of the left inverse allows us to define the left division as a function. The union expression as the value of the function extracts the only element of the set of solutions of the equation xz=y for given x,y=pG×G using the identity {x}=x.

definition

 LeftDiv(G,A){p,{zG. Afst(p),z=snd(p)}. pG×G}

Similarly the right division is defined as a function on G×G.

definition

 RightDiv(G,A){p,{zG. Az,fst(p)=snd(p)}. pG×G}

Left and right divisions are binary operations on G.

lemma lrdiv_binop:

assumes IsAquasigroup(G,A)

shows  LeftDiv(G,A):G×GG and  RightDiv(G,A):G×GGproof

We will use multiplicative notation for the quasigroup operation. The right and left division will be denoted a/b and ab, resp.

locale quasigroup0

assumes qgroupassum: IsAquasigroup(G,A)

defines xyAx,y

defines xy LeftDiv(G,A)x,y

defines x/y RightDiv(G,A)y,x

The quasigroup operation is closed on G.

lemma (in quasigroup0) qg_op_closed:

assumes xG, yG

shows xyG using qgroupassum, assms, IsAquasigroup_def, apply_funtype

A couple of properties of right and left division:

lemma (in quasigroup0) lrdiv_props:

assumes xG, yG

shows !z. zGzx=y, y/xG, (y/x)x=y and !z. zGxz=y, xyG, x(xy)=yproof

We can cancel the left element on both sides of an equation.

lemma (in quasigroup0) qg_cancel_left:

assumes xG, yG, zG and xy=xz

shows y=z using qgroupassum, assms, qg_op_closed, lrdiv_props(4)

We can cancel the right element on both sides of an equation.

lemma (in quasigroup0) qg_cancel_right:

assumes xG, yG, zG and yx=zx

shows y=z using qgroupassum, assms, qg_op_closed, lrdiv_props(1)

Two additional identities for right and left division:

lemma (in quasigroup0) lrdiv_ident:

assumes xG, yG

shows (yx)/x=y and x(xy)=yproof
end