Proving $\mathcal{P}(g \circ f) = \mathcal{P}(g) \circ \mathcal{P}(f)$ in a general topos

Question

I'm going through Goldblatt's "Topoi", and I'm stuck on exercise 12.5.3. There, he suggests proving that $\Omega^{g \circ f} = \Omega^g \circ \Omega^f$, where $\Omega^f$ is the morphism $f : a \rightarrow b$ lifted to act on the "powerset" $\Omega^a$ (hence $\Omega^f : \Omega^a \rightarrow \Omega^b$).

Since this doesn't seem to be a too common thing, here's how Goldblatt defines $\Omega^f$ for a given $f$:

1. Take the evaluation arrow $\text{ev}_a : \Omega^a \times a \rightarrow \Omega$. Treat it as a character of some subobject $\overline{\text{ev}_a} : \bullet \rightarrowtail \Omega^a \times a$ (we don't care about the domain, hence $\bullet$).
2. Take the image arrow $1_{\Omega^a} \times f\ [\overline{\text{ev}_a}]$, which is the monic part of the epi-monic factorization of $(1_{\Omega^a} \times f)\circ (\overline{\text{ev}_a})$. This is going to be some morphism into $\Omega^a \times b$.
3. Take the exponential adjoint of the character of this morphism and call it $\Omega^f$.

Or, graphically:

Now, I can't think of any other proof strategy except to show that $\Omega^g \circ \Omega^f$ makes the diagram defining $\Omega^{g \circ f}$ commute. Or, in other words, I'm aiming to show that $\Omega^g \circ \Omega^f$ is the exponential adjoint for $\text{char}\ 1_{\Omega^a} \times gf [\overline{\text{ev}_a}]$. How do I prove that?

The top triangle here commutes by definition of $\Omega^g$ (where $g : b \rightarrow c$), so I only need to prove that the bottom one commutes:

Here it's perhaps time to use the definition of $\text{char}$, and I was trying to prove that the top part here:

could be completed to form a pullback, hence the outer square would be pullback by the pullback lemma, hence I'll get the desired result by the $\Omega$-axiom, but all my attempts at proving that were a dead end.

Am I on the right track? What's the most straightforward way to do this exercise?

Answer 1

The most straightforward proof would be to use Yoneda's lemma and the corresponding point of view. Thus, let us start by defining a morphism of functors $f_* : \operatorname{Sub}({-} \times a) \to \operatorname{Sub}({-} \times b)$ which takes a subobject $S$ of $u\times a$ to the image of $(\operatorname{id}_u \times f)\circ \operatorname{inc}_S \in \operatorname{Hom}(S, u \times b)$. To see this is indeed a natural transformation is simple: if you take the epi-mono factorization of $(\operatorname{id}_u \times f) \circ \operatorname{inc}_S$, and then for $\alpha \in \operatorname{Hom}(v, u)$ you take the fibered product of this factorization with $\alpha \times \operatorname{id}_b \in \operatorname{Hom}(v\times b, u\times b)$, you get an epi-mono factorization of $(\operatorname{id}_v \times f) \circ \operatorname{inc}_{\alpha^* S}$.

We can similarly define $g_* : \operatorname{Sub}({-} \times b) \to \operatorname{Sub}({-} \times c)$ and $(g\circ f)_* : \operatorname{Sub}({-} \times a) \to \operatorname{Sub}({-} \times c)$. We claim that $(g\circ f)_* = g_* \circ f_*$. To see this, suppose we have a subobject $S$ of $u \times a$. Then by the definition of $f_*(S)$, we have an epimorphism $S \to f_*(S)$ and a monomorphism $f_*(S) \to u\times b$ which is exactly what we consider to be the canonical inclusion. Also, by the definition of $g_*$, we have an epimorphism $f_*(S) \to g_*(f_*(S))$ and a monomorphism $g_*(f_*(S)) \to u \times c$. Now, the composition of the two epimorphisms gives an epimorphism $S \to g_*(f_*(S))$; so by the uniqueness of epi-mono factorization, and the easy fact that $(\operatorname{id}_u \times g) \circ (\operatorname{id}_u \times f) = \operatorname{id}_u \times (g \circ f)$, we get that $(g\circ f)_*(S) = g_*(f_*(S))$ as subobjects of $u\times c$.

Now, by the Yoneda lemma, corresponding to $f_*$, $g_*$, and $(g\circ f)_*$, we have morphisms $\Omega^a \to \Omega^b$, $\Omega^b \to \Omega^c$, and $\Omega^a \to \Omega^c$. If you look at the proof of the Yoneda lemma, it is easy to see that these corresponding morphisms give exactly $\Omega^f$, $\Omega^g$, and $\Omega^{g\circ f}$ as constructed in the problem statement. Then, from the easy fact that the Yoneda lemma correspondence respects compositions (which might even be directly in some formulations of the Yoneda lemma), we conclude that $(g\circ f)_* = g_* \circ f_*$ implies $\Omega^{g\circ f} = \Omega^g \circ \Omega^f$.

---

Of course, as it often happens, we can fairly easily unfold the proof of the Yoneda lemma to get a direct proof. In this case, I think it would involve taking the special case of the argument above where $u = \Omega^a$ and $S$ is the subobject of $\Omega^a \times a$ corresponding to $\operatorname{ev}_{a, \Omega} : \Omega^a \times a \to \Omega$. If you trace through, it might also end up involving a special case of the naturality condition on $g_*$ and/or $f_*$. However, in my opinion, using the unfolded proof would obscure the essential point of the argument above, which is that taking images of subobjects acts well with respect to compositions.

Answer 2

An alternative approach is to use the internal language of the topos. In fact, a very small fragment (the simply typed $\lambda$-calculus) is already enough.

The power object $PX$ is the exponential $\Omega^X$ in the topos. When $f: X\to Y$ is a morphism in the topos, then we may add it and its domain and codomain to the signature and write $$x:X\vdash f(x):Y$$ for its action. The right way to translate this is that $x$ is a code for the identity of $X$, so that $f(x) =f\circ id_X = f$. Now the morphism $P(f)$ may be denoted as follows in the internal language.$$\phi:\Omega^Y\vdash\lambda x.\phi (f x):\Omega^X$$ A well defined interpretation procedure tells you exactly what the associated morphism in the topos is in terms of the universal properties of the involved objects. You may read about that in chapter 2 of Bart Jacobs' book Categorical Logic and Type Theory. It is really not that hard and you can learn it before you learn about the full internal language of a topos.

Now, assume we have to morphisms $f:X\to Y$ and $g:Y\to Z$. Comosition in the topos corresponds to substitution in the $\lambda$-calculus, and so we see that the composite $Pf\circ Pg$ is the interpretation of the following expression. $$\phi: \Omega^Z\vdash \lambda x.(\lambda y.\phi (g y))(f x): \Omega^X$$ We use the typical computer science convention that $\lambda$s bind as far as they can. Now the rules of the $\lambda$-calculus (and the soundness of the interpretation with respect to those rules) tell us that this is the same morphism as the one denoted by the expression below. $$\phi: \Omega^Z\vdash \lambda x.\phi (g(f x)): \Omega^X$$ But the interpretation of that morphism will be exactly the map $P(g \circ f)$, and that finishes the proof.