Todd Trimble digraph stuff

Contents

Introduction

The following is written at the request of Victor Porton, and is an extremely nuts-and-bolts description of the cartesian closed structure of the category $\mathbf{Dig}$, whose objects are sets $V$ equipped with a binary relation $E \subseteq V \times V$ and whose morphisms $V \to W$ preserve the assigned relations.

From a high-level point of view, $\mathbf{Dig}$ is equivalent to the category of $\neg\neg$-separated presheaves on the presheaf topos $\mathbf{Gph}$ of directed graphs. It is well-known that the (full) inclusion of separated presheaves (for a topology on a presheaf category) has a left adjoint that preserves finite products, and it follows that the separated presheaves forms an exponential ideal within the ambient presheaf topos, and thus in particular is cartesian closed. (Indeed, much more is true: not only is the category of separated presheaves cartesian closed, it is a quasitopos, hence it is locally cartesian closed as well.) As a special case, the cartesian closed structure of $\mathbf{Dig}$ is inherited from the cartesian closed structure of the ambient category $\mathbf{Gph}$.

Our plan is to descend from the general to the particular. First we give a general description of the cartesian closed structure on presheaf categories, but in very elementary nuts-and-bolts fashion. (That is, we bypass the more conceptual descriptions involving presheaves as colimits of representable functors, the Yoneda lemma, etc. – in other words, we just unwind the definitions, which is straightforward but less than enlightening.) Then we apply this directly to the special case $\mathbf{Gph}$. Then, we specialize further to the subcategory $\mathbf{Dig}$ and examine the cartesian closed structure directly in this case.

Possibly all this will eventually be extended to “funcoids” and “reloids”.

The cartesian closed category of directed graphs

First we describe the exponential or internal hom in the cartesian closed category of directed graphs $(E, V, s: E \to V, t: E \to V)$.

Consider the category $C$ with objects and non-identity morphisms as follows:

The category of directed graphs is equivalent to the category of presheaves $F: C^{op} \to Set$. Given $F$, the set of vertices is $V = F(0)$, the set of edges is $E = F(1)$, the source function is $s = F(a): F(1) \to F(0)$, and the target function is $t = F(b): F(1) \to F(0)$.

Cartesian closed structure on presheaf toposes

Consider any small category $C$. If $F, G: C^{op} \to Set$ are presheaves on $C$, their exponential $G^F$ is (by abstract nonsense) given by the formula

where for an object $U$ of $C$, we let $C(-, U)$ denote the hom-functor $\hom_C(-, U): C^{op} \to Set$, and $Nat$ a set of natural transformations. (Note: if $\alpha: X \to Y$ is a natural transformation, we denote its component at an object $U$ by $\alpha (U)$.) Given a morphism $f: V \to U$ of $C$, the map $G^F(f): G^F(U) \to G^F(V)$ takes a natural transformation $\alpha: C(-, U) \times F \to G$ to the composite transformation

The evaluation transformation $\epsilon_{F, G}: G^F \times F \to G$ is the one whose component at an object $U$ is the map $G^F(U) \times F(U) \to G(U)$ which takes a pair $(\alpha: C(-, U) \times F \to G, x \in F(U))$ to the element $\alpha(U)(1_U, x) \in G(U)$.

Suppose given a natural transformation $\theta: H \times F \to G$. We define the exponential transpose $\tilde{\theta}: H \to G^F$ to be the transformation whose component at $U$ is the map that takes an element $y \in H(U)$ to the transformation $\tilde{\theta}\cdot y: C(-, U) \times F \to G$ whose component at an object $V$ is defined to be the function

that sends a pair $(f: V \to U, x \in F(V))$ to $\theta (V)(H(f)(y), x)$.

These definitions specify the cartesian closed structure of the presheaf category. The cartesian closure means that the function

(natural in $H, F, G$) is inverse to the function $Nat(H, G^F) \to Nat(H \times F, G)$ that maps a transformation $\eta: H \to G^F$ to the composite

The verification that these two functions are mutually inverse is given in the proofs of the following two propositions.

Cartesian closed structure on directed graphs

Now we consider apply the previous section to the special case $C = 0 \stackrel{\overset{a}{\to}}{\underset{b}{\to}} 1$, where the presheaves may be identified with directed graphs.

Taking $U = 0$, and letting $F, G: C^{op} \to Set$ be directed graphs, the set of vertices $G^F(0)$ is the set of natural transformations

where we note that $C(1, 0)$ is empty and $C(0, 0)$ is a singleton, and so this set is naturally identified with the set of functions

between the sets of vertices of $F$ and $G$.

The set of edges $G^F(1)$ is the set of natural transformations

Here $C(1, 1)$ is a singleton and $C(0, 1) = \{a, b\}$, so the data of an edge of $G^F$ amounts to a pair of functions

or if you like, a triple of functions $e_1, e_{0, a}, e_{0, b}$, subject to a naturality condition that amounts to asserting commutativity of the diagrams

It is straightforward to check (following the definitions of the preceding section) that the source of an edge $(e_1, e_{0, a}, e_{0, b})$ of $G^F$ is the vertex $e_{0, a}: F(0) \to G(0)$ of $G^F$, and that the target of $(e_1, e_{0, a}, e_{0, b})$ is the vertex $e_{0, b}: F(0) \to G(0)$.

The evaluation map $G^F \times F \to G$ consists of a vertex function $G^F(0) \times F(0) \to G(0)$ and an edge function $G^F(1) \times F(1) \to G(1)$. The vertex function is, according to the above, a function $G(0)^{F(0)} \times F(0) \to G(0)$ and is just ordinary evaluation, mapping a pair $(f: F(0) \to G(0), x \in F(0))$ to $f(x) \in G(0)$. The edge function maps a pair $((e_1, e_{0, a}, e_{0, b}) \in G^F(1); e \in F(1))$ to $e_1(e) \in G(1)$.

Given a map $\theta: H \times F \to G$ of directed graphs, consisting of a vertex map $\theta(0): H(0) \times F(0) \to G(0)$ and an edge map $\theta(1): H(1) \times F(1) \to G(1)$, the exponential transpose $\tilde{\theta}$ is described as follows. The vertex map $\tilde{\theta}(0): H(0) \to G^F(0)$ is just the exponential transpose $\widetilde{\theta(0)}: H(0) \to G(0)^{F(0)}$ in the category of sets, taking an vertex $v \in H(0)$ to $\theta(0)(v, -): F(0) \to G(0)$. The edge map $\tilde{\theta}(1): H(1) \to G^F(1)$ takes an edge $e \in H(1)$ to a triple

where, letting $s(e)$ and $t(e)$ be the source and target of $e$, we take $e_1 \coloneqq \theta(1)(e, -)$ and $e_{0, a} \coloneqq \theta(0)(s(e), -)$ and $e_{0, b} \coloneqq \theta(0)(t(e), -)$.

All of these constructions are just special cases of the general considerations in the previous section, and so these constructions indeed define the cartesian closed structure on the category of directed graphs.

Cartesian closed structure on $\mathbf{Dig}$

Now we specialize even further to the case where we consider only directed graphs $(V, E, i: E \to V \times V)$ where $i$ is a monomorphism or injective function. The full subcategory consisting of such graphs and graph morphisms between them is equivalent to $\mathbf{Dig}$, the category of sets $V$ equipped with an endorelation $E$. (Briefly, any such directed graph is isomorphic to one where we take $i$ to be a subset inclusion $E \subseteq V \times V$, just by replacing a monomorphism by its image.)

In this case, we may verify directly that if $F = (V, E, i)$ and $G = (V', E', i')$ are directed graphs for which the source-target pairings $i$, $i'$ are injective, then the source-target pairing for $G^F$, mapping a triple $(e_1, e_{0, a}, e_{0, b})$ to the pair $(e_{0, a}, e_{0, b})$, is also injective. In other words, given $(e_{0, a}, e_{0, b})$ there is at most one function $e_1: F(1) \to G(1)$ for which

But this is clear: injectivity of $i' = \langle s_G, t_G \rangle: G(1) \to G(0) \times G(0)$ means there is at most $e_1$ such that

This shows that $\mathbf{Dig}$ is closed with respect to the cartesian closed structure on $Gph$.

Recasting all this in the language of sets equipped with endorelations: if $(X, \sim_X)$ and $(Y, \sim_Y)$ are such structures, then their internal hom is the set $Y^X$ of functions $f: X \to Y$, where there is an edge or relation $f \sim_{Y^X} g$ if there is an edge $f(x) \sim_Y g(x')$ whenever there is an edge $x \sim_X x'$. (Here $f$ plays the role of $e_{0, a}$ in the previous paragraph, and $g$ plays the role of $e_{0, b}$.)