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 \(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
\( Has\text{ LeftDiv}(G,A) \equiv \forall a\in G.\ \forall b\in G.\ \exists !x.\ (x\in G \wedge A\langle a,x\rangle = b) \)
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
\( Has\text{ RightDiv}(G,A) \equiv \forall a\in G.\ \forall b\in G.\ \exists !x.\ (x\in G \wedge A\langle x,a\rangle = b) \)
An operation that has both left and right division is said to have the Latin square property.
definition
\( A \text{ has Latin square property on } G \equiv Has\text{ LeftDiv}(G,A) \wedge Has\text{ RightDiv}(G,A) \)
A quasigroup is a set with a binary operation that has the Latin square property.
definition
\( \text{IsAquasigroup}(G,A) \equiv A:G\times G\rightarrow G \wedge A \text{ 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 \(x\cdot z = y\) for given \(\langle x,y \rangle = p \in G\times G\) using the identity \(\bigcup \{x\} =x\).
definition
\( \text{ LeftDiv}(G,A) \equiv \{\langle p,\bigcup \{z\in G.\ A\langle \text{fst}(p),z\rangle = \text{snd}(p)\}\rangle .\ p\in G\times G\} \)
Similarly the right division is defined as a function on \(G\times G\).
definition
\( \text{ RightDiv}(G,A) \equiv \{\langle p,\bigcup \{z\in G.\ A\langle z,\text{fst}(p)\rangle = \text{snd}(p)\}\rangle .\ p\in G\times G\} \)
Left and right divisions are binary operations on \(G\).
lemma lrdiv_binop:
assumes \( \text{IsAquasigroup}(G,A) \)
shows \( \text{ LeftDiv}(G,A):G\times G\rightarrow G \) and \( \text{ RightDiv}(G,A):G\times G\rightarrow G \)proof{
}
fix \( p \)
assume \( p\in G\times G \)
with assms have \( \bigcup \{x\in G.\ A\langle \text{fst}(p),x\rangle = \text{snd}(p)\} \in G \) and \( \bigcup \{x\in G.\ A\langle x,\text{fst}(p)\rangle = \text{snd}(p)\} \in G \) unfolding IsAquasigroup_def, HasLatinSquareProp_def, HasLeftDiv_def, HasRightDiv_def using ZF1_1_L9(2)
then show \( \text{ LeftDiv}(G,A):G\times G\rightarrow G \) and \( \text{ RightDiv}(G,A):G\times G\rightarrow G \) unfolding LeftDiv_def, RightDiv_def using ZF_fun_from_total
qed
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
assumes qgroupassum: \( \text{IsAquasigroup}(G,A) \)
defines \( x\cdot y \equiv A\langle x,y\rangle \)
defines \( x\backslash y \equiv \text{ LeftDiv}(G,A)\langle x,y\rangle \)
defines \( x/ y \equiv \text{ RightDiv}(G,A)\langle y,x\rangle \)
The quasigroup operation is closed on \(G\).
lemma (in quasigroup0) qg_op_closed:
assumes \( x\in G \), \( y\in G \)
shows \( x\cdot y \in G \) using qgroupassum, assms, IsAquasigroup_def, apply_funtypeA couple of properties of right and left division:
lemma (in quasigroup0) lrdiv_props:
assumes \( x\in G \), \( y\in G \)
shows \( \exists !z.\ z\in G \wedge z\cdot x = y \), \( y/ x \in G \), \( (y/ x)\cdot x = y \) and \( \exists !z.\ z\in G \wedge x\cdot z = y \), \( x\backslash y \in G \), \( x\cdot (x\backslash y) = y \)proof let \( z_r = \bigcup \{z\in G.\ z\cdot x = y\} \)
from qgroupassum have I: \( \text{ RightDiv}(G,A):G\times G\rightarrow G \) using lrdiv_binop(2)
with assms have \( \text{ RightDiv}(G,A)\langle x,y\rangle = z_r \) unfolding RightDiv_def using ZF_fun_from_tot_val
moreover
from qgroupassum, assms show \( \exists !z.\ z\in G \wedge z\cdot x = y \) unfolding IsAquasigroup_def, HasLatinSquareProp_def, HasRightDiv_def
then have \( z_r\cdot x = y \) by (rule ZF1_1_L9 )
ultimately show \( (y/ x)\cdot x = y \)
let \( z_l = \bigcup \{z\in G.\ x\cdot z = y\} \)
from qgroupassum have II: \( \text{ LeftDiv}(G,A):G\times G\rightarrow G \) using lrdiv_binop(1)
with assms have \( \text{ LeftDiv}(G,A)\langle x,y\rangle = z_l \) unfolding LeftDiv_def using ZF_fun_from_tot_val
moreover
from qgroupassum, assms show \( \exists !z.\ z\in G \wedge x\cdot z = y \) unfolding IsAquasigroup_def, HasLatinSquareProp_def, HasLeftDiv_def
then have \( x\cdot z_l = y \) by (rule ZF1_1_L9 )
ultimately show \( x\cdot (x\backslash y) = y \)
from assms, I, II show \( y/ x \in G \) and \( x\backslash y \in G \) using apply_funtype
qed
We can cancel the left element on both sides of an equation.
lemma (in quasigroup0) qg_cancel_left:
assumes \( x\in G \), \( y\in G \), \( z\in G \) and \( x\cdot y = x\cdot z \)
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 \( x\in G \), \( y\in G \), \( z\in G \) and \( y\cdot x = z\cdot x \)
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 \( x\in G \), \( y\in G \)
shows \( (y\cdot x)/ x = y \) and \( x\backslash (x\cdot y) = y \)proof from assms have \( (y\cdot x)/ x \in G \) and \( ((y\cdot x)/ x)\cdot x = y\cdot x \) using qg_op_closed, lrdiv_props(2,3)
with assms show \( (y\cdot x)/ x = y \) using qg_cancel_right
from assms have \( x\backslash (x\cdot y) \in G \) and \( x\cdot (x\backslash (x\cdot y)) = x\cdot y \) using qg_op_closed, lrdiv_props(5,6)
with assms show \( x\backslash (x\cdot y) = y \) using qg_cancel_left
qed
end
Definition of IsAquasigroup:
\( \text{IsAquasigroup}(G,A) \equiv A:G\times G\rightarrow G \wedge A \text{ has Latin square property on } G \)
Definition of HasLatinSquareProp:
\( A \text{ has Latin square property on } G \equiv Has\text{ LeftDiv}(G,A) \wedge Has\text{ RightDiv}(G,A) \)
Definition of HasLeftDiv:
\( Has\text{ LeftDiv}(G,A) \equiv \forall a\in G.\ \forall b\in G.\ \exists !x.\ (x\in G \wedge A\langle a,x\rangle = b) \)
Definition of HasRightDiv:
\( Has\text{ RightDiv}(G,A) \equiv \forall a\in G.\ \forall b\in G.\ \exists !x.\ (x\in G \wedge A\langle x,a\rangle = b) \)
lemma ZF1_1_L9:
assumes \( \exists ! x.\ x\in A \wedge \phi (x) \)
shows \( \exists a.\ \{x\in A.\ \phi (x)\} = \{a\} \), \( \bigcup \{x\in A.\ \phi (x)\} \in A \), \( \phi (\bigcup \{x\in A.\ \phi (x)\}) \)Definition of LeftDiv:
\( \text{ LeftDiv}(G,A) \equiv \{\langle p,\bigcup \{z\in G.\ A\langle \text{fst}(p),z\rangle = \text{snd}(p)\}\rangle .\ p\in G\times G\} \)
Definition of RightDiv:
\( \text{ RightDiv}(G,A) \equiv \{\langle p,\bigcup \{z\in G.\ A\langle z,\text{fst}(p)\rangle = \text{snd}(p)\}\rangle .\ p\in G\times G\} \)
lemma ZF_fun_from_total:
assumes \( \forall x\in X.\ b(x) \in Y \)
shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \) lemma lrdiv_binop:
assumes \( \text{IsAquasigroup}(G,A) \)
shows \( \text{ LeftDiv}(G,A):G\times G\rightarrow G \) and \( \text{ RightDiv}(G,A):G\times G\rightarrow G \) lemma ZF_fun_from_tot_val:
assumes \( f:X\rightarrow Y \), \( x\in X \) and \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)
shows \( f(x) = b(x) \) and \( b(x)\in Y \) lemma ZF1_1_L9:
assumes \( \exists ! x.\ x\in A \wedge \phi (x) \)
shows \( \exists a.\ \{x\in A.\ \phi (x)\} = \{a\} \), \( \bigcup \{x\in A.\ \phi (x)\} \in A \), \( \phi (\bigcup \{x\in A.\ \phi (x)\}) \) lemma lrdiv_binop:
assumes \( \text{IsAquasigroup}(G,A) \)
shows \( \text{ LeftDiv}(G,A):G\times G\rightarrow G \) and \( \text{ RightDiv}(G,A):G\times G\rightarrow G \) lemma (in quasigroup0) qg_op_closed:
assumes \( x\in G \), \( y\in G \)
shows \( x\cdot y \in G \) lemma (in quasigroup0) lrdiv_props:
assumes \( x\in G \), \( y\in G \)
shows \( \exists !z.\ z\in G \wedge z\cdot x = y \), \( y/ x \in G \), \( (y/ x)\cdot x = y \) and \( \exists !z.\ z\in G \wedge x\cdot z = y \), \( x\backslash y \in G \), \( x\cdot (x\backslash y) = y \) lemma (in quasigroup0) lrdiv_props:
assumes \( x\in G \), \( y\in G \)
shows \( \exists !z.\ z\in G \wedge z\cdot x = y \), \( y/ x \in G \), \( (y/ x)\cdot x = y \) and \( \exists !z.\ z\in G \wedge x\cdot z = y \), \( x\backslash y \in G \), \( x\cdot (x\backslash y) = y \) lemma (in quasigroup0) lrdiv_props:
assumes \( x\in G \), \( y\in G \)
shows \( \exists !z.\ z\in G \wedge z\cdot x = y \), \( y/ x \in G \), \( (y/ x)\cdot x = y \) and \( \exists !z.\ z\in G \wedge x\cdot z = y \), \( x\backslash y \in G \), \( x\cdot (x\backslash y) = y \) lemma (in quasigroup0) qg_cancel_right:
assumes \( x\in G \), \( y\in G \), \( z\in G \) and \( y\cdot x = z\cdot x \)
shows \( y=z \) lemma (in quasigroup0) lrdiv_props:
assumes \( x\in G \), \( y\in G \)
shows \( \exists !z.\ z\in G \wedge z\cdot x = y \), \( y/ x \in G \), \( (y/ x)\cdot x = y \) and \( \exists !z.\ z\in G \wedge x\cdot z = y \), \( x\backslash y \in G \), \( x\cdot (x\backslash y) = y \) lemma (in quasigroup0) qg_cancel_left:
assumes \( x\in G \), \( y\in G \), \( z\in G \) and \( x\cdot y = x\cdot z \)
shows \( y=z \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8