Each object is the n-fold monoidal product of the generating object \(1\).
To specify a prop \(P\) it is enough to specify 5 things (and check they satisfy the rules for symmetric monoidal categories):
A set \(\mathcal{C}(m,n))\) of morphisms \(m \rightarrow n\) for \(m,n \in \mathbb{N}\).
For all naturals, an identity map \(n \xrightarrow{id_n} n\)
For all \(m,n \in \mathbb{N}\), a symmetry map \(m+n \xrightarrow{\sigma_{m,n}} n+m\)
A composition rule: given \(m \xrightarrow f n\) and \(n \xrightarrow g p\), a map \(m \xrightarrow{f;g} p\)
A monoidal product on morphisms: given \(m \xrightarrow f m'\) and \(n \xrightarrow g n'\), a map \(m+n \xrightarrow{f+g} m' +n'\)
A prop
A symmetric strict monoidal category \((\mathcal{C}, 0,+)\) for which \(Ob(\mathcal{C})=\mathbb{N}\) and the monoidal product on objects is given by addition.
A \(\ref{Prop|\emph{prop|referenced}}\) functor \(\mathcal{C} \xrightarrow F \mathcal{D}\) A functor for which
\(\forall n \in \mathbb{N}: F(n)=n\)
For all \(m_1 \xrightarrow f m_2\) and \(n_1 \xrightarrow g n_2 \in \mathcal{C}\): \(F(f))+F(g)=F(f+g) \in \mathcal{D}\)
The prop FinSet
Morphisms \(m \xrightarrow f n\) are functions from \(\bar m\) to \(\bar n\).
The identities, symmetries, and composition rule are obvious.
The monoidal product on functions is given by the disjoint union.
The compact closed category \(\ref{Correl as CCC|\textbf{Corel|referenced}}\) is a prop.
There is a prop Rel
Morphisms are relations \(R \subseteq \bar m \times \bar n\)
Composition with \(S \subseteq \bar n \times \bar p\) is
\(\{(i, k)\ |\ \exists (i, j) \in R \land \exists (j,k) \in S\}\)
Monoidal product is given by the coproduct, which amounts to placing the two relations side-by-side.
The inclusion \(\mathbf{Bij} \overset{i}{\hookrightarrow} \mathbf{FinSet}\) is a prop functor.
There is a prop functor \(\mathbf{Bij} \xrightarrow F \mathbf{Rel_{Fin}}\) defined by \(F(\bar{m} \xrightarrow{f} \bar{n}):=\{(i,j)\ |\ f(i)=j\} \in \bar m \times \bar n\)
Draw a morphism \(3 \xrightarrow f 2\) and a morphism \(2 \xrightarrow g 4\) in \(\ref{FinSet as prop|\textbf{FinSet|referenced}}\)
Draw \(f+g\)
What is the natural composition rule for morphisms in \(\ref{FinSet as prop|\textbf{FinSet|referenced}}\)
What are the identities in \(\ref{FinSet as prop|\textbf{FinSet|referenced}}\)
Draw a symmetry map \(\sigma_{m,n}\) for some \(m,n\) in \(\ref{FinSet as prop|\textbf{FinSet|referenced}}\).
TODO
A posetal prop is a prop that is also a poset.
In other words, a symmetric monoidal preorder \((\mathbb{N}, \leq)\) for some posetal relation \(\leq\), where the monoidal product is addition.
Give three examples of a posetal prop.
The normal meaning of \(\leq\) as less than or equal to
The divisibility relation
The opposite of the first example (greater than or equal to).
A port graph
A special type of prop where morphisms are open, directed, acyclic port graphs \((V, in, out, i)\)
\(V\) is a set of vertices
functions \(V \xrightarrow{in, out} \mathbb{N}\) give the in degree and out degree of each vertex
A bijection \(\bar m \sqcup O \xrightarrow{i} I \sqcup \bar n\), where \(I = \{(v,i)\ |\ v \in V, 1 \leq i \leq in(v)\}\) and \(O=\{(v,i)\ |\ v \in V, 1 \leq i \leq out(v))\}\) are the vertex inputs and vertex outputs, respectively.
Furthermore, an acyclicity condition:
Use the bijection \(i\) to construct the internal flow graph: a graph with an arrow \(u \xrightarrow{e^{u,i}_{v,j}} v\) for every \(i,j \in \mathbb{N}\) such that \(i(u,i)=(v,j)\)
This graph must be acyclic
A \((2,3)\) port-graph. [Draw this]
Since the overall type is \((2,3)\) we know we need a box with two overall inputs and three overall outputs.
There are three internal boxes, meaning the vertex set is \(\{a, b, c\}\).
\(in(a)=1\) and \(out(a)=3\) which tells us to draw one port on the LHS and three on the RHS.
The bijection \(i\) tells us how the ports are connected by wires.
The acyclic internal flow graph is shown below [TODO Draw this]
A category PG whose objects are natural numbers and morphisms are port graphs
We can compose a \((m,n)\) port graph with a \((n, p)\) port graph \((V \sqcup V',[in,in'],[out,out'], i'')\)
\(V \sqcup V' \xrightarrow{[in,in']} \mathbb{N}\) maps elements of \(V\) according to \(in\) and elements of \(V'\) according to \(in'\) (likewise for out).
The bijection \(\bar m \sqcup O \sqcup O' \xrightarrow{i''} I \sqcup I' \sqcup \bar p\) is defined as \(i''(x)=\begin{cases}i(x) & i(x) \in I \\ i'(i(x))& i(x) \in \bar n \\ i'(x) & x \in O' \end{cases}\)
The identity port graph on \(n\) is \((\varnothing, !, !, id_{\bar n})\) where \(\varnothing \xrightarrow{!} \mathbb{N}\) is a unique function.
This category is a prop.
The monoidal product of two portgraphs... TODO
Describe how port graph composition looks, with respect to the visual representation of Example 5.14, and give a nontrivial example
Todo