Equivalence of categories preserves cartesian closedness

This is the second part of Exercise I.4 of Mac Lane & Moerdijk's, "Sheaves in Geometry and Logic [. . .]".

The Details:

First we have

Definition 1: A functor $F: \mathbf{A}\to \mathbf{B}$ is an equivalence of categories if for any $\mathbf{A}$-objects $A, A'$, we have that

$$\begin{align} {\rm Hom}_{\mathbf{A}}(A, A')&\to{\rm Hom}_{\mathbf{B}}(FA, FA')\\ p&\mapsto F(p) \end{align}$$

is a bijection and, moreover, any object of $\mathbf{B}$ is isomorphic to an object in the image of $F$.

From p. 17 ibid. . . .

Definition 2: Given two functors

$$F:\mathbf{X}\to \mathbf{A}\quad G: \mathbf{A}\to \mathbf{X},$$

we say that $G$ is right adjoint to $F$, written $F\dashv G$, when for any $X\in{\rm Ob}(\mathbf{X})$ and any $A\in{\rm Ob}(\mathbf{A})$, there is a natural bijection between morphisms

$$\frac{X\stackrel{f}{\to}G(A)}{F(X)\stackrel{h}{\to}A},$$

in the sense that each $f$, as displayed, uniquely determines $h$, and conversely.

There is more to this definition on page 18.

From p. 19 ibid. . . .

Definition 3: Suppose products exist in $\mathbf{C}$. For a fixed $A\in{\rm Ob}(\mathbf{C})$, one may consider the functor

$$A\times -: \mathbf{C}\to \mathbf{C}.$$

If this functor had a right adjoint (unique up to isomorphism), this adjoint is denoted by

$$(-)^A:\mathbf{C}\to \mathbf{C}.$$

In this case $A$ is said to be an exponentiable object of $\mathbf{C}$.

From p. 20 ibid. . . .

Definition 4: A category $\mathbf{C}$ is a cartesian closed category (CCC) if

• it has all finite products (which is equivalent to saying there exists a terminal object and all binary products in $\mathbf{C}$) and

• all $\mathbf{C}$-objects are exponentiable.

The Question:

Let $F:\mathbf{A}\to\mathbf{B}$ be an equivalence of categories. Suppose $\mathbf{A}$ is a CCC. Show that $\mathbf{B}$ is a CCC.

Context:

I am teaching myself topos theory for fun.

I have read (but not fully understood) Goldblatt's, Topoi: [. . .].

Previous questions along these lines from myself include the following:

• The Adjunction $\_\times A\dashv (\_ )^A$ for Preorders: The Deduction Theorem.

• Adjunctions via Universal Arrows: Understanding a Proof.

• Showing $1^A\cong 1$ in a CCC.

But these are from several years ago.

My Attempt:

Terminal object . . .

From the reasoning in

• Equivalence of categories preserves subobject classifiers.

I may conclude that $\mathbf{B}$ has a terminal object.

Binary products . . .

Suppose that $Y, B, B'\in{\rm Ob}(\mathbf{B})$. Then $Y=F(X), B=F(A), B'=F(A')$ for some $X, A, A'\in{\rm Ob}(\mathbf{A})$.

Since $\mathbf{A}$ is a CCC, the product $A\times A'$ exists. So there exist morphisms $\pi_1: A\times A'\to A$ and $\pi_2: A\times A'\to A'$ such that for any $p_1: X\to A$ and any $p_2: X\to A'$, there exists a unique $u: X\to A\times A'$ such that

$$p_1=\pi_1\circ u\quad\text{and}\quad p_2=\pi_2\circ u.$$

Consider $\widetilde{p_i}=F(p_i)$.

We have, by the equivalence, that

$$ {\rm Hom}_{\mathbf{A}}(X, A\times A')\cong {\rm Hom}_{\mathbf{B}}(Y, F(A\times A')),$$

but $\lvert{\rm Hom}_{\mathbf{A}}(X, A\times A')\rvert=\lvert\{u\}\rvert=1,$ so $F(u): Y\to F(A\times A')$ is unique.

Also by equivalence there exists a functor $G:\mathbf{B}\to \mathbf{A}$ such that there are natural transformations $\alpha: F\circ G\stackrel{\sim}{\to}{\rm id}_{\mathbf{B}}$ and $\beta: G\circ F\stackrel{\sim}{\to}{\rm id}_{\mathbf{A}}$.

Define $\widetilde{\pi_i}=F(\pi_i)$. Then we have

