ETCS direct image functor

Question

In Lawvere's paper on Elementary Theory of Category of Sets (https://artscimedia.case.edu/wp-content/uploads/2013/07/14182623/Lawvere-ETCS.pdf), at page 27, he proves Lemma 3. by constructing a morphism. For $h:R \to A$, he constructs $\overline{h}:2^R \to 2^A$.

What he does is construct an equalizer $\Psi$ of $R \times 2^R \xrightarrow{\text{eval}} 2$ with $R \times 2^R \to 1 \xrightarrow{i_1} 2$ (I assume $i_1$ plays a role of morphism $\text{true}:1 \to 2$). Afterwards, he composes $\Psi$ with $h \times 2^R$ and taking an image, hence getting a subobject $\text{im} \hookrightarrow A \times 2^R$. Then he takes characteristic function (which I assume is the unique morphism from the definition of subobject classifier), and exponentially transposes it to get $\overline{h}:2^R \to 2^A$.

On the next page, he remarks that we have constructed a covariant direct image functor. I've tried to prove this is a functor, but I couldn't do it.

I've tried proving it for identities ($h = \text{id}_R$), I've concluded that since we are looking at an equalizer, it is a monomorphism, and we compose it with an identity times identity, so the resulting morphism is $\Psi$ itself. Image of a mono is its domain and I use subobject classifier to get $\chi_\Psi$ and transpose it into $\overline{\text{id}_R} := \lambda \chi_\Psi:2^R \to 2^R$. But I don't know how to prove it is equal to $\text{id}_{2^R}$.

As for the composition, I assume I need to prove $\lambda \chi_g \lambda \chi_f = \lambda \chi_{gf}$, but I got nowhere after I constructed $x$ such that $\lambda x = \lambda \chi_g \lambda \chi_f$.

Answer 1

$\require{AMScd}$ First of all, from the role of $2^A$ as a power object of $A$, we can see that for $h : R \to A$, then $\bar h : 2^R \to 2^A$ is the unique morphism such that we have a cartesian square $$\begin{CD} i_h @>>> {\in}_A \\ @V \operatorname{inc}VV @VV \operatorname{inc} V \\ A \times 2^R @> \operatorname{id} \times \bar h >> A \times 2^A \end{CD}$$ where $i_h$ is the image of ${\in}_R \overset{\operatorname{inc}}\to R \times 2^R \overset{h \times \operatorname{id}}\longrightarrow A \times 2^R$. (Here ${\in}_A$ is the subobject of $A \times 2^A$ with characteristic function $\operatorname{eval}_{A, 2}$ and similarly for ${\in}_R$.) Furthermore, using the characterization of image in terms of epi-mono factorization, we see that $\bar h$ is the unique morphism such that we have a commutative diagram $$\begin{CD} {\in}_R @>>> i_h @>>> {\in}_A \\ @V \operatorname{inc} VV @VVV @VV \operatorname{inc}V \\ R \times 2^R @> h \times \operatorname{id} >> A \times 2^R @> \operatorname{id} \times \bar h >> A \times 2^A \end{CD}$$ where the morphism ${\in}_R \to i_h$ is an epimorphism and the right square is cartesian. (Note that the commutativity of the outer rectangle is related to the fact that if $x \in S \subseteq R$, then $h(x) \in \bar h(S)$.)

This immediately gives the identity condition: for any object $A$, we clearly have such a commutative diagram $$\begin{CD} {\in}_A @>>> {\in}_A @>>> {\in}_A \\ @VVV @VVV @VVV \\ A \times 2^A @> \operatorname{id} \times \operatorname{id} >> A \times 2^A @> \operatorname{id} \times \operatorname{id} >> A \times 2^A. \end{CD}$$

Now for the composition condition, suppose we have $g : A \to B$ and $f : B \to C$. Then putting together the above diagrams for $f$ and $g$, we have a commutative diagram $$\begin{CD} {\in}_A @>>> i_g @>>> {\in}_B @>>> i_f @>>> {\in}_C \\ @VVV @VVV @VVV @VVV @VVV \\ A \times 2^A @> g\times\operatorname{id} >> B \times 2^A @> \operatorname{id}\times \bar g >> B \times 2^B @> f\times\operatorname{id} >> C \times 2^B @> \operatorname{id}\times \bar f >> C \times 2^C \end{CD}$$ where the second and fourth squares are cartesian, and the first and third morphisms in the top row are epimorphisms.

Now, considering where we want to end up, let us refactor $(f \times \operatorname{id}) \circ (\operatorname{id} \times \bar g) = (f, \bar g) = (\operatorname{id}, \bar g) \circ (f, \operatorname{id})$, and in the top row, fill in an object constructed to make a second cartesian square. In this way, we get a commutative diagram $$\begin{CD} {\in}_A @>>> i_g @>>> (\operatorname{id} \times \bar g)^* i_f @>>> i_f @>>> {\in}_C \\ @VVV @VVV @VVV @VVV @VVV \\ A \times 2^A @> g\times\operatorname{id} >> B \times 2^A @> f\times\operatorname{id} >> C \times 2^A @> \operatorname{id}\times \bar g >> C \times 2^B @> \operatorname{id}\times \bar f >> C \times 2^C \end{CD}$$ where the right two squares are cartesian, and ${\in}_A \to i_g$ is an epimorphism.

