Exponentiable functors | Synthetic category theory

Chapters 1 and 2 use the rebuild2 formalization. Agda links for Chapter 3 remain temporarily unavailable.

3.5 Exponentiable functors

For a category $T$, we may consider categories $C$ equipped with a functor $f\colon C \to T$, which we will refer to as categories over $T$ (to be discussed in more detail in Chapter 4 (outside selection)). Given a functor $p\colon S \to T$, we obtain a notion of base change along $p$: \begin {align*} \{\text {categories }&\text {over $T$ }\} &&\to &\{\text {categories }&\text {over $S$ }\} \\ f\colon C &\to T &&\mapsto &p^*(f)\colon C \times _T &S \to S. \end {align*}

This assignment admits a left adjoint, given by postcomposition with $p$: \begin {align*} \{\text {categories }&\text {over $S$ }\} &&\to &\{\text {categories }&\text {over $T$ }\} \\ g\colon D &\to S &&\mapsto &p \circ g\colon D &\to T. \end {align*}

However, in general this assignment will not admit a right adjoint. Let us illustrate this with the following simple counterexample:

Example 3.5.1. Consider the functor $p = d_1\colon [1] \to [2]$ given by $d_1(0) = 0$ and $d_1(1) = 2$. We will argue that pullback along $p$ does not preserve pushouts of categories, and hence cannot admit a right adjoint. To see this, consider the following commutative square:

Commutative diagram from the manuscript; its arrows and comparisons are described in the surrounding text. — (3.1)

We see as a consequence of the Segal axiom Axiom E that this is a pushout square of categories. If we pull back this square along the functor $d_1\colon [1] \to [2]$, we obtain the commutative square

But this is no longer a pushout square of categories: if it were, then it would remain a pushout square after passing to geometric realization by Corollary 3.4.7. But since $\geom {[1]} \iso *$ by part (2) of Proposition 3.4.4, this square takes the form

and this is only a pushout square if $* \sqcup * \iso *$. Consequently, in every model in which $*\sqcup *$ is not equivalent to $*$, the functor $d_1$ is not exponentiable. This supplies the intended semantic counterexample. The non-equivalence $*\sqcup *\not \simeq *$ is not a consequence of the axioms imposed so far, so we do not claim internally that $d_1$ fails to be exponentiable in every model.

As the previous example indicates, we cannot expect the existence of a right adjoint to $p^*$ in full generality. There is, however, a large class of functors, the exponentiable functors, for which this right adjoint does exist. This class includes cartesian and cocartesian fibrations, to be introduced in Chapter 5 (outside selection).

In this section, we will give a precise definition of this class of functors. We start with some auxiliary definitions and constructions.

Definition 3.5.2. Let $S$ be a category and let $f\colon C \to S$ and $g\colon D \to S$ be categories over $S$. We define the category $\Fun _S(C,D)$ of functors $C \to D$ over $S$ as the following pullback:

Note that objects of $\Fun _S(C,D)$ are pairs $(h,\alpha )$ where $h\colon C \to D$ is a functor and $\alpha $ is an identification $f = g \circ h$. In other words, objects are commutative triangles of the form

We write $\Map _S(C,D)$ for the groupoid core of $\Fun _S(C,D)$, which fits into a pullback square of the form

Construction 3.5.3. Let $p\colon S \to T$ be a functor. For categories $C$ and $D$ over $T$, we obtain an induced functor \[ p^*\colon \Fun _T(C,D) \to \Fun _{S}(C \times _T S, D \times _T S) \] by noting that the composite $\Fun _T(C,D) \to \Fun (C,D) \xrightarrow {p^*} \Fun (C \times _T S, D \times _T S)$ lands in the correct fiber.

Definition 3.5.4 (Dependent product). Consider a functor $p\colon S \to T$ and let $f\colon C \to S$ be a category over $S$. A dependent product of $C$ along $p$ is a category $g\colon D \to T$ over $T$ equipped with a functor $\varepsilon \colon D \times _T S \to C$ over $S$ which satisfies the property that for any other category $E \to T$ over $T$ the composite functor \[ \Map _{T}(E, D) \xrightarrow {p^*} \Map _{S}(E \times _T S, D \times _T S) \xrightarrow {\varepsilon \circ -} \Map _{S}(E \times _T S, C) \] is an equivalence.

If a dependent product of $C$ along $p$ exists, it is unique; see Exercise 3.8.6. We will denote it by $p_*(f)\colon p_*(C) \to T$.

