Singleton map is always monic

Question

Let $\mathcal{T}$ be a topos and $X,Y$ objects in $\mathcal{T}$. Let $\delta_X=\langle 1_X,1_X\rangle\colon X\to X\times X$ be the diagonal map, $\Delta_X\colon X\times X\to\Omega$ the map which classifies $\delta_X$ and $\{\cdot\}\colon X\to\Omega^X$ the exponential transpose of $\Delta_X$. Show that $\{\cdot\}$ is monic.

My attempt:

Let $f,g\colon Y\to X$ such that $\{\cdot\}f=\{\cdot\}g$, and let $H\colon X\times Y\to\Omega$ be the transpose of $\{\cdot\}f=\{\cdot\}g$. I want to show that $H$ classifies both $\langle f, 1_Y\rangle$ and $\langle g, 1_Y\rangle$. I showed that $$t\circ !_Y = t\circ !_X\circ f=\Delta_X\circ\delta_X\circ f=\text{ev}_X\circ\langle f,\{\cdot\}f\rangle=H\circ\langle f, 1_Y\rangle $$ (where $!_X$ is the unique map $X\to 1$) and similarly for $g$. But I'm stuck on showing that this square

is a pullback diagram.

Answer 1

Exponential transposition is a bijection between morphisms $X\times Y\to\Omega$ and morphisms $Y\to\Omega^X$, natural in $Y$. Thus $H\colon X\times Y\to\Omega$ being the exponential transpose of $\{\cdot\}f=\{\cdot\}g$ is the composite $\Delta_X 1_X\times f=\Delta_X1_X\times g$.

In particular, since the subobject of $X\times Y$ classified by $H\colon X\times Y\to\Omega$ is the pullback of the canonical subobject of $\Omega$, by the pullback lemma it is also the pullback along both $1_X\times f,1_X\times g\colon X\times Y\to X\times X$ of pullback along $\Delta_X\colon X\times X\to\Omega$ of the canonical subobject, i.e. of $\delta_X=(1_X,1_X)\colon X\to X\times X$.

Now in general, the pullback of $(1_X,1_X)\colon X\to X\times X$ along $1_X\times h\colon X\times Y\to X\times X$ is $(h,1_Y)$. Indeed, a pair of morphisms $x\colon W\to X$ and $(x',y)\colon W\to X\times Y$ satisfy $(1_X,1_X)\circ x=(h,1_Y)\circ(x'y,)$ if and only if $(x,x)=(h\circ y,x')$, i.e. if and only if $x'=h\circ y$.

Thus, $(f,1_Y),(g,1_Y)\colon Y\to X\times Y$ are both pullbacks of $(1_X,1_X)\colon X\to X\times X$ along $1_X\times f,1_X\times g\colon X\times Y\to X\times X$, and are hence classified by $H=\Delta_X1_X\times f=\Delta_X1_X\times g$.

Answer 2

It is a standard fact that for $f \in \operatorname{Hom}(U, X)$, $\{\}_X \circ f \in \operatorname{Hom}(U, P(X)) \simeq \operatorname{Sub}(U \times X)$ corresponds to the graph of $f$, i.e. the subobject $\Gamma_f$ given by the monic morphism $(\operatorname{id}_U, f) \in \operatorname{Hom}(U, U \times X)$. Now given such a graph subobject, we know that $\pi_1 \circ (\operatorname{id}_U, f) = \operatorname{id}_U$ is an isomorphism, and we can recover $f$ as the composition of $\pi_2 \circ (\operatorname{id}_U, f)$ and the inverse of $\pi_1 \circ (\operatorname{id}_U, f)$. Therefore, if for $f, g \in \operatorname{Hom}(U, X)$ there is an isomorphism of subobjects of $U\times X$, $\Gamma_f \simeq \Gamma_g$ we see that we must have $f = g$. (Alternatively, you can just show directly that if you have an isomorphism of subobjects $(\operatorname{id}_U, f) \in \operatorname{Mon}(U, U \times X)$ and $(\operatorname{id}_U, g) \in \operatorname{Mon}(U, U \times X)$, then that isomorphism must act as $\operatorname{id}_U$ on $U$, and from there conclude that $f = g$. I just thought the other argument I gave would have more of a geometric flavor to show why two morphisms with the same graph must be equal. It would generalize the argument in the case of $\mathbf{Set}$ that to recover a function $f : X\to Y$ from its graph, you can take a point $x\in X$, find the unique point on the graph with first coordinate equal to $x$, and then take the second coordinate of that point.)

It follows that $\{\}_X \circ {-} : \operatorname{Hom}(U, X) \to \operatorname{Hom}(U, P(X))$ is injective for each $U$. By definition, this shows that $\{\}_X$ is monic.

---

Yet another way to construct a proof would be via the machinery of the internal language of a topos. First, by tracing through some definitions, we can see that $\{\}_X$ amounts to exactly the interpretation of the term $\lambda (x : X) . [\{ y : X \mid x = y \} : P(X)]$. Now, to show this is monic, it suffices to show that the interpretation of the formula $\forall (x_1, x_2 : X), \{ y : X \mid x_1 = y \} = \{ y : X \mid x_2 = y \} \rightarrow x_1 = x_2$ is equal to $\top \in \operatorname{Hom}(1, \Omega)$. But it is easy to give a formal proof of this formula as a theorem of the (intuitionistic) internal logic of a topos, which certainly implies its interpretation will always be $\top$. The informal description of this proof would be: we have that $x_1 \in \{ y:X \mid x_1 = y \}$. Therefore, by substitution, we also have $x_1 \in \{ y:X \mid x_2 = y \}$, which gives exactly that $x_2 = x_1$. By symmetry of equality, we conclude $x_1 = x_2$ as desired.