Premonoidal categories and state transformers
The graphical presentation of symmetric premonoidal categories uses extra control
arcs to model control dependencies. This can be seen as a simple form
of state transformer where each graph has one extra incoming arc
and one extra outgoing arc.
Given a strict symmetric monoidal category C with a chosen
object S, the state transformer category of
C, State(C) is given
by:
- Objects are those of C.
- The homset State(C)[X, Y]
is C[X S, Y S].
The identity-on-objects inclusion
C
State(C)
maps f
to f idS.
C
State(C)
is a strict symmetric premonoidal category with premonoidal structure given by:
The state transformer construction is well-known, and is given by
Power and Robinson as one of the canonical examples of a symmetric premonoidal
category. We shall now show that state transformers are canonical
strict symmetric premonoidal categories by showing that for any
strict symmetric premonoidal category C
P
we can find a strict symmetric monoidal category
D
such that:
that is
C
P
is a full sub-strict-symmetric-premonoidal-category of
D
State(D).
The rest of this section shows how to construct
D, and show that it has the
required properties.
Let LGraph(C)
be the subcategory of Graph(V,C)
category of linear flow graphs, that is ones where:
- All nodes are labelled from C.
- Each edge occurs exactly once either as an outgoing edge of the
graph, or an incoming edge of a node.
Note in particular that since we cannot duplicate or discard edges, this
means this category has no diagonal or terminal. In fact, we can
adapt the previous proof to show that
this is the initial strict symmetric monoidal category over
C.
Similarly, let LGraph(C,P)
be the subcategory of Graph(V,C,P)
where:
- All nodes are labelled from C or P.
- Each edge occurs exactly once either as an outgoing edge of the
graph, or an incoming edge of a node.
We can adapt the previous proof to show that
this is the initial strict symmetric premonoidal category over
P
with centre
LGraph(C).
Given two signatures
C and
P with the same sorts,
define Mix(C,P)
to be the signature with:
We then have:
LGraph(C) |
|
LGraph(C,P) |
|
|
|
LGraph(Mix(C,P)) |
|
State(LGraph(Mix(C,P))) |
where the full subcategories are taken by only including objects which
do not include the new sort S.
We can regard a monoidal category
C
as a signature with:
and similarly for premonoidal categories. Any category is trivially
a category over itself, and so we have a unique symmetric premonoidal functor:
[[_]]C : |
LGraph(C) |
|
C |
[[_]]P : |
LGraph(C,P) |
|
P |
such that:
[[
]]C
=
c
[[
]]P
=
d
and so we can define
D
Q
as a pushout in the category of strict symmetric premonoidal categories:
[[_]]C : |
LGraph(C) |
|
C |
|
|
|
|
[[_]]D : |
LGraph(Mix(C,P)) |
|
D |
[[_]]P : |
LGraph(C,P) |
|
P |
|
|
|
|
[[_]]Q : |
State(LGraph(Mix(C,P))) |
|
Q |
Proposition (Full sub-strict-symmetric-premonoidal-category).
C
P
is a full sub-strict-symmetric-premonoidal category of
D
Q.
Proof.
Proposition (Q is State(D)).
Q is isomorphic to
State(D).
Proof.
Thus for any strict symmetric premonoidal category
C
P
we can find an strict symmetric monoidal category
D such that:
Previous |
Next