1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
|
\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}
\begin{definition}\label{trivial_group}
$G$ is the trivial group iff $G$ is a group and $\{\neutral[G]\}=G$.
\end{definition}
\begin{theorem}\label{trivial_implies_abelian}
Let $G$ be a group.
Suppose $G$ is the trivial group.
Then $G$ is an abelian group.
\end{theorem}
|
