blob: e70bbaa0e84b51505528ad505a95969d38ec87d3 (
plain)
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
|
Given modules:
\stexexample{
\begin{smodule}{magma}
\symdef{universe}{\comp{\mathcal U}}
\symdef{operation}[args=2,op=\circ]{#1 \comp\circ #2}
\end{smodule}
\begin{smodule}{monoid}
\importmodule{magma}
\symdef{unit}{\comp e}
\end{smodule}
\begin{smodule}{group}
\importmodule{monoid}
\symdef{inverse}[args=1]{{#1}^{\comp{-1}}}
\end{smodule}
}
We can form a module for \emph{rings} by ``cloning''
an instance of |group| (for addition) and |monoid| (for multiplication),
respectively, and ``glueing them together'' to ensure they share the
same universe:
\stexexample{
\begin{smodule}{ring}
\begin{copymodule}{group}{addition}
\renamedecl[name=universe]{universe}{runiverse}
\renamedecl[name=plus]{operation}{rplus}
\renamedecl[name=zero]{unit}{rzero}
\renamedecl[name=uminus]{inverse}{ruminus}
\end{copymodule}
\notation*{rplus}[plus,op=+,prec=60]{#1 \comp+ #2}
%\setnotation{rplus}{plus}
\notation*{rzero}[zero]{\comp0}
%\setnotation{rzero}{zero}
\notation*{ruminus}[uminus,op=-]{\comp- #1}
%\setnotation{ruminus}{uminus}
\begin{copymodule}{monoid}{multiplication}
\assign{universe}{\runiverse}
\renamedecl[name=times]{operation}{rtimes}
\renamedecl[name=one]{unit}{rone}
\end{copymodule}
\notation*{rtimes}[cdot,op=\cdot,prec=50]{#1 \comp\cdot #2}
%\setnotation{rtimes}{cdot}
\notation*{rone}[one]{\comp1}
%\setnotation{rone}{one}
Test: $\rtimes a{\rplus c{\rtimes de}}$
\end{smodule}
}
\textcolor{red}{TODO: explain donotclone}
\stexexample{
\begin{smodule}{int}
\symdef{Integers}{\comp{\mathbb Z}}
\symdef{plus}[args=2,op=+]{#1 \comp+ #2}
\symdef{zero}{\comp0}
\symdef{uminus}[args=1,op=-]{\comp-#1}
\begin{interpretmodule}{group}{intisgroup}
\assign{universe}{\Integers}
\assign{operation}{\plus!}
\assign{unit}{\zero}
\assign{inverse}{\uminus!}
\end{interpretmodule}
\end{smodule}
}
|