diff options
Diffstat (limited to 'library/algebra')
| -rw-r--r-- | library/algebra/group.tex | 1 | ||||
| -rw-r--r-- | library/algebra/loop.tex | 7 | ||||
| -rw-r--r-- | library/algebra/magma.tex | 100 | ||||
| -rw-r--r-- | library/algebra/quasigroup.tex | 36 | ||||
| -rw-r--r-- | library/algebra/semigroup.tex | 82 |
5 files changed, 226 insertions, 0 deletions
diff --git a/library/algebra/group.tex b/library/algebra/group.tex new file mode 100644 index 0000000..48934bd --- /dev/null +++ b/library/algebra/group.tex @@ -0,0 +1 @@ +\section{Groups} diff --git a/library/algebra/loop.tex b/library/algebra/loop.tex new file mode 100644 index 0000000..338985c --- /dev/null +++ b/library/algebra/loop.tex @@ -0,0 +1,7 @@ +\import{algebra/quasigroup.tex} + +\section{Loops} + +\begin{struct}\label{loop} + A loop $A$ is a quasigroup and a unital magma. +\end{struct} diff --git a/library/algebra/magma.tex b/library/algebra/magma.tex new file mode 100644 index 0000000..6f5ac04 --- /dev/null +++ b/library/algebra/magma.tex @@ -0,0 +1,100 @@ +\import{function.tex} + +\section{Magmas} + +\begin{struct}\label{magma} + A magma $A$ is a onesorted structure equipped with + \begin{enumerate} + \item $\mul$ + \end{enumerate} + such that + \begin{enumerate} + \item\label{magma_welldef} for all $a, b\in \carrier[A]$ we have $\mul[A](a,b)\in \carrier[A]$. + \end{enumerate} +\end{struct} + +\begin{abbreviation}\label{cdot} + $a\cdot b = \mul(a,b)$. +\end{abbreviation} + +\begin{abbreviation}\label{idempotentelement} + $a$ is an idempotent element of $A$ iff + $a\in\carrier[A]$ and + $\mul[A](a,a) = a$. +\end{abbreviation} + + +\begin{definition}\label{idempotents} + $\idempotents{A} = \{a\in\carrier[A]\mid \mul[A](a,a) = a\}$. +\end{definition} + +%\begin{definition}\label{rightinternalorbit} +% $\rightinternalorbit{a}{A} = \{\mul[A](a,a') \mid a'\in\carrier[A]\}$. +%\end{definition} + +\begin{abbreviation}\label{commutes} + $a$ commutes with $b$ iff $a\cdot b = b\cdot a$. +\end{abbreviation} + +\begin{definition}\label{submagma} + $A$ is a submagma of $B$ iff + $A$ is a magma and + $B$ is a magma and + $\carrier[A]\subseteq \carrier[B]$ and + $\mul[A]\subseteq \mul[B]$. +\end{definition} + +\begin{proposition}\label{submagma_transitive} + Suppose $A$ is a submagma of $B$. + Suppose $B$ is a submagma of $C$. + Then $A$ is a submagma of $C$. +\end{proposition} +\begin{proof} + Follows by \cref{submagma,subseteq_transitive}. +\end{proof} + +\begin{struct}\label{unitalmagma} + A unital magma $A$ is a magma equipped with + \begin{enumerate} + \item $\neutral$ + \end{enumerate} + such that + \begin{enumerate} + \item\label{unitalmagma_type} $\neutral[A]\in \carrier[A]$. + \item\label{unitalmagma_right} for all $a\in \carrier[A]$ we have $\mul[A](a,\neutral[A]) = a$. + \item\label{unitalmagma_left} for all $a\in \carrier[A]$ we have $\mul[A](\neutral[A], a) = a$. + \end{enumerate} +\end{struct} + +\begin{proposition}\label{unitalmagma_mul_neutral_neutral} + Let $A$ be a unital magma. + Then $\mul(\neutral,\neutral) = \neutral$. +\end{proposition} + +\begin{proposition}\label{unitalmagma_neutral_unique} + Let $A$ be a unital magma. + Let $e$ be a set such that $e\in A$ and for all $x\in A$ we have $\mul(x, e) = x = \mul(e, x)$. + Then $e = \neutral$. +\end{proposition} +\begin{proof} + Follows by \cref{unitalmagma_type,unitalmagma_left}. +\end{proof} + + + +\begin{definition}[Left orbit]\label{left_orbit} + $\LeftOrb{x}{A} = \{\mul[A](a,x) \mid a\in\carrier[A] \}$. +\end{definition} + +\begin{proposition}\label{eq_left_orbit_witness} + Let $A$ be a magma. + Let $e,f\in\carrier[A]$. + Suppose $\LeftOrb{e}{A} = \LeftOrb{f}{A}$. + Let $x\in\carrier[A]$. + Then there exists $y\in\carrier[A]$ such that $x\cdot e = y\cdot f$. +\end{proposition} +\begin{proof} + We have $x\cdot e\in \LeftOrb{e}{A}$ by \cref{left_orbit}. + Thus $x\cdot e\in\LeftOrb{f}{A}$ by assumption. + Take $y\in\carrier[A]$ such that $x\cdot e = y\cdot f$ by \cref{left_orbit}. +\end{proof} diff --git a/library/algebra/quasigroup.tex b/library/algebra/quasigroup.tex new file mode 100644 index 0000000..747ab03 --- /dev/null +++ b/library/algebra/quasigroup.tex @@ -0,0 +1,36 @@ +\import{algebra/magma.tex} + +\section{Quasigroups} + +\begin{struct}\label{quasigroup} + A quasigroup $A$ is a magma equipped with + \begin{enumerate} + \item $\ldiv$ + \item $\rdiv$ + \end{enumerate} + such that + \begin{enumerate} + \item for all $a, b\in A$ we have $\ldiv (a,b)\in A$. + \item for all $a, b\in A$ we have $\rdiv (a,b)\in A$. + \item for all $a,b \in A$ we have $b = \mul(a,\ldiv (a,b))$. + \item for all $a,b \in A$ we have $b = \ldiv(a,\mul (a,b))$. + \item for all $a,b \in A$ we have $b = \mul(\rdiv (b,a),a)$. + \item for all $a,b \in A$ we have $b = \rdiv(\mul (b,a),a)$. + \end{enumerate} +\end{struct} + +% Cancelling an element on the left. +\begin{lemma}\label{quasigroup_cancel_left} + Let $A$ be a quasigroup. + Let $a,b,c \in A$. + Suppose $\mul(a,b) = \mul(a,c)$. + Then $b = c$. +\end{lemma} + +% Cancelling an element on the right. +\begin{lemma}\label{quasigroup_cancel_right} + Let $A$ be a quasigroup. + Let $a,b,c \in A$. + Suppose $\mul(a,c) = \mul(b,c)$. + Then $a = b$. +\end{lemma} diff --git a/library/algebra/semigroup.tex b/library/algebra/semigroup.tex new file mode 100644 index 0000000..e090a56 --- /dev/null +++ b/library/algebra/semigroup.tex @@ -0,0 +1,82 @@ +\import{algebra/magma.tex} + +\section{Semigroups} + +\begin{struct}\label{semigroup} + A semigroup $A$ is a magma such that + \begin{enumerate} + %\item for all $a, b, c\in \carrier[A]$ we have $\mul[A](a,\mul[A](b,c)) = \mul[A](\mul[A](a,b),c)$. + \item\label{semigroup_assoc} for all $a, b, c$ we have $\mul[A](a,\mul[A](b,c)) = \mul[A](\mul[A](a,b),c)$. + \end{enumerate} +\end{struct} + + + +\section{Regular semigroups} + + +\begin{struct}\label{regularsemigroup} + A regular semigroup $A$ is a semigroup such that + \begin{enumerate} + %\item for all $a\in \carrier[A]$ there exists $b\in\carrier[A]$ such that $\mul[A](a, \mul[A](b, a)) = a$. + \item\label{regularsemigroup_regular} for all $a$ there exists $b\in\carrier[A]$ such that $\mul[A](a, \mul[A](b, a)) = a$. + \end{enumerate} +\end{struct} + + + +\section{Inverse semigroups} + +\begin{struct}\label{inversesemigroup} + An inverse semigroup $A$ is a regular semigroup such that + \begin{enumerate} + \item\label{inversesemigroup_comm} for all $a,b\in\idempotents{A}$ we have $\mul[A](a, b) = \mul[A](b, a)$. + \end{enumerate} +\end{struct} + +\begin{proposition}\label{inversesemigroup_is_semigroup} + Suppose $A$ is an inverse semigroup. + Then $A$ is a semigroup. +\end{proposition} + + +\begin{proposition}\label{inversesemigroup_is_regularsemigroup} + Suppose $A$ is an inverse semigroup. + Then $A$ is a regular semigroup. +\end{proposition} + +\begin{proposition}\label{idempotentelems_eq_iff_orbits_eq} + Let $A$ be an inverse semigroup. + Let $e,f\in\idempotents{A}$. + % TODO use Orbits explicitly? + Suppose for all $x\in\carrier[A]$ there exists $y\in\carrier[A]$ + such that $x\cdot e = y\cdot f$. + Suppose for all $x\in\carrier[A]$ there exists $y\in\carrier[A]$ + such that $x\cdot f = y\cdot e$. + Then $e = f$. +\end{proposition} +\begin{proof} + Take $x, y\in\carrier[A]$ such that $e = x\cdot f$ and $f = y\cdot e$ by \cref{idempotents}. + % + \begin{align*} + e + &= x \cdot f + \explanation{by assumption}\\ + &= x\cdot (f\cdot f) + \explanation{by \cref{idempotents}}\\ + &= (x\cdot f)\cdot f + \explanation{by \cref{semigroup_assoc,inversesemigroup_is_semigroup}}\\ + &= e\cdot f + \explanation{by assumption}\\ + &= f\cdot e + \explanation{by \hyperref[inversesemigroup_comm]{commutativity of idempotent elements}}\\ + &= (y\cdot e)\cdot e + \explanation{by assumption}\\ + &= y\cdot (e\cdot e) + \explanation{by \cref{semigroup_assoc,inversesemigroup_is_semigroup}}\\ + &= y \cdot e + \explanation{by \cref{idempotents}}\\ + &= f + \explanation{by assumption} + \end{align*} +\end{proof} |