diff options
| -rw-r--r-- | Error.txt | 16 | ||||
| -rw-r--r-- | latex/stdlib.tex | 3 | ||||
| -rw-r--r-- | library/algebra/group.tex | 83 | ||||
| -rw-r--r-- | library/algebra/monoid.tex | 19 | ||||
| -rw-r--r-- | library/everything.tex | 3 | ||||
| -rw-r--r-- | library/test.tex | 54 |
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 |