Terminology 3.5.5. Assume that $C$ admits a dependent product $p_*(C)$ along $p$. Given a functor $\varphi \colon D \to p_*(C)$ over $T$, we obtain a functor \[ \varphi ^u := \varepsilon \circ p^*(\varphi )\colon D \times _T S \to C \] over $S$ that we will refer to as the relative uncurrying of $\varphi $. Conversely, there is for every functor $\psi \colon D \times _T S \to C$ over $S$ a relatively curried functor $\psi _c\colon D \to p_*(C)$, satisfying \[ (\varphi ^u)_c = \varphi \qquadtext { and } (\psi _c)^u = \psi . \] In this way, we may think of the equivalence in Definition 3.5.4 as a relative version of currying/uncurrying.

Construction 3.5.6. Consider a pullback square

of categories, and let $f\colon C \to S$ be a category over $S$. Assume that:

There exists a dependent product $p_*(C) \to T$ of $C$ along $p$;
There exists a dependent product $p'_*(C \times _S S') \to T'$ of $C \times _SS'$ along $p'$.

We will construct a functor \[ \BC _*\colon p_*(C) \times _{T} T' \to p'_*(C \times _S S') \] over $T'$ called the Beck-Chevalley map. By relative uncurrying, we may equivalently define $\BC _*$ by specifying a map $(p_*(C) \times _{T} T') \times _{T'} S' \to C \times _S S'$, which we take to be the map \[ (p_*(C) \times _{T} T') \times _{T'} S' \simeq (p_*(C) \times _{T} S) \times _{S} S' \xrightarrow {\varepsilon \times _S S'} C \times _S S'. \]

We are now ready to introduce the class of exponentiable functors.

Definition 3.5.7. Let $p\colon S \to T$ be a functor. We say that $p$ is exponentiable if the following two conditions are satisfied:

(1)

For every pullback square

and every category $C'$ over $S'$, there exists a dependent product $p'_*(C') \to T'$ of $C'$ along $p'$.

(2)

For every pullback diagram

and every $f'\colon C' \to S'$, the Beck-Chevalley map $\BC _*\colon p'_*(C') \times _{T'} T'' \to p''_*(C' \times _{S'} S'')$ is an equivalence.

Remark 3.5.8. Note that exponentiable functors are by definition closed under base change: if $p\colon S \to T$ is exponentiable, then so is any base change $p'\colon S' \to T'$ of $p$.

Construction 3.5.9. Let $p\colon S \to T$ be an exponentiable functor, and write $\varepsilon _C\colon p_*(C)\times _T S\to C$ and $\varepsilon _D\colon p_*(D)\times _T S\to D$ for the evaluation functors. A functor $\varphi \colon C\to D$ over $S$ determines a composite \[ p_*(C)\times _T S\xrightarrow {\varepsilon _C}C\xrightarrow {\varphi }D \] over $S$. Its relative currying is a functor $p_*(\varphi )\colon p_*(C)\to p_*(D)$ over $T$. The uniqueness part of relative currying supplies identifications \[ p_*(\id _C) = \id _{p_*(C)} \qquadtext {and}\qquad p_*(\psi \circ \varphi ) = p_*(\psi )\circ p_*(\varphi ). \] Thus dependent products are functorial in categories over $S$.

Lemma 3.5.10. Let $p\colon S \to T$ be an exponentiable functor. Then the assignment $f \mapsto p_*(f)$ preserves pullbacks: given functors $C_1 \to C_3 \leftarrow C_2$ over $S$, there exists a preferred equivalence \[ p_*(C_1 \times _{C_3} C_2) \iso p_*(C_1) \times _{p_*(C_3)} p_*(C_2) \] over $T$.

Proof

Proof. Functoriality of dependent products applied to the two projections constructs the displayed comparison functor. For every category $E$ over $T$, the universal properties of dependent products and pullbacks give equivalences \begin {align*} \Map _T\bigl (E,p_*(C_1\times _{C_3}C_2)\bigr ) &\simeq \Map _S\bigl (E\times _T S,C_1\times _{C_3}C_2\bigr )\\ &\simeq \Map _S(E\times _T S,C_1) \times _{\Map _S(E\times _T S,C_3)} \Map _S(E\times _T S,C_2)\\ &\simeq \Map _T(E,p_*(C_1)) \times _{\Map _T(E,p_*(C_3))} \Map _T(E,p_*(C_2))\\ &\simeq \Map _T\bigl (E,p_*(C_1)\times _{p_*(C_3)}p_*(C_2)\bigr ). \end {align*}

These equivalences are induced by the comparison functor and are natural in $E$. Taking $E$ to be either side of the comparison constructs an inverse over $T$ and identifications between the two composites and the respective identity functors, exactly as in the proof of Proposition 1.4.11. Hence the comparison is an equivalence. □

Corollary 3.5.11. Let $p\colon S \to T$ be an exponentiable functor. If $f\colon C \to S$ is an embedding, then also $p_*(f) \colon p_*(C) \to T$ is an embedding.

Proof

Proof. The identity functor of $T$ exhibits $T\to T$ as the dependent product of $S\to S$ along $p$, so there is a preferred equivalence $p_*(S)\iso T$. Since $f$ is an embedding, its diagonal square is a pullback. Applying Lemma 3.5.10 shows that the diagonal square of $p_*(f)\colon p_*(C)\to p_*(S)\simeq T$ is a pullback. Hence $p_*(f)$ is an embedding. □

The terminology ‘exponentiable’ comes from the fact that it allows us to construct certain ‘exponential objects’ relative to a base category $S$:

Definition 3.5.12. Let $p\colon C \to S$ and $q\colon D \to S$ be two functors and assume that $p$ is an exponentiable functor. We define the relative functor category $\ulFun _S(C,D) \to S$ as

It comes equipped with an evaluation map \[ \ev \colon \ulFun _S(C,D) \times _S C \to D \] over $S$ satisfying the property that for every other functor $E \to S$ the composite functor \[ \Map _S(E,\ulFun _S(C,D)) \xrightarrow {- \times _S C} \Map _S(E \times _S C, \ulFun _S(C,D) \times _S C) \xrightarrow {\ev \circ -} \Map _S(E \times _S C, D). \] is an equivalence. In other words, $\ulFun _S(C,D)$ is an ‘internal hom object’ or ‘exponential object’ for categories over $S$.

Remark 3.5.13. Note that, for a category $T$, the data of a functor $T \to \ulFun _S(C,D)$ is equivalent to the data of a pair $(t,f)$, where $t\colon T \to S$ is a functor and $f\colon T \times _S C \to T \times _S D$ is a functor over $T$.

Observation 3.5.14. For any functor $t\colon T \to S$ and categories $C$ and $D$ over $S$ such that $C \to S$ is exponentiable, there is a pullback square

In particular, the fiber of $\ulFun _S(C,D) \to S$ over an object $s$ of $S$ is the functor category $\Fun (C_s,D_s)$, where $C_s$ and $D_s$ are the fibers of $C$ and $D$ over $s$, respectively.

Proposition 3.5.15. For every category $S$, the terminal functor $p_S\colon S\to *$ is exponentiable. Moreover, if $p\colon C\to S$ is exponentiable and $q\colon D\to S$ is any functor, there is a canonical equivalence \[ \Fun _S(C,D)\iso (p_S)_*\,\ulFun _S(C,D). \]

Proof

Proof. Let $T$ be a category. The base change of $p_S$ along $T\to *$ is the projection $\pr _T\colon T\times S\to T$. Given a category $r\colon E\to T\times S$, let $\delta _T\colon T\to \Fun (S,T\times S)$ be the currying of $\id _{T\times S}$. Define $\Pi _S(E)\to T$ by the pullback square

Uncurrying the upper horizontal functor gives an evaluation functor $\Pi _S(E)\times S\to E$ over $T\times S$. For every category $K\to T$, the pullback property and currying identify \[ \Map _T(K,\Pi _S(E)) \iso \Map _{T\times S}(K\times S,E). \] Thus $\Pi _S(E)$ is a dependent product of $E$ along $\pr _T$. If $T'\to T$ is a functor, the pullback defining $\Pi _S(E)$ base changes to the analogous pullback over $T'$, since functor categories preserve pullbacks. The resulting Beck–Chevalley map is therefore an equivalence. This proves that $p_S$ is exponentiable.

Now let $p\colon C\to S$ and $q\colon D\to S$ be as in the statement. For every category $K$, the universal properties of the dependent product and the relative functor category give equivalences \begin {align*} \Map \bigl (K,(p_S)_*\ulFun _S(C,D)\bigr ) &\simeq \Map _S(K\times S,\ulFun _S(C,D))\\ &\simeq \Map _S(K\times C,D)\\ &\simeq \Map (K,\Fun _S(C,D)). \end {align*}

These equivalences are induced by evaluation and are natural in $K$. Hence the canonical functor $\Fun _S(C,D)\to (p_S)_*\ulFun _S(C,D)$ is an equivalence by Proposition 1.4.11. □

Corollary 3.5.16. Let $p\colon C\to S$ be exponentiable and let $q\colon D\to S$ be any functor. Then there is a canonical equivalence \[ \Map _S(C,D)\iso \bigl ((p_S)_*\,\ulFun _S(C,D)\bigr )^\simeq . \]

Proof

Proof. The definition of $\Map _S(C,D)$ and preservation of pullbacks by groupoid cores give $\Map _S(C,D)\iso \Fun _S(C,D)^\simeq $. Now apply the preceding proposition. □

Supplementary notes

Triangles over a base AI-generated
Base change of triangles AI-generated
Relative currying and evaluation AI-generated