A coherence relation $\symp_X$ on a set $X$ is a reflexive and symmetric relation. A coherence space is a pair $(X, \symp_X)$, and a morphism $f : X \to Y$ between coherence spaces is a relation $f \subseteq X \times Y$ such that for all $(x,y) \in f$ and $(x',y') \in f$,

  1. if $x \symp_X x'$ then $y \symp_Y y'$, and
  2. if $x \symp_X x'$ and $y = y'$ then $x = x'$.

The category of coherence spaces is both Cartesian and monoidal closed. I would like to know when pullbacks or pushouts exist for this category, and when some monoidal analogue of pullbacks or pushout exists (and how to define it, in case this notion makes sense).

  • $\begingroup$ Where is this definition from? The one in Girard, Lafont & Taylor looks very different. $\endgroup$ – Charles Stewart Jan 19 '11 at 14:25
  • $\begingroup$ The two definitions are equivalent. I'm just taking the web as primitive, from which the set of cliques can be derived. $\endgroup$ – Neel Krishnaswami Jan 19 '11 at 16:54
  • $\begingroup$ I find Neel's choice of definition much more comprehensible than the original. $\endgroup$ – Dave Clarke Jan 19 '11 at 18:24
  • 3
    $\begingroup$ I'll state the obvious question: do you know that they don't always exist? In other words, are you familiar with any examples of a functor into coherence relations that doesn't have a limit/colimit? $\endgroup$ – Ohad Kammar Jan 21 '11 at 2:24
  • 1
    $\begingroup$ The two definitions are equivalent - Right, but did you make up this definition, or did you get it from someone else? Great question, btw, I'm surprised that no one seems to know whether equalisers always exist. $\endgroup$ – Charles Stewart Feb 2 '11 at 12:47

I now see how to define equalizers for coherence spaces, which means pullbacks always exist (since products do). I don't know how to do this, actually....

Recall that composition is the usual relational composition, so if $f : A \to B$ and $g : B \to C$, then:

$f ; g = \{(a,c) \in A \times C \;|\; \exists b \in B.\; (a,b) \in f \land (b,c) \in g\}$

(In this definition, the existential actually implies unique existence. Suppose that we have $b' \in B$ such that $(a,b') \in f$ and $(b', c) \in g$. Since we know that $a \Bumpeq_A a$, this means that $b \Bumpeq_B b'$. Then this means that we have $b \Bumpeq_B b'$ and $(b,c) \in g$ and $(b',c) \in g$, so consequently $b = b'$.)

We now construct equalizers. Suppose we have coherence spaces $A$ and $B$, and morphisms $f, g : A \to B$. Now define the equalizer $(E, e : E \to A)$ as follows.

  1. For the web, take $$E = \left\{ \begin{array}{l|c} & \forall b.\; (a,b) \in f \implies \exists a' \Bumpeq_A a.\; (a',b) \in g \\ a \in A & \land \\ & \forall b.\; (a,b) \in g \implies \exists a' \Bumpeq_A a.\; (a',b) \in f \\ \end{array} \right\} $$ This picks out the subset of tokens of $A$ on which either $f$ and $g$ agree (up to coherence -- I had this wrong in my first version), or are both undefined.

  2. Define the coherence relation on $\Bumpeq_E = \{ (a,a') \in \Bumpeq_A \;|\; a \in E \land a' \in E\}$. This is just the restriction of the coherence relation on $A$ to the subset $E$. This will be reflexive and symmetric since $\Bumpeq_A$ is.

  3. The equalizer map $e$ is just the diagonal $e : E \to A = \{(a, a)\;|\;a \in E\}$.

Since I messed up my first version of the proof, I'll give the universality property explicitly. Suppose we have any other object $X$ and morphism $m : X \to A$ such that $m;f = m;g$.

Now define $h : X \to E$ as $\{(x,a) \;|\; a \in E\}$. Obviously $h;i \subseteq m$, but to show the equality we need to show the converse $m \subseteq h;i$.

So assume $(x,a) \in m$. We now need to show that $\forall b.\; (a,b) \in f \implies \exists a' \Bumpeq_A a.\; (a',b) \in g$ and $\forall b.\; (a,b) \in g \implies \exists a' \Bumpeq_A a.\; (a',b) \in f$.

First, assume $b \in B$ and $(a,b) \in f$. So we know that $(x,a) \in m$ and $(a,b) \in f$, so $(x,b) \in m;f$. Therefore $(x,b) \in m;g$, and so there is an $a' \in A$ such that $(x,a') \in m$ and $(a',b) \in g$. Since $x \Bumpeq x$, we know $a \Bumpeq a'$, and so there is an $a' \Bumpeq a$ such that $(a',b) \in g$.

Symmetrically, assume $b \in B$ and $(a,b) \in g$. So we know that $(x,a) \in m$ and $(a,b) \in g$, so $(x,b) \in m;g$. Therefore $(x,b) \in m;f$, and so there is an $a' \in A$ such that $(x,a') \in m$ and $(a',b) \in f$. Since $x \Bumpeq x$, we know $a \Bumpeq a'$, and so there is an $a' \Bumpeq a$ such that $(a',b) \in f$.

| cite | improve this answer | |
  • $\begingroup$ I don't see how you can prove $e$ universal. There is only one way to factor any $m : X \rightarrow A$, and that's by setting $h : X \rightarrow E$ as $h := \{(x, a) : (x,a) \in m, a \in E\}$. Obviously $h;e \subset m$, but I don't see why the converse holds: take some $xma$, and some $b \in B$, with $afb$. Then we have $x(m;f)b$, hence from $m$'s choice we have $x(m;g)b$. From the definition of composition, there exists some $a'$ such that $xma'$ and $a'gb$. We can deduce that $a \symp a'$, but we only know that $afb$ and $a'gb$, so we can't really deduce that $a=a'$ and finish. $\endgroup$ – Ohad Kammar Jan 21 '11 at 12:25
  • $\begingroup$ Yes, you're right -- the subset the equalizer picks out has to be up to coherence, not equality. I've changed the definition to reflect this, and given the proof the diagram commutes explicitly. $\endgroup$ – Neel Krishnaswami Jan 21 '11 at 14:08
  • $\begingroup$ Ah... But now $e$ doesn't equalise the diagram. Indeed, assume $a(e;f)b$. Then, by $e$'s definition, we have $afb$, hence there exists some $a'\symp a$ such that $a'gb$. But we don't have that $aea'$, so we can't show that $a(e;g)b$. You seem to be running into the same problems I ran into last night, hence my obvious question above. But perhaps you'll succeed where I failed! My next step was to take a more sophisticated $e$, say something like $aea' \iff a\symp a'$, but then $e$ is not a valid morphism, so some more careful choice is required. $\endgroup$ – Ohad Kammar Jan 21 '11 at 14:15
  • $\begingroup$ I now remember why I was hoping the answer was in someone's thesis already. :) Anyway, I'll think about it more -- there may be some trick possible via to the fact that inverse images are pairwise incoherent. $\endgroup$ – Neel Krishnaswami Jan 21 '11 at 17:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.