PRELIMINARY DRAFT
Kelly does this in an extremely precise and careful way, so it seems best to quote him fairly exactly on this.
$\newcommand\calJ{{\mathcal J}} \newcommand\calT{{\mathcal T}}$
Actually, what we give is a considerable simplification of what Kelly gives in AAC Section 3.1 (the parenthesized numbers of the form (m.n) are references to that document):
(1) It is only for single-sorted theories, not multi-sorted theories.
(2) It only describes algebraic theories that can describe structures borne by sets, not the more complex theories needed to describe structures borne by categories.
(3) It does not allow for permutation of variables.
Starting from
(a graded set $\boxed{\leftcat\calB}$ of names of the basic generating operations), Kelly describes
(the free discrete club $\boxed\calT$ that it generates), (a monoid in the monoidal (under the wreath product $\circ$) category of graded sets).
(The objects of $\calT$) and (their augmentations) are defined inductively by:
(3.2) There is an element $\boxed\bfone$ (boldface 1) in $\calT$ of arity ${\bfone}\Gamma = 1 \in \N$.
$\bfone$ is (the element in the theory $\calT$)
which will be interpreted in (a model) as (the identity arrow (unary operation) for the model).
With $\bfone$ we can define the unit for the monoid $\calT$, $\boxed{ \leftadj\eta : \calJ \mathrel{\leftadj\to} \calT : 1 \mathrel{\leftadj\mapsto} \bfone }$.
(3.3) If ($\leftcat{B \in \calB}$) and ($T_1,\ldots,T_{\leftcat B \Gamma} \in \calT$),
then there is an object (i.e. element) $\boxed{ \leftcat B \{T_1,\ldots,T_{\leftcat B\Gamma}\} } \in \calT$ wlth domain-type $(\leftcat B\Gamma)(T_1\Gamma,\ldots, T_{\leftcat B\Gamma}\Gamma) = T_1\Gamma + \cdots + T_{\leftcat B\Gamma}\Gamma$.
EXAMPLE
For a concrete, familiar example of this, consider $\leftcat{\calB = \{0,s\}}$, the names of the classic Peano successor algebra operators.
Then $\calT$ and (its interpretation in the classic model in $\Set$, on $\N$) are:
\[ \boxed{ \begin{array}{l|llll| llll} & & \kern3em \leftcat\calT &&& {} \rlap{\kern3em \rightcat{ \text{interpretation in } \N }} &&& \kern0em \\ \hline \text{arity } 0 & \leftcat{ 0\{\} }, & \leftcat{ s\{0\{\}\} }, & \leftcat{ s\{s\{0\{\}\} }, & \leftcat \dots & \rightcat 0, & \rightcat{s0}, & \rightcat{ s^2 0}, & \rightcat \dots \\ \text{arity } 1 & \leftcat \bfone, & \leftcat{ s\{\bfone\} }, & \leftcat{ s\{s\{\bfone\}\} }, & \leftcat \ldots & \rightcat { 1_\N = \text{id}_\N }, & \rightcat { s:\N\to\N }, & \rightcat{ s^2 }, & \rightcat \ldots \end{array} } \]
Using (3.2) and (3.3) we can define an embedding $\boxed{ \leftcat\calB \mathrel{\leftadj \hookrightarrow} \calT : \leftcat B \mathrel{\leftadj\mapsto} \leftcat B\{\bfone,\dots,\bfone\} }$.
We define the composition (or substitution) operation on $\calT$
\[ \boxed{ \begin{array}{} \calT \circ \calT & \xrightarrow[\kern3em]{\textstyle \mu } & \calT \\ T\leftcat[S_1,\dots,S_{T\Gamma}\leftcat] & \mapsto & T\rightcat(S_1,\dots,S_{T\Gamma}\rightcat) \end{array} } \]
inductively by setting
(3.4) $\bfone \leftcat[S\leftcat] \mapsto \bfone \rightcat(S\rightcat) = S$,
(3.5) $\begin{equation} \big(\leftcat B\{T_1,\ldots,T_{\leftcat B \Gamma}\}\big)\leftcat[S_1,\ldots,S_m\leftcat] \mapsto \\ \big(\leftcat B \{T_1,\ldots,T_{\leftcat B\Gamma}\}\big) \rightcat(S_1,\ldots,S_m\rightcat) = \leftcat B \big\{T_1\rightcat(S_1,\ldots,S_{m_1}\rightcat),\ldots,T_{\leftcat B \Gamma}\rightcat( \ldots,S_m\rightcat)\big\} \end{equation}$,
where $m_i = T_i\Gamma$ and $m$ is the sum of these.
We identify $\leftcat{B \in \calB}$ with $\leftcat B \{\bfone,\ldots,\bfone\} \in \calT$.
Then $\leftcat B \{T_1,\ldots,T_{\leftcat B \Gamma}\}$ coincides with $\leftcat B \rightcat(T_1,\ldots,T_{\leftcat B \Gamma}\rightcat)$ by (3.4) and (3.5):
\[ \leftcat B \rightcat(T_1,\ldots,T_{\leftcat B \Gamma}\rightcat) \xlongequal{\leftcat\calB \hookrightarrow\calT} \big(\leftcat B \{\bfone,\ldots,\bfone\}\big)\rightcat(T_1,\dots,T_{\leftcat B \Gamma}\rightcat) \xlongequal[\text{(3.5)}]{\mu} \leftcat B \big\{\bfone\rightcat(T_1\rightcat),\dots,\bfone\rightcat(T_{\leftcat B \Gamma}\rightcat)\big\} \xlongequal[\text{(3.4)}]{\mu} \leftcat B \{T_1,\dots,T_{\leftcat B \Gamma}\} \; , \]
and we can now drop (the curly-bracket notation) in favor of (round brackets).
To see how (Kelly's various definitions) play together in (a simple and familiar case),
let us apply them to (the $\leftcat{ \calB = \{0,s\} }$ example above):
Identify ($\leftcat{ 0,s \in \calB }$) with ($\leftcat 0 \{\}, \leftcat s \{\bfone\} \in \calT$).
Then we have:
\[ \begin{array}{} \calT \circ \calT & \xrightarrow[\kern3em]{\textstyle \mu } & && \calT \\ \leftcat s \leftcat[0\leftcat] & \mapsto & \leftcat s \rightcat(0\rightcat) &&&& \leftcat s \{0\} \\ \llap{\leftcat\calB \hookrightarrow\calT} \Vert & \mapsto & \llap{\calB\hookrightarrow\calT} \Vert &&&& \Vert \rlap{\leftcat\calB \hookrightarrow\calT} \\ \big(\leftcat s \{\bfone\}\big) \leftcat{\big[}0\{\}\leftcat{\big]} & \mapsto & \big(\leftcat s \{\bfone\}\big)\rightcat{\big(}0\{\}\rightcat{\big)} & \xlongequal[\text{(3.5)}]{\mu} & \leftcat s \Big\{\bfone\rightcat{\big(}0\{\}\rightcat{\big)}\Big\} & \xlongequal[\text{(3.4)}]{\mu} & \leftcat s \big\{0\{\}\big\} \end{array} \]
Thus together we have a cospan (AKA opspan) in $(\Set\downarrow\N)$:
\[ \boxed{ \begin{array}{} && 1 & \mapsto & \bfone \\ &&&& B\{\bfone,\ldots,\bfone\} & \leftarrow \kern-.2em\shortmid & B \\ \hline \leftadj\eta & : & \leftcat\calJ & \mathrel{\leftadj\to} & \calT & \leftadj\hookleftarrow & \leftcat\calB \\ &&& \llap{ |\bfone|_\calA = \ulcorner 1_{\calA} \urcorner } \searrow & \Bigg\downarrow \rlap{|\,|_\calA} & \swarrow \\ &&&& \{\calA,\calA\} \ \end{array} } \]
No comments:
Post a Comment