(* This file is a part of IsarMathLib - a library of formalized mathematics written for Isabelle/Isar. Copyright (C) 2021 Slawomir Kolodynski This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) 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