We claim that in fact, the second morphism on the top row, $i_g \to (\operatorname{id} \times \bar g)^* i_f$, is also an epimorphism. To show this, we will show that the commutative square $$\begin{CD} i_g @>>> (\operatorname{id} \times \bar g)^* i_f \\ @VVV @VVV \\ {\in}_B @>>> i_f \end{CD}$$ is cartesian, and then use the fact that ${\in}_B \to i_f$ is an epimorphism. To see this, extend the square above to the commutative diagram $$\begin{CD} i_g @>>> (\operatorname{id} \times \bar g)^* i_f @>>> C \times 2^A \\ @VVV @VVV @VVV \\ {\in}_B @>>> i_f @>>> C \times 2^B. \end{CD}$$ Here, we know that the right square is cartesian; therefore, to show the left square is cartesian, it will suffice to show the composed rectangle is a cartesian square. However, that rectangle can be refactored as $$\begin{CD} i_g @>>> B \times 2^A @> f\times\operatorname{id} >> C \times 2^A \\ @VVV @V \operatorname{id}\times\bar g VV @VV \operatorname{id}\times\bar g V \\ {\in}_B @>>> B \times 2^B @> f\times\operatorname{id} >> C \times 2^B. \end{CD}$$ Here, we know that the left square is cartesian by assumption; and it should be a straightforward exercise to show that the right square is cartesian. Therefore, the outer rectangle is also a cartesian square, completing the proof that $i_g \to (\operatorname{id} \times \bar g)^* i_f$ is an epimorphism.

Now, combining the two left squares, and the two right squares, we get a commutative diagram $$\begin{CD} {\in}_A @>>> (\operatorname{id} \times \bar g)^* i_f @>>> {\in}_C \\ @VVV @VVV @VVV \\ A \times 2^A @> (f\circ g) \times \operatorname{id} >> C \times 2^A @> \operatorname{id} \times (\bar f\circ\bar g) >> C \times 2^C \end{CD}$$ in which the morphism ${\in}_A \to (\operatorname{id} \times \bar g)^* i_f$ is a composition of two epimorphisms, so it is an epimorphism; and the right-hand square is a composition of two cartesian squares, so it is a cartesian square. Therefore, by the uniqueness condition above, we can conclude $\overline{f\circ g} = \bar f \circ \bar g$.

(Note that the proof also gives that $i_{f\circ g} = (\operatorname{id} \times \bar g)^* i_f$ as subobjects of $C\times 2^A$. It might be an interesting exercise to show why this is true in $\mathsf{Set}$.)

Also, note that nothing here used any of the special axioms of ETCS, except for $2$ being the subobject classifier; therefore, the proof above will work for any topos if you just replace $2$ with $\Omega$ throughout.

Answer 2

$\newcommand{\ev}{\mathsf{eval}}\newcommand{\id}{\mathsf{id}}$

Lets start with the identity case. We want to show that $\bar{\id_R}$ is the map $\id_{2^R}$. Note that the map $\id_{2^R}$ corresponds to the map $\ev : R \times 2^R \to 2$ under transposition. Since transposition is an equivalence, it suffices to show that the transpose of $\bar{\id_R}$ is the map $\ev$. By definition, the transpose of $\bar{\id_R}$ is the classifying map of $\mathsf{Im} \to R \times 2^R$. Thus, it is the unique dotted map that fits into the following pullback square:

So it suffices to show that $\ev$ fits into the pushout square where the dotted map is. First we should show that the square with $\ev$ swapped in actually commutes. As you noticed, since $h = \id$, we have that $\mathsf{Im}$ is just the image of $\psi$. By the definition of $\psi$ and $\mathsf{im}$, we have the following commutative diagram:

In particular, $(\mathsf{t} \circ !) \circ \mathsf{im} \circ e = \ev \circ \mathsf{im} \circ e$. But $e$ must be epi, since we are working in a topos. This implies

$$(\mathsf{t} \circ !) \circ \mathsf{im} = \ev \circ \mathsf{im}$$

which proves that $\ev$ makes the first square commute. We of course still need to prove the square is a pullback. So, suppose we have two maps, $j : X \to R \times 2^R$ and $k : X \to \star$ that make the square commute. Since every monomorphism in a topos in regular, we have that the image is the equalizer of the cokernel pair. We can use this (the mapping in property of the equalizer) to construct a map into the image. We have the following diagram

Now, $k = ! \circ j$, by the uniqueness of maps into $\star$. So $\ev \circ j = \mathsf{t} \circ k = \mathsf{t} \circ ! \circ j$. So $j$ equalizes the maps in the definition of $\psi$. Thus we obtain the unique existance of the dotted map $\hat j : X \to E$ such that $\psi \circ \hat j = j$. Since the bottom left square is commutative, it follows that $i_1 \circ \psi \circ \hat j = i_0 \circ \psi \circ \hat j$. By the definition of $\hat j$, this means $i_1 \circ j = i_0 \circ j$. Thus $j$ equalizes the cokernel pair, lending the existence of a unique map (the finely dotted map) $X \to \mathsf{Im(\psi)}$ that commutes with everything.

This proves that the square is a pullback, establishing that $\bar{\id_R} = \id_{R^2}$. Here is a reference for any of the unproven claims I made about the image.

A similar style of argument will prove that the map respects composites. Forgive me for not writing it all out. P.S. noticed we didn't use too many properties specific to the ETCS. We really just need to be working in a topos.