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
93
94
95
96
97
98
99
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}
|
