Theory Quasigroup_ZF
section ‹ Quasigroups ›
theory Quasigroup_ZF imports func1
begin
text‹ 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. ›
subsection‹ Definitions and notation ›
text‹ 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. ›
text‹ A quasigroup operation does not have to have the neutral element. The left division is defined
as the only solution to the equation $a\cdot x=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
"HasLeftDiv(G,A) ≡ ∀a∈G.∀b∈G.∃!x. (x∈G ∧ A`⟨a,x⟩ = b)"
text‹ An operation $A$ has the right inverse if for all elements $a,b \in G$ the equation $x\cdot a=b$
has a unique solution. ›
definition
"HasRightDiv(G,A) ≡ ∀a∈G.∀b∈G.∃!x. (x∈G ∧ A`⟨x,a⟩ = b)"
text‹An operation that has both left and right division is said to have the Latin square property. ›
definition
HasLatinSquareProp (infix "{has Latin square property on}" 65) where
"A {has Latin square property on} G ≡ HasLeftDiv(G,A) ∧ HasRightDiv(G,A)"
text‹ A quasigroup is a set with a binary operation that has the Latin square property. ›
definition
"IsAquasigroup(G,A) ≡ A:G×G→G ∧ A {has Latin square property on} G"
text‹ 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 $x\cdot z = y$ for given
$\langle x,y \rangle = p \in G\times G$ using the identity $\bigcup \{x\} =x$. ›
definition
"LeftDiv(G,A) ≡ {⟨p,⋃{z∈G. A`⟨fst(p),z⟩ = snd(p)}⟩.p∈G×G}"
text‹Similarly the right division is defined as a function on $G\times G$. ›
definition
"RightDiv(G,A) ≡ {⟨p,⋃{z∈G. A`⟨z,fst(p)⟩ = snd(p)}⟩.p∈G×G}"
text‹Left and right divisions are binary operations on $G$. ›
lemma lrdiv_binop: assumes "IsAquasigroup(G,A)" shows
"LeftDiv(G,A):G×G→G" and "RightDiv(G,A):G×G→G"
proof -
{ fix p assume "p∈G×G"
with assms have
"⋃{x∈G. A`⟨fst(p),x⟩ = snd(p)} ∈ G" and "⋃{x∈G. A`⟨x,fst(p)⟩ = snd(p)} ∈ G"
unfolding IsAquasigroup_def HasLatinSquareProp_def HasLeftDiv_def HasRightDiv_def
using ZF1_1_L9(2) by auto
} then show "LeftDiv(G,A):G×G→G" and "RightDiv(G,A):G×G→G"
unfolding LeftDiv_def RightDiv_def using ZF_fun_from_total by auto
qed
text‹ We will use multiplicative notation for the quasigroup operation. The right and left division will
be denoted $a/b$ and $a\backslash b$, resp.›
locale quasigroup0 =
fixes G A
assumes qgroupassum: "IsAquasigroup(G,A)"
fixes qgroper (infixl "⋅" 70)
defines qgroper_def[simp]: "x⋅y ≡ A`⟨x,y⟩"
fixes leftdiv (infixl "\<ld>" 70)
defines leftdiv_def[simp]: "x\<ld>y ≡LeftDiv(G,A)`⟨x,y⟩"
fixes rightdiv (infixl "\<rd>" 70)
defines rightdiv_def[simp]:"x\<rd>y ≡RightDiv(G,A)`⟨y,x⟩"
text‹ The quasigroup operation is closed on $G$. ›
lemma (in quasigroup0) qg_op_closed: assumes "x∈G" "y∈G"
shows "x⋅y ∈ G"
using qgroupassum assms IsAquasigroup_def apply_funtype by auto
text‹ A couple of properties of right and left division: ›
lemma (in quasigroup0) lrdiv_props: assumes "x∈G" "y∈G"
shows
"∃!z. z∈G ∧ z⋅x = y" "y\<rd>x ∈ G" "(y\<rd>x)⋅x = y" and
"∃!z. z∈G ∧ x⋅z = y" "x\<ld>y ∈ G" "x⋅(x\<ld>y) = y"
proof -
let ?z⇩r = "⋃{z∈G. z⋅x = y}"
from qgroupassum have I: "RightDiv(G,A):G×G→G" using lrdiv_binop(2) by simp
with assms have "RightDiv(G,A)`⟨x,y⟩ = ?z⇩r"
unfolding RightDiv_def using ZF_fun_from_tot_val by auto
moreover
from qgroupassum assms show "∃!z. z∈G ∧ z⋅x = y"
unfolding IsAquasigroup_def HasLatinSquareProp_def HasRightDiv_def by simp
then have "?z⇩r⋅x = y" by (rule ZF1_1_L9)
ultimately show "(y\<rd>x)⋅x = y" by simp
let ?z⇩l = "⋃{z∈G. x⋅z = y}"
from qgroupassum have II: "LeftDiv(G,A):G×G→G" using lrdiv_binop(1) by simp
with assms have "LeftDiv(G,A)`⟨x,y⟩ = ?z⇩l"
unfolding LeftDiv_def using ZF_fun_from_tot_val by auto
moreover
from qgroupassum assms show "∃!z. z∈G ∧ x⋅z = y"
unfolding IsAquasigroup_def HasLatinSquareProp_def HasLeftDiv_def by simp
then have "x⋅?z⇩l = y" by (rule ZF1_1_L9)
ultimately show "x⋅(x\<ld>y) = y" by simp
from assms I II show "y\<rd>x ∈ G" and "x\<ld>y ∈ G" using apply_funtype by auto
qed
text‹ We can cancel the left element on both sides of an equation. ›
lemma (in quasigroup0) qg_cancel_left:
assumes "x∈G" "y∈G" "z∈G" and "x⋅y = x⋅z"
shows "y=z"
using qgroupassum assms qg_op_closed lrdiv_props(4) by blast
text‹ We can cancel the right element on both sides of an equation. ›
lemma (in quasigroup0) qg_cancel_right:
assumes "x∈G" "y∈G" "z∈G" and "y⋅x = z⋅x"
shows "y=z"
using qgroupassum assms qg_op_closed lrdiv_props(1) by blast
text‹ Two additional identities for right and left division: ›
lemma (in quasigroup0) lrdiv_ident: assumes "x∈G" "y∈G"
shows "(y⋅x)\<rd>x = y" and "x\<ld>(x⋅y) = y"
proof -
from assms have "(y⋅x)\<rd>x ∈ G" and "((y⋅x)\<rd>x)⋅x = y⋅x"
using qg_op_closed lrdiv_props(2,3) by auto
with assms show "(y⋅x)\<rd>x = y" using qg_cancel_right by simp
from assms have "x\<ld>(x⋅y) ∈ G" and "x⋅(x\<ld>(x⋅y)) = x⋅y"
using qg_op_closed lrdiv_props(5,6) by auto
with assms show "x\<ld>(x⋅y) = y" using qg_cancel_left by simp
qed
end