diff options
Diffstat (limited to 'library/algebra')
| -rw-r--r-- | library/algebra/magma.tex | 7 | ||||
| -rw-r--r-- | library/algebra/monoid.tex | 5 | ||||
| -rw-r--r-- | library/algebra/quasigroup.tex | 30 | ||||
| -rw-r--r-- | library/algebra/semigroup.tex | 43 |
4 files changed, 45 insertions, 40 deletions
diff --git a/library/algebra/magma.tex b/library/algebra/magma.tex index d05ce29..3937b56 100644 --- a/library/algebra/magma.tex +++ b/library/algebra/magma.tex @@ -71,10 +71,13 @@ Let $A$ be a unital magma. Then $\mul(\neutral,\neutral) = \neutral$. \end{proposition} +\begin{proof} + Follows by \cref{unitalmagma_type,unitalmagma_left}. +\end{proof} \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)$. + Let $e$ be a set such that $e\in \carrier[A]$ and for all $x\in \carrier[A]$ we have $\mul(x, e) = x = \mul(e, x)$. Then $e = \neutral$. \end{proposition} \begin{proof} @@ -97,5 +100,5 @@ \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}. + Take $y$ such that $y\in\carrier[A]$ and $x\cdot e = y\cdot f$ by \cref{left_orbit}. \end{proof} diff --git a/library/algebra/monoid.tex b/library/algebra/monoid.tex index bef3166..ed9d2ff 100644 --- a/library/algebra/monoid.tex +++ b/library/algebra/monoid.tex @@ -4,10 +4,13 @@ \begin{struct}\label{monoid} A monoid $A$ is a unital magma such that \begin{enumerate} - \item\label{monoid_assoc} for all $a, b, c$ we have $\mul[A](a,\mul[A](b,c)) = \mul[A](\mul[A](a,b),c)$. + \item\label{monoid_assoc} for all $a,b,c\in\carrier[A]$ we have $\mul[A](a,\mul[A](b,c)) = \mul[A](\mul[A](a,b),c)$. \end{enumerate} \end{struct} \begin{corollary}\label{monoid_implies_semigroup} Let $A$ be a monoid. Then $A$ is a semigroup. \end{corollary} +\begin{proof} + Follows by \cref{monoid,unitalmagma,semigroup}. +\end{proof} diff --git a/library/algebra/quasigroup.tex b/library/algebra/quasigroup.tex index 747ab03..50d7b0f 100644 --- a/library/algebra/quasigroup.tex +++ b/library/algebra/quasigroup.tex @@ -10,27 +10,37 @@ \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)$. + \item\label{quasigroup_ldiv_type} for all $a,b\in\carrier[A]$ we have $\ldiv[A](a,b)\in\carrier[A]$. + \item\label{quasigroup_rdiv_type} for all $a,b\in\carrier[A]$ we have $\rdiv[A](a,b)\in\carrier[A]$. + \item\label{quasigroup_mul_ldiv} for all $a,b\in\carrier[A]$ we have $b = \mul[A](a,\ldiv[A](a,b))$. + \item\label{quasigroup_ldiv_mul} for all $a,b\in\carrier[A]$ we have $b = \ldiv[A](a,\mul[A](a,b))$. + \item\label{quasigroup_rdiv_mul} for all $a,b\in\carrier[A]$ we have $b = \mul[A](\rdiv[A](b,a),a)$. + \item\label{quasigroup_mul_rdiv} for all $a,b\in\carrier[A]$ we have $b = \rdiv[A](\mul[A](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)$. + Let $a,b,c\in\carrier[A]$. + Suppose $\mul[A](a,b) = \mul[A](a,c)$. Then $b = c$. \end{lemma} +\begin{proof} + We have $b=\ldiv[A](a,\mul[A](a,b))$ by \cref{quasigroup_ldiv_mul}. + We have $c=\ldiv[A](a,\mul[A](a,c))$ by \cref{quasigroup_ldiv_mul}. + Follows by assumption. +\end{proof} % 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)$. + Let $a,b,c\in\carrier[A]$. + Suppose $\mul[A](a,c) = \mul[A](b,c)$. Then $a = b$. \end{lemma} +\begin{proof} + We have $a=\rdiv[A](\mul[A](a,c),c)$ by \cref{quasigroup_mul_rdiv}. + We have $b=\rdiv[A](\mul[A](b,c),c)$ by \cref{quasigroup_mul_rdiv}. + Follows by assumption. +\end{proof} diff --git a/library/algebra/semigroup.tex b/library/algebra/semigroup.tex index e090a56..be94945 100644 --- a/library/algebra/semigroup.tex +++ b/library/algebra/semigroup.tex @@ -5,8 +5,7 @@ \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)$. + \item\label{semigroup_assoc} for all $a, b, c\in \carrier[A]$ we have $\mul[A](a,\mul[A](b,c)) = \mul[A](\mul[A](a,b),c)$. \end{enumerate} \end{struct} @@ -18,8 +17,7 @@ \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$. + \item\label{regularsemigroup_regular} for all $a\in \carrier[A]$ there exists $b\in\carrier[A]$ such that $\mul[A](a, \mul[A](b, a)) = a$. \end{enumerate} \end{struct} @@ -38,12 +36,18 @@ Suppose $A$ is an inverse semigroup. Then $A$ is a semigroup. \end{proposition} +\begin{proof} + Follows by \cref{inversesemigroup,regularsemigroup}. +\end{proof} \begin{proposition}\label{inversesemigroup_is_regularsemigroup} Suppose $A$ is an inverse semigroup. Then $A$ is a regular semigroup. \end{proposition} +\begin{proof} + Follows by \cref{inversesemigroup}. +\end{proof} \begin{proposition}\label{idempotentelems_eq_iff_orbits_eq} Let $A$ be an inverse semigroup. @@ -56,27 +60,12 @@ 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*} + Take $x,y$ such that $x,y\in\carrier[A]$ and + $e = x\cdot f$ and $f = y\cdot e$ by \cref{idempotents}. + We have $e=e\cdot f$ by + \cref{idempotents,semigroup_assoc,inversesemigroup_is_semigroup}. + We have $f=f\cdot e$ by + \cref{idempotents,semigroup_assoc,inversesemigroup_is_semigroup}. + We have $e\cdot f=f\cdot e$ by \cref{inversesemigroup_comm}. + Follows by assumption. \end{proof} |