5
$\begingroup$

Let Rel be the category whose objects are sets and whose morphisms are binary relations, with composition defined by $x (S \circ R) z \Leftrightarrow (\exists y : x R y \wedge y S z)$, and identity the equality relation.

If we have relations $R \in Rel(X, X')$ and $S \in Rel(Y, Y')$, we can define a relation $(R \to S) \in Rel(X \to Y, X' \to Y')$ by \begin{equation} f (R \to S) g \Leftrightarrow (\forall x \in X, x' \in X' : x R x' \Rightarrow f(x) S g(x')), \end{equation} i.e. functions are related iff they map related arguments to related values.

Unfortunately, this does not constitute a bifunctor $\to : Rel \times Rel \to Rel$. Indeed, composition is not respected. We have $(R' \to S') \circ (R \to S) \subseteq (R' \circ R) \to (S' \circ S)$, but in general these relations are not equal.

My question is: what is this operation $\to$? Is its behaviour documented, and perhaps an instance of a more general structure?

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ I don't quite see how to apply these ideas here, but whenever thinking about how functions and relations interact, I usually find it helpful to think about the proarrow equipment formed by sets, functions, and relations. $\endgroup$
    – Tim Campion
    Commented May 11, 2016 at 1:47

3 Answers 3

Reset to default
3
$\begingroup$

The operation you are describing is a cartesian closed structure, not on the category $Rel$ of sets (as objects) and relations (as morphisms), but rather on a category whose objects are relations and whose morphisms are pairs of functions mapping related arguments to related results. This is a bit easier to see/explain if instead of considering (binary) relations, we consider (unary) predicates.

So, let $SubSet$ be the category whose objects are pairs $(A,P\subseteq A)$ of a set together with a predicate on that set, and whose morphisms $(A,P) \to (B,Q)$ are functions $f : A \to B$ mapping arguments in $P$ to results in $Q$: $$\forall a.\, a \in P \Rightarrow f(a) \in Q$$ There is an obvious functor $\pi : SubSet \to Set$ given by the first projection. Now, the key fact is that $\pi$ is a strict cartesian closed functor. This means that for any pair of predicates $P \subseteq A$ and $Q \subseteq B$, there are predicates \begin{align*} P\times Q &\subseteq A \times B \\ Q^P & \subseteq B^A \end{align*} such that $(A\times B,P\times Q)$ and $(B^A,Q^P)$ are respectively the product and exponential in $SubSet$. In particular, $P\times Q$ and $Q^P$ are defined by \begin{align*} (a,b) \in (P\times Q) \quad &\text{iff}\quad a\in P \wedge b\in Q \\ f \in Q^P \quad &\text{iff}\quad \forall a.\,a\in P \Rightarrow f(a)\in Q \end{align*} Essentially the same explanation goes through in the case of binary relations, but in that case we consider a category $Sub(Set\times Set)$ equipped with a projection functor $\pi' : Sub(Set\times Set) \to Set\times Set$. Once again the key point is that $\pi'$ is a strict cartesian closed functor. Note that these projection functors have some other important properties as well (for example, they are bifibrations), but for the construction alluded to in your question this cartesian closed structure suffices.

Finally, if you are interested in reading more about this categorical approach to "logical predicates", you might have a look at Hermida's thesis (as well as some of the followup literature):

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thanks. However, now I don't have any information about composition of relations at all. What I am interested in, is how the $\to$-nonfunctor interacts with the category structure of $Rel$. I guess in the discreption you give here, we could define a category $Composable$ as the pullback in Cat of the diagram $Sub(Set \times Set) \xrightarrow{src} Set \xleftarrow{tgt} Sub(Set \times Set)$ and then a functor $\circ: Composable \to Sub(Set \times Set)$. Now the problem I initially noted, becomes: the functor $\circ$ does not preserve exponentials. $\endgroup$
    – anuyts
    Commented May 11, 2016 at 13:53
  • 1
    $\begingroup$ Indeed, viewing relations as objects of $\mathcal{R} = Sub(Set\times Set)$, composition of relations corresponds to a functor $\circ : \mathcal{R} \times_{src,tgt} \mathcal{R} \to \mathcal{R}$. The fact that $\circ$ does not preserve exponentials is just that: a property of the functor...which is good, because we've managed to replace a "problem" by a "property". I'm not sure what exactly was your motivation for this question, but you might also find the intro to arxiv.org/abs/1601.06098 interesting, where some related issues are discussed (in particular, see equations (6) and (7)). $\endgroup$
    – Noam Zeilberger
    Commented May 11, 2016 at 15:14
0
$\begingroup$

Assuming that the second f is supposed to be g, notice that functions are also relations. So, f is related to g iff the square $$ \begin{array}{ccc} X & \stackrel{R}{\to} & X' \\ f \downarrow & & \downarrow g \\ Y & \stackrel{S}{\to} & Y' \end{array} $$ commutes.

Edit: Only the forward implication holds.

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ Sorry for the typo, I corrected the question. I agree that if the square commutes, then $f (S \circ R) g$, but I disagree on the opposite implication. Consider the case where Y = Y' = {0, 1}, both f and g are the constant maps $x \mapsto 0$ and $S$ is the true relation. Then $f$ and $g$ are related, but the square does not commute if $X \neq \emptyset$. Indeed, take $x \in X$. Then $x (S \circ f) 1$ holds, because $f(x) = 0 \wedge 0 \mathrel{S} 1$, but $x (g \circ R)1$ does not hold, because $1$ is not in the image of $g$. $\endgroup$
    – anuyts
    Commented May 6, 2016 at 7:21
  • 1
    $\begingroup$ I guess the "iff" holds if you take the square to be a 2-morphism, i.e. if you take it to mean $g \circ R \subseteq S \circ f$. $\endgroup$
    – anuyts
    Commented May 6, 2016 at 7:28
0
$\begingroup$

It is a lax functor that preserves identity.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .