1. A few reminders [0000]

[0001] 1.1 (Elementary topos).

An elementary topos is a category $\ECat$ satisfying the following conditions:

  1. $\ECat$ inductive and finite projective limits;
  2. $\ECat$ admits exponentials: for each $A\in \Ob{\ECat}$, the functor $(-)\times A : \ECat\to\ECat$ admits a right adjoint, written $\prn{-}\Sup{A}$;
  3. $\ECat$ has an arrow $v : \ObjTerm{\ECat}\to \Omega$ that for each $X\in \Ob{\ECat}$ the arrows from $X$ to $\Omega$ give by fibered product with $v$ exactly the subobjects of $X$.

We can reduce these axiomatics, as recent work by A. Kock and Ch. Mikkelson (Hurd & Loeb, 1974) has shown, and describe for example in the manner of F.W. Lawvere (Lawvere, 1972) an elementary topos as a cartesian closed category in which the notion of a subobject is representable.

[0002] 1.2 (Axiomatics in terms of partial morphisms).

We know that for a topos $\ECat$ the embedding functor into the category $\ECat\Sub{p}$ of partial morphisms admits a right adjoint. This property can also be substituted for axiom (3) of 1.1 [0001].

We will describe a different embedding of interest below.

[0003] 1.3 (The algebra of subobjects).

We also know that for each object $X$ of a topos $\ECat$, the category $\Sl{\ECat}{X}$ of objects above $X$ is again a topos, and that each arrow $f : X \to Y$ determines a functor $\InvImg{f} : \Sl{\ECat}{Y}\to\Sl{\ECat}{X}$ which admits both a left adjoint (written $\Sigma\Sub{f}$) and a right adjoint (written $\Pi\Sub{f}$).

If we consider just the subobjects of $X$, we obtain a Heyting algebra $\Opns{X}$ and the functor $\InvImg{f}$ induces $f\Sup{-1} : \Opns{Y}\to \Opns{X}$, which likewise admits a right adjoint ($\forall\Sub{f}$, induced by $\Pi\Sub{f}$) and a left adjoint (written $\exists\Sub{f}$, defined by taking the image). By the cartesian adjunction, the objects of $\Opns{X}$ amount to points of $\Omega\Sup{X}$ and the action of the last three functors can be described by arrows of the topos. Thus restricting the image of $A\times f$ to a subobject of $A\times X$ amounts to composing the cartesian adjoint of its characteristic function with the arrow $\exists\Sub{f} : \Omega\Sup{X}\to\Omega\Sup{Y}$, which corresponds exactly to the restriction of the image of $\Omega\Sup{X}\times f$ to $\in\Sub{X}\rightarrowtail \Omega\Sup{X}\times X$ (the subobject characterized by evaluation).

[0004] Translator’s Note 1.3·a (Images).

I have taken some liberties with the wording involving images in 1.3 [0003] in order to conform with English mathematical usage; for instance, I have translated phrases like “prendre l’image par $f$ d’un sous-objet de $X$” as “restricting the image of $f$ to a subobject of $X$”.

[000I] Translator’s Note 1.3·b (Cartesian adjunction).

We note that Bénabou writes “adjonction cartésienne” to refer to the product-exponential adjunction $\prn{-}\times X \dashv \prn{-}\Sup{X}$. Although this terminology is not current, we have retained it as “the cartesian adjunction”.

Another aspect of Bénabou’s terminology that we have retained is the use of “adjoint” to mean “adjoint transpose”; for instance, Bénabou speaks of the “cartesian adjoint” $T\times X\to Y$ of a morphism $T\to Y\Sup{X}$.

1.4. Relations in a topos [0005]

[0007] Definition 1.4·a.

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.

[0008] Lemma 1.4·b.

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}$.

[0006] Proposition 1.4·c.

The embedding $I$ of $\ECat$ into $\REL{\ECat}$ admits a right adjoint.

Proof. Since for each $X,Y\in\Ob{\ECat}$ we have

$$ \begin{aligned} \REL{\ECat}\brk{I\prn{X},Y} &= \Hom{\ECat}{X\times Y}{\Omega}\\ &\cong \Hom{\ECat}{X}{\Omega\Sup{Y}} \end{aligned} $$

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}}}$. ∎

[0009] Remark 1.4·d.

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: