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.tex3
-rw-r--r--library/test.tex54
4 files changed, 103 insertions, 56 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 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