Formalisation of groups and monoids

The test.tex file was deleted and all formalisations of groups and monoids was moved to the fitting document of the library. Some proof steps of the new formalisation were optimized for proof time

6 files changed, 105 insertions, 73 deletions

diff --git a/Error.txt b/Error.txt
deleted file mode 100644
index 7aa836a..0000000
--- a/Error.txt
+++ /dev/null
@@ -1,16 +0,0 @@
-stack exec zf -- library/test.tex 
-Verification failed: prover found countermodel
-fof(leftinverse_eq_rightinverse,conjecture,fa=fc).
-fof(monoid_right,axiom,![XA]:(monoid(XA)=>![Xa]:(elem(Xa,s__carrier(XA))=>apply(s__mul(XA),pair(Xa,s__neutral(XA)))=Xa))).
-fof(leftinverse_eq_rightinverse1,axiom,apply(s__mul(fG),pair(fa,s__neutral(fG)))=fc).
-fof(leftinverse_eq_rightinverse2,axiom,apply(s__mul(fG),pair(fa,s__neutral(fG)))=apply(s__mul(fG),pair(fc,s__neutral(fG)))).
-fof(leftinverse_eq_rightinverse3,axiom,fc=apply(s__mul(fG),pair(s__neutral(fG),fc))).
-fof(leftinverse_eq_rightinverse4,axiom,fc=apply(s__mul(fG),pair(fc,s__neutral(fG)))).
-fof(leftinverse_eq_rightinverse5,axiom,apply(s__mul(fG),pair(fa,s__neutral(fG)))=apply(s__mul(fG),pair(s__neutral(fG),fc))).
-fof(leftinverse_eq_rightinverse6,axiom,apply(s__mul(fG),pair(apply(s__mul(fG),pair(fa,fb)),fc))=apply(s__mul(fG),pair(fa,apply(s__mul(fG),pair(fb,fc))))).
-fof(leftinverse_eq_rightinverse7,axiom,apply(s__mul(fG),pair(apply(s__mul(fG),pair(fa,fb)),fc))=apply(s__mul(fG),pair(s__neutral(fG),fc))).
-fof(leftinverse_eq_rightinverse8,axiom,apply(s__mul(fG),pair(fa,fb))=s__neutral(fG)).
-fof(leftinverse_eq_rightinverse9,axiom,apply(s__mul(fG),pair(fb,fc))=s__neutral(fG)&elem(fc,s__carrier(fG))).
-fof(leftinverse_eq_rightinverse10,axiom,apply(s__mul(fG),pair(fa,fb))=s__neutral(fG)&elem(fb,s__carrier(fG))).
-fof(leftinverse_eq_rightinverse11,axiom,elem(fa,s__carrier(fG))).
-fof(leftinverse_eq_rightinverse12,axiom,group(fG)).
\ No newline at end of file
diff --git a/latex/stdlib.tex b/latex/stdlib.tex
index 4921363..e545395 100644
--- a/latex/stdlib.tex
+++ b/latex/stdlib.tex
@@ -36,6 +36,8 @@
     \input{../library/cardinal.tex}
     \input{../library/algebra/magma.tex}
     \input{../library/algebra/semigroup.tex}
+    \input{../library/algebra/monoid.tex}
+    \input{../library/algebra/group.tex}
     %\input{../library/algebra/quasigroup.tex}
     %\input{../library/algebra/loop.tex}
     \input{../library/order/order.tex}
@@ -43,5 +45,4 @@
     \input{../library/topology/topological-space.tex}
     \input{../library/topology/basis.tex}
     \input{../library/topology/disconnection.tex}
-    \input{../library/test.tex}
 \end{document}