$$\begin{align} \widetilde{\pi_i}\circ F(u)=\widetilde{p_i}&\iff F(\pi_i)\circ F(u)=F(p_i) \\ &\iff F(\pi_i\circ u)=F(p_i) \\ &\iff (G\circ F)(\pi_i\circ u)=(G\circ F)(p_i) \\ &\iff {\rm id}_{\mathbf{A}}(\pi_i\circ u)={\rm id}_{\mathbf{A}}(p_i) \\ &\iff \pi_i\circ u=p_i, \end{align}$$

which holds by definition of $u$ (and $G$ is as defined above).

Thus $B\times B'=F(A\times A')$ exists.

Exponents . . .

Since $\mathbf{A}$ is a CCC, each $A, A'\in {\rm Ob}(\mathbf{A})$ is exponentiable.

From $A\times -\dashv (-)^A$, we have

$$\frac{A'\stackrel{f}{\to}A\times A'}{A'^A\stackrel{g}{\to}A'}$$

for some $f, g\in {\rm Mor}(\mathbf{A})$. But then

$$\frac{F(A'\stackrel{f}{\to}A\times A')}{F(A'^A\stackrel{g}{\to}A')},$$

i.e.,

$$\frac{F(A')\stackrel{F(f)}{\to}F(A\times A')=B\times B'}{F(A'^A)\stackrel{F(g)}{\to}F(A')=B'}.$$

But here I am stuck. What does $F(A'^A)$ correspond to in $\mathbf{B}$?

I'm guessing $F(A'^A)\stackrel{?}{\equiv}F(A')^{F(A)}\stackrel{?}{\equiv}B'^B$ in some sense . . .

Please help :)

Solution 1:

An equivalence of categories $F$ it is handier with it's quasi-inverse. And since equivalences can be promoted to adjoint equivalences, let's just take that too.

So consider $G$ to be the right adjoint quasi-inverse to $F$ (since they are equivalences it is also a left adjoint). Now with this we have natural isomorphisms that will help. First of all the product in $\mathbf{B}$ can be written $F(G(B)\times G(B'))$. Consider the functor $$Y \mapsto \text{Hom}_{\mathbf{B}}(F(G(Y)\times G(B)),B').$$ We have the following chain of equivalences natural in $Y$, $$\begin{align} \text{Hom}_{\mathbf{B}}(F(G(Y)\times G(B)),B')&\simeq \text{Hom}_{\mathbf{A}}(G(Y)\times G(B),G(B'))\\ &\simeq \text{Hom}_{\mathbf{A}}(G(Y),G(B')^{G(B)})\\ &\simeq \text{Hom}_{\mathbf{B}}(Y,F(G(B')^{G(B)})). \end{align}$$ This show that $F(G(B')^{G(B)})$ is the exponent object.

Solution 2:

Although it is good to solve these questions by yourself, here is a neat trick you can also use : there is a known result in category theory (I don't really know to whom I should attribute it) which states that all properties that do not mention any equalities between the objects of the category are invariant under equivalence of categories.

With this result it is all very easy :

• The definition of product does not require equality between objects, as it is expressed, for all objects $A$ and $B$ as an object $P$ together with maps $p_A:P\to A$ and $p_B:P\to B$, such that for all other object $X$ equipped with maps $f : X\to A$ and $g:X\to B$, there exists a unique map $(f,g) : X\to P$ such that $p_A(f,g) = f$ and $p_B(f,g) = g$. As you can see this definition is written with equalitied between morphisms (like $p_A(f,g) = f$, but those are allowed), but never do you need equality between objects to formulate it. Hence "products are preserved by equivalence of categories". What I mean by that is, if a category has products, then any category equivalent to it also has products, and the functor defining the equivalence sends the products onto products (up to isomorphism)

• The notion of adjoint functor does not require equality between objects either (you can write down the definition to convince yourself). Hence it is preserved by equivalence of categories. What I mean is if $F : C\to C'$ is a functor with an adjoint, and you have two equivalences of categories $e_1: D \to C$ and $e_2 : C'\to D'$, then the functor $$ e_2 F e_1 : D\to D' $$ also have an adjoint (which is obtained by composing the adjoint of $F$ with the quadi-inverses of $e_1$ and $e_2$)

Now you can see that a CCC is a category which has products and such that the product functor has an adjoint. Since both these notions are invariant under equivalence of categories, so is the one of CCC.

I don't think you should spare yourself from the explicit computation, as it is a good exercise, but this kind of reasoning can come in very handy in the future and really makes obvious which notions are invariant or not. And I think it is a good habit to take, everytime you encounter a new notion to make this little test to see if it is invariant under equivalence of categories or not