theory Loop_ZF imports Quasigroup_ZF
begin
This theory specifies the definition and proves basic properites of loops. Loops are very similar to groups, the only property that is missing is associativity of the operation.
Definitions and notation
In this section we define the notions of identity element and left and right inverse.
A loop is a quasigroup with an identity elemen.
definition
\( \text{IsAloop}(G,A) \equiv \text{IsAquasigroup}(G,A) \wedge (\exists e\in G.\ \forall x\in G.\ A\langle e,x\rangle = x \wedge A\langle x,e\rangle = x) \)
The neutral element for a binary operation \(A:G\times G \rightarrow G \) is defined as the only element \(e\) of \(G\) such that \(A\langle x,e\rangle = x\) and \(A\langle e,x\rangle = x\) for all \(x\in G\). Note that although the loop definition guarantees the existence of (some) such element(s) at this point we do not know if this element is unique. We can define this notion h ere but it will become usable only after we prove uniqueness.
definition
\( \text{ TheNeutralElement}(G,f) \equiv \) \( ( \text{The } e.\ e\in G \wedge (\forall g\in G.\ f\langle e,g\rangle = g \wedge f\langle g,e\rangle = g)) \)
We will reuse the notation defined in the quasigroup0 locale, just adding the assumption about the existence of a neutral element and notation for it.
locale loop0 = quasigroup0 +
assumes ex_ident: \( \exists e\in G.\ \forall x\in G.\ e\cdot x = x \wedge x\cdot e = x \)
defines \( 1 \equiv \text{ TheNeutralElement}(G,A) \)
In the loop context the pair \( (G,A) \) forms a loop.
lemma (in loop0) is_loop:
shows \( \text{IsAloop}(G,A) \) unfolding IsAloop_def using ex_ident, qgroupassumIf we know that a pair \( (G,A) \) forms a loop then the assumptions of the loop0 locale hold.
lemma loop_loop0_valid:
assumes \( \text{IsAloop}(G,A) \)
shows \( loop0(G,A) \) using assms unfolding IsAloop_def, loop0_axioms_def, quasigroup0_def, loop0_defThe neutral element is unique in the loop.
lemma (in loop0) neut_uniq_loop:
shows \( \exists !e.\ e\in G \wedge (\forall x\in G.\ e\cdot x = x \wedge x\cdot e = x) \)proof from ex_ident show \( \exists e.\ e \in G \wedge (\forall x\in G.\ e \cdot x = x \wedge x \cdot e = x) \)
next
fix \( e \) \( y \)
assume \( e \in G \wedge (\forall x\in G.\ e \cdot x = x \wedge x \cdot e = x) \), \( y \in G \wedge (\forall x\in G.\ y \cdot x = x \wedge x \cdot y = x) \)
then have \( e\cdot y =y \) and \( e\cdot y = e \)
thus \( e=y \)
qed
The neutral element as defined in the loop0 locale is indeed neutral.
lemma (in loop0) neut_props_loop:
shows \( 1 \in G \) and \( \forall x\in G.\ 1 \cdot x =x \wedge x\cdot 1 = x \)proof let \( n = \text{The } e.\ e\in G \wedge (\forall x\in G.\ e\cdot x = x \wedge x\cdot e = x) \)
have \( 1 = \text{ TheNeutralElement}(G,A) \)
then have \( 1 = n \) unfolding TheNeutralElement_def
moreover
qed
have \( n\in G \wedge (\forall x\in G.\ n\cdot x = x \wedge x\cdot n = x) \) using neut_uniq_loop, theI
ultimately show \( 1 \in G \) and \( \forall x\in G.\ 1 \cdot x = x \wedge x\cdot 1 = x \)
Every element of a loop has unique left and right inverse (which need not be the same). Here we define the left inverse as a function on \(G\).
definition
\( \text{LeftInv}(G,A) \equiv \{\langle x,\bigcup \{y\in G.\ A\langle y,x\rangle = \text{ TheNeutralElement}(G,A)\}\rangle .\ x\in G\} \)
Definition of the right inverse as a function on \(G\):
definition
\( \text{RightInv}(G,A) \equiv \{\langle x,\bigcup \{y\in G.\ A\langle x,y\rangle = \text{ TheNeutralElement}(G,A)\}\rangle .\ x\in G\} \)
In a loop \(G\) right and left inverses are functions on \(G\).
lemma (in loop0) lr_inv_fun:
shows \( \text{LeftInv}(G,A):G\rightarrow G \), \( \text{RightInv}(G,A):G\rightarrow G \) unfolding LeftInv_def, RightInv_def using neut_props_loop, lrdiv_props(1,4), ZF1_1_L9, ZF_fun_from_totalRight and left inverses have desired properties.
lemma (in loop0) lr_inv_props:
assumes \( x\in G \)
shows \( \text{LeftInv}(G,A)(x) \in G \), \( ( \text{LeftInv}(G,A)(x))\cdot x = 1 \), \( \text{RightInv}(G,A)(x) \in G \), \( x\cdot ( \text{RightInv}(G,A)(x)) = 1 \)proof from assms show \( \text{LeftInv}(G,A)(x) \in G \) and \( \text{RightInv}(G,A)(x) \in G \) using lr_inv_fun, apply_funtype
from assms have \( \exists !y.\ y\in G \wedge y\cdot x = 1 \) using neut_props_loop(1), lrdiv_props(1)
then have \( (\bigcup \{y\in G.\ y\cdot x = 1 \})\cdot x = 1 \) by (rule ZF1_1_L9 )
with assms show \( ( \text{LeftInv}(G,A)(x))\cdot x = 1 \) using lr_inv_fun(1), ZF_fun_from_tot_val unfolding LeftInv_def
from assms have \( \exists !y.\ y\in G \wedge x\cdot y = 1 \) using neut_props_loop(1), lrdiv_props(4)
then have \( x\cdot (\bigcup \{y\in G.\ x\cdot y = 1 \}) = 1 \) by (rule ZF1_1_L9 )
with assms show \( x\cdot ( \text{RightInv}(G,A)(x)) = 1 \) using lr_inv_fun(2), ZF_fun_from_tot_val unfolding RightInv_def
qed
end
Definition of IsAloop:
\( \text{IsAloop}(G,A) \equiv \text{IsAquasigroup}(G,A) \wedge (\exists e\in G.\ \forall x\in G.\ A\langle e,x\rangle = x \wedge A\langle x,e\rangle = x) \)
Definition of TheNeutralElement:
\( \text{ TheNeutralElement}(G,f) \equiv \)
\( ( \text{The } e.\ e\in G \wedge (\forall g\in G.\ f\langle e,g\rangle = g \wedge f\langle g,e\rangle = g)) \)
lemma (in loop0) neut_uniq_loop: shows \( \exists !e.\ e\in G \wedge (\forall x\in G.\ e\cdot x = x \wedge x\cdot e = x) \)
Definition of LeftInv:
\( \text{LeftInv}(G,A) \equiv \{\langle x,\bigcup \{y\in G.\ A\langle y,x\rangle = \text{ TheNeutralElement}(G,A)\}\rangle .\ x\in G\} \)
Definition of RightInv:
\( \text{RightInv}(G,A) \equiv \{\langle x,\bigcup \{y\in G.\ A\langle x,y\rangle = \text{ TheNeutralElement}(G,A)\}\rangle .\ x\in G\} \)
lemma (in loop0) neut_props_loop: shows \( 1 \in G \) and \( \forall x\in G.\ 1 \cdot x =x \wedge x\cdot 1 = x \)
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 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 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 (in loop0) lr_inv_fun: shows \( \text{LeftInv}(G,A):G\rightarrow G \), \( \text{RightInv}(G,A):G\rightarrow G \)
lemma (in loop0) neut_props_loop: shows \( 1 \in G \) and \( \forall x\in G.\ 1 \cdot x =x \wedge x\cdot 1 = x \)
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 loop0) lr_inv_fun: shows \( \text{LeftInv}(G,A):G\rightarrow G \), \( \text{RightInv}(G,A):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 (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 loop0) lr_inv_fun: shows \( \text{LeftInv}(G,A):G\rightarrow G \), \( \text{RightInv}(G,A):G\rightarrow G \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8