Merge branch 'main' into main

1 files changed, 82 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}