summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/stex/doc/packages/features.tex
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}
}