summaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/algebra/group.tex83
-rw-r--r--library/algebra/monoid.tex19
-rw-r--r--library/everything.tex2
3 files changed, 103 insertions, 1 deletions
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 9b85f83..a5166af 100644
--- a/library/everything.tex
+++ b/library/everything.tex
@@ -20,6 +20,8 @@
\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}