Loading [MathJax]/extensions/TeX/HTML.js

Monday, February 22, 2021

How Kelly builds clubs from generators

PRELIMINARY DRAFT

Kelly does this in an extremely precise and careful way, so it seems best to quote him fairly exactly on this.
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

MathJax 2.7.9