diff --git a/library/algebra/group.tex b/library/algebra/group.tex
index 48934bd..a79bd2f 100644
--- a/library/algebra/group.tex
+++ b/library/algebra/group.tex
@@ -1 +1,82 @@
-\section{Groups}
+\import{algebra/monoid.tex}
+\section{Group}
+
+\begin{struct}\label{group}
+    A group $G$ is a monoid such that
+    \begin{enumerate}
+        \item\label{group_inverse} for all $g \in \carrier[G]$ there exist $h \in \carrier[G]$ such that $\mul[G](g, h) =\neutral[G]$.
+    \end{enumerate} 
+\end{struct}   
+
+\begin{corollary}\label{group_implies_monoid}
+    Let $G$ be a group. Then $G$ is a monoid.
+\end{corollary}
+
+\begin{abbreviation}\label{cfourdot}
+    $g \cdot h = \mul(g,h)$.
+\end{abbreviation}
+
+\begin{lemma}\label{neutral_is_idempotent}
+    Let $G$ be a group. $\neutral[G]$ is a idempotent element of $G$.
+\end{lemma}
+
+\begin{lemma}\label{group_divison_right}
+    Let $G$ be a group. Let $a,b,c \in G$.
+    Then $a \cdot c = b \cdot c$ iff $a = b$.
+\end{lemma}
+\begin{proof}
+    Take $a,b,c \in G$ such that $a \cdot c = b \cdot c$.
+    There exist $c' \in G$ such that $c \cdot c' = \neutral[G]$.
+    Therefore $a \cdot c = b \cdot c$ iff $(a \cdot c) \cdot c' = (b \cdot c) \cdot c'$.
+    \begin{align*}
+        (a \cdot c) \cdot c'
+            &= a \cdot (c \cdot c')
+                \explanation{by \cref{semigroup_assoc,group_implies_monoid,monoid_implies_semigroup}}\\
+            &= a \cdot \neutral[G]
+                \explanation{by \cref{group_inverse}}\\
+            &= a
+                \explanation{by \cref{group_implies_monoid,monoid_right}}
+    \end{align*}
+    \begin{align*}
+        (b \cdot c) \cdot c'
+            &= b \cdot (c \cdot c')
+                \explanation{by \cref{semigroup_assoc,group_implies_monoid,monoid_implies_semigroup}}\\
+            &= b \cdot \neutral[G]
+                \explanation{by \cref{group_inverse}}\\
+            &= b
+                \explanation{by \cref{group_implies_monoid,monoid_right}}
+    \end{align*}
+    $(a \cdot c) \cdot c' = (b \cdot c) \cdot c'$ iff $a \cdot c = b \cdot c$ by assumption. 
+    $a = b$ iff $a \cdot c = b \cdot c$ by assumption.
+\end{proof}
+
+
+\begin{proposition}\label{leftinverse_eq_rightinverse}
+    Let $G$ be a group and assume $a \in G$.
+    Then there exist $b\in G$ 
+    such that $a \cdot b = \neutral[G]$ and $b \cdot a = \neutral[G]$.
+\end{proposition}
+\begin{proof}
+    There exist $b \in G$ such that $a \cdot b = \neutral[G]$.
+    There exist $c \in G$ such that $b \cdot c = \neutral[G]$.
+    $a \cdot b = \neutral[G]$.
+    $(a \cdot b) \cdot c = (\neutral[G]) \cdot c$.
+    $(a \cdot b) \cdot c = a \cdot (b \cdot c)$.
+    $a \cdot \neutral[G] = \neutral[G] \cdot c$.
+    $c = c \cdot \neutral[G]$.
+    $c = \neutral[G] \cdot c$.
+    $a \cdot \neutral[G] = c \cdot \neutral[G]$.
+    $a \cdot \neutral[G] = c$ by \cref{monoid_right,group_divison_right}.
+    $a = c$ by \cref{monoid_right,group_divison_right,neutral_is_idempotent}.
+    $b \cdot a = b \cdot c$.
+    $b \cdot a = \neutral[G]$.
+\end{proof}
+
+\begin{definition}\label{group_abelian}
+    $G$ is an abelian group iff $G$ is a group and for all $g,h \in G$ $\mul[G](g,h) = \mul[G](h,g)$. 
+\end{definition}
+
+
+\begin{definition}\label{group_automorphism}
+    Let $f$ be a function. $f$ is a group-automorphism iff $G$ is a group and $\dom{f}=G$ and $\ran{f}=G$. 
+\end{definition}
diff --git a/library/algebra/monoid.tex b/library/algebra/monoid.tex
new file mode 100644
index 0000000..06fcb50
--- /dev/null
+++ b/library/algebra/monoid.tex
@@ -0,0 +1,19 @@
+\import{algebra/semigroup.tex}
+\section{Monoid}
+
+\begin{struct}\label{monoid}
+    A monoid $A$ is a semigroup equipped with
+    \begin{enumerate}
+        \item $\neutral$
+    \end{enumerate}
+    such that
+    \begin{enumerate}
+        \item\label{monoid_type} $\neutral[A]\in \carrier[A]$.
+        \item\label{monoid_right} for all $a\in \carrier[A]$ we have $\mul[A](a,\neutral[A]) = a$.
+        \item\label{monoid_left} for all $a\in \carrier[A]$ we have $\mul[A](\neutral[A], a) = a$.
+    \end{enumerate}
+\end{struct}
+
+\begin{corollary}\label{monoid_implies_semigroup}
+    Let $A$ be a monoid. Then $A$ is a semigroup.
+\end{corollary}
\ No newline at end of file
diff --git a/library/everything.tex b/library/everything.tex
index 599bc27..a5166af 100644
--- a/library/everything.tex
+++ b/library/everything.tex
@@ -20,13 +20,14 @@
 \import{cardinal.tex}
 \import{algebra/magma.tex}
 \import{algebra/semigroup.tex}
+\import{algebra/monoid.tex}
+\import{algebra/group.tex}
 \import{order/order.tex}
 %\import{order/semilattice.tex}
 \import{topology/topological-space.tex}
 \import{topology/basis.tex}
 \import{topology/disconnection.tex}
 \import{topology/separation.tex}
-\import{test.tex}
 
 \begin{proposition}\label{trivial}
     $x = x$.
diff --git a/library/test.tex b/library/test.tex
deleted file mode 100644
index d30bbba..0000000
--- a/library/test.tex
+++ /dev/null
@@ -1,54 +0,0 @@
-\import{algebra/semigroup.tex}
-\section{monoid}
-
-\begin{struct}\label{monoid}
-    A monoid $A$ is a semigroup equipped with
-    \begin{enumerate}
-        \item $\neutral$
-    \end{enumerate}
-    such that
-    \begin{enumerate} %muss hier ein enumerate hin
-        \item\label{monoid_type} $\neutral[A]\in \carrier[A]$.
-        \item\label{monoid_right} for all $a\in \carrier[A]$ we have $\mul[A](a,\neutral[A]) = a$.
-        \item\label{monoid_left} for all $a\in \carrier[A]$ we have $\mul[A](\neutral[A], a) = a$.
-    \end{enumerate}
-\end{struct}
-
-
-\section{Group}
-
-\begin{struct}\label{group}
-    A group $A$ is a monoid such that
-    \begin{enumerate}
-        \item\label{group_inverse} for all $a \in \carrier[A]$ there exist $b \in \carrier[A]$ such that $\mul[A](a, b) =\neutral[A]$.
-    \end{enumerate} 
-\end{struct}    
-
-\begin{abbreviation}\label{cfourdot}
-    $a\cdot b = \mul(a,b)$.
-\end{abbreviation}
-
-\begin{lemma}\label{neutral_is_idempotent}
-    Let $G$ be a group. $\neutral[G]$ is a idempotent element of $G$.
-\end{lemma}
-
-\begin{proposition}\label{leftinverse_eq_rightinverse}
-    Let $G$ be a group and assume $a \in G$.
-    Then there exist $b\in G$ 
-    such that $a \cdot b = \neutral[G]$ and $b \cdot a = \neutral[G]$.
-\end{proposition}
-\begin{proof}
-    There exist $b \in G$ such that $a \cdot b = \neutral[G]$.
-    There exist $c \in G$ such that $b \cdot c = \neutral[G]$.
-    $a \cdot b = \neutral[G]$.
-    $(a \cdot b) \cdot c = (\neutral[G]) \cdot c$.
-    $(a \cdot b) \cdot c = a \cdot (b \cdot c)$.
-    $a \cdot \neutral[G] = \neutral[G] \cdot c$.
-    $c = c \cdot \neutral[G]$.
-    $c = \neutral[G] \cdot c$.
-    $a \cdot \neutral[G] = c \cdot \neutral[G]$.
-    $a \cdot \neutral[G] = c$ by \cref{monoid_right}.
-    $a = c$ by \cref{monoid_right}.
-    $b \cdot a = b \cdot c$.
-    $b \cdot a = \neutral[G]$.
-\end{proof}
\ No newline at end of file