Theory Loop_ZF
section ‹ Loops ›
theory Loop_ZF imports Quasigroup_ZF
begin
text‹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.›
subsection‹ Definitions and notation ›
text‹ In this section we define the notions of identity element and left and right inverse. ›
text‹ A loop is a quasigroup with an identity elemen. ›
definition "IsAloop(G,A) ≡ IsAquasigroup(G,A) ∧ (∃e∈G. ∀x∈G. A`⟨e,x⟩ = x ∧ A`⟨x,e⟩ = x)"
text‹ 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
"TheNeutralElement(G,f) ≡
( THE e. e∈G ∧ (∀ g∈G. f`⟨e,g⟩ = g ∧ f`⟨g,e⟩ = g))"
text‹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: "∃e∈G. ∀x∈G. e⋅x = x ∧ x⋅e = x"
fixes neut ("𝟭")
defines neut_def[simp]: "𝟭 ≡ TheNeutralElement(G,A)"
text‹ In the loop context the pair ‹(G,A)› forms a loop. ›
lemma (in loop0) is_loop: shows "IsAloop(G,A)"
unfolding IsAloop_def using ex_ident qgroupassum by simp
text‹If we know that a pair ‹(G,A)› forms a loop then the assumptions of the ‹loop0› locale hold. ›
lemma loop_loop0_valid: assumes "IsAloop(G,A)" shows "loop0(G,A)"
using assms unfolding IsAloop_def loop0_axioms_def quasigroup0_def loop0_def
by auto
text‹The neutral element is unique in the loop. ›
lemma (in loop0) neut_uniq_loop: shows
"∃!e. e∈G ∧ (∀x∈G. e⋅x = x ∧ x⋅e = x)"
proof
from ex_ident show "∃e. e ∈ G ∧ (∀x∈G. e ⋅ x = x ∧ x ⋅ e = x)" by auto
next
fix e y
assume "e ∈ G ∧ (∀x∈G. e ⋅ x = x ∧ x ⋅ e = x)" "y ∈ G ∧ (∀x∈G. y ⋅ x = x ∧ x ⋅ y = x)"
then have "e⋅y =y" and "e⋅y = e" by auto
thus "e=y" by simp
qed
text‹ The neutral element as defined in the ‹loop0› locale is indeed neutral. ›
lemma (in loop0) neut_props_loop: shows "𝟭∈G" and "∀x∈G. 𝟭⋅x =x ∧ x⋅𝟭 = x"
proof -
let ?n = "THE e. e∈G ∧ (∀x∈G. e⋅x = x ∧ x⋅e = x)"
have "𝟭 = TheNeutralElement(G,A)" by simp
then have "𝟭 = ?n" unfolding TheNeutralElement_def by simp
moreover have "?n∈G ∧ (∀x∈G. ?n⋅x = x ∧ x⋅?n = x)" using neut_uniq_loop theI
by simp
ultimately show "𝟭∈G" and "∀x∈G. 𝟭⋅x = x ∧ x⋅𝟭 = x"
by auto
qed
text‹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
"LeftInv(G,A) ≡ {⟨x,⋃{y∈G. A`⟨y,x⟩ = TheNeutralElement(G,A)}⟩. x∈G}"
text‹Definition of the right inverse as a function on $G$: ›
definition
"RightInv(G,A) ≡ {⟨x,⋃{y∈G. A`⟨x,y⟩ = TheNeutralElement(G,A)}⟩. x∈G}"
text‹In a loop $G$ right and left inverses are functions on $G$. ›
lemma (in loop0) lr_inv_fun: shows "LeftInv(G,A):G→G" "RightInv(G,A):G→G"
unfolding LeftInv_def RightInv_def
using neut_props_loop lrdiv_props(1,4) ZF1_1_L9 ZF_fun_from_total
by auto
text‹Right and left inverses have desired properties.›
lemma (in loop0) lr_inv_props: assumes "x∈G"
shows
"LeftInv(G,A)`(x) ∈ G" "(LeftInv(G,A)`(x))⋅x = 𝟭"
"RightInv(G,A)`(x) ∈ G" "x⋅(RightInv(G,A)`(x)) = 𝟭"
proof -
from assms show "LeftInv(G,A)`(x) ∈ G" and "RightInv(G,A)`(x) ∈ G"
using lr_inv_fun apply_funtype by auto
from assms have "∃!y. y∈G ∧ y⋅x = 𝟭"
using neut_props_loop(1) lrdiv_props(1) by simp
then have "(⋃{y∈G. y⋅x = 𝟭})⋅x = 𝟭"
by (rule ZF1_1_L9)
with assms show "(LeftInv(G,A)`(x))⋅x = 𝟭"
using lr_inv_fun(1) ZF_fun_from_tot_val unfolding LeftInv_def by simp
from assms have "∃!y. y∈G ∧ x⋅y = 𝟭"
using neut_props_loop(1) lrdiv_props(4) by simp
then have "x⋅(⋃{y∈G. x⋅y = 𝟭}) = 𝟭"
by (rule ZF1_1_L9)
with assms show "x⋅(RightInv(G,A)`(x)) = 𝟭"
using lr_inv_fun(2) ZF_fun_from_tot_val unfolding RightInv_def by simp
qed
end