1.4. Relations in a topos [0005]
We may define the category of relations in the topos $\ECat$ (written $\REL{\ECat}$) in the following manner:
- we set $\Ob{\REL{\ECat}} = \Ob{\ECat}$;
- an arrow from $X$ to $Y$ in $\REL{\ECat}$ is a subobject of $X\times Y$ in $\ECat$ — more precisely an arrow from $X\times Y$ into $\Omega$;
- the composition of $\phi:X\times Y\to \Omega$ and $\psi:Y\times Z\to\Omega$ is done by taking the fibered product $P$ over $Y$ of the subobjects corresponding to $\phi$ and $\psi$ and taking the characteristic function of the image of $P$ in $X\times Z$.
The verification of the fact that $\REL{\ECat}$ is a category is left to the reader.
We embed $\ECat$ into $\REL{\ECat}$ by associating to $f : X\to Y$ the arrow $\prn{\Idn{X},f} : X \to X\times Y$; this embedding factors through the (obvious) embedding of $\ECat\Sub{p}$ into $\REL{\ECat}$.
The embedding $I$ of $\ECat$ into $\REL{\ECat}$ admits a right adjoint.
Proof. Since for each $X,Y\in\Ob{\ECat}$ we have
we see that the functors $\REL{\ECat}\brk{I\prn{-},Y}$ are representable.
There is therefore an adjoint, whose value at $Y$ is $\Omega^Y$. Let us explain its value on morphisms: a morphism $\phi:X\to Y$ in $\ECat$ is sent to the morphism $\Omega^\phi:\Omega^X\to \Omega^Y$ in $\REL{\ECat}$ defined as the cartesian adjoint to the characteristic function of the subobject of $\Omega^X\times Y$ obtained by taking the image of the fibered product of $\in\Sub{X}$ and $R\Sub{\phi}$ over $X$.
In $\SET$, we find that $\Omega^\phi$ sends each $X\tick\subseteq X$ to $\brc{y \mid \prn{\exists x} \prn{x\in X\tick \text{ and } \phi\prn{x,y} \text{ is true}}}$.
If $\phi$ corresponds to the graph of an operation $f:X\to Y$, then $X\tick$ is sent to $\brc{y\mid \prn{\exists x}\prn{x\in X\tick \text{ and } y=f\prn{x}}}$. ∎
This suggests that by preceding the adjoint in question by the embedding $I$ we shall obtain the “existential quantification” (which sends $X$ to $\Omega\Sup{X}$ and $f$ to $\exists\Sub{f}$) from $\ECat$ to $\ECat$. Indeed, the image of the fibered product of $\in\Sub{X}$ and $\prn{\Idn{X},f}$ — therefore of $\in\Sub{X}$ — over $\Omega\Sup{X}\times Y$ is indeed the vertical composite depicted below: