This is a fairly technical article. This article will most likely not have any significance for you if you haven’t heard of the Beck-Chevalley condition before.
When one talks about “indexed (co)products” in an indexed category, it is often described as follows:
Let |\mathcal C| be an |\mathbf S|-indexed category, i.e. a pseudofunctor |\mathbf S^{op} \to \mathbf{Cat}| where |\mathbf S| is an ordinary category. Write |\mathcal C^I| for |\mathcal C(I)| and |f^* : \mathcal C^J \to \mathcal C^I| for |\mathcal C(f)| where |f : I \to J|. The functors |f^*| will be called reindexing functors. |\mathcal C| has |\mathbf S|-indexed coproducts whenever
The first condition is reasonable, especially motivated with some examples, but the second condition is more mysterious. It’s clear that you’d need something more than simply a family of adjunctions, but it’s not clear how you could calculate the particular condition quoted. That’s the goal of this article. I will not cover what the Beck-Chevalley condition is intuitively saying. I cover that in this Stack Exchange answer from a logical perspective, though there are definitely other possible perspectives as well.
Some questions are:
The concepts we’re interested in will typically be characterized by universal properties, so we’ll want an indexed notion of adjunction. We can get that by instantiating the general definition of an adjunction in any bicategory if we can make a bicategory of indexed categories. This is pretty easy since indexed categories are already described as pseudofunctors which immediately suggests a natural notion of indexed functor would be a pseudonatural transformation.
Explicitly, given indexed categories |\mathcal C, \mathcal D : \mathbf S^{op} \to \mathbf{Cat}|, an indexed functor |F : \mathcal C \to \mathcal D| consists of a functor |F^I : \mathcal C^I \to \mathcal D^I| for each object |I| of |\mathbf S| and a natural isomorphism |F^f : \mathcal D(f) \circ F^J \cong F^I \circ \mathcal C(f)| for each |f : I \to J| in |\mathbf S|.
An indexed natural transformation corresponds to a modification which is the name for the 3-cells between the 2-cells in the 3-category of 2-categories. For us, this works out to be the following: for each object |I| of |\mathbf S|, we have a natural transformation |\alpha^I : F^I \to G^I| such that for each |f : I \to J| the following diagram commutes $$\begin{CD} \mathcal D(f) \circ F^J @>\!\!\!\!\!\!\!id_{\mathcal D(f)}*\alpha^J>> \mathcal D(f) \circ G^J \\ @V\cong VV @VV\cong V \\ F^I \circ \mathcal C(f) @>>\!\!\!\!\!\!\!\alpha^I*id_{\mathcal C(f)}> G^I \circ \mathcal C(f) \end{CD}$$ where the isomorphisms are the isomorphisms from the pseudonaturality of |F| and |G|.
Indexed adjunctions can now be defined via the unit and counit definition which works in any bicategory. In particular, since indexed functors consist of families of functors and indexed natural transformations consist of families of natural transformations, both indexed by the objects of |\mathbf S|, part of the data of an indexed adjunction is a family of adjunctions.
Let’s work out what the additional data is. First, to establish notation, we have indexed functors |F : \mathcal D\to \mathcal C| and |U : \mathcal C \to \mathcal D| such that |F \dashv U| in an indexed sense. That means we have |\eta : Id \to U \circ F| and |\varepsilon : F \circ U \to Id| as indexed natural transformations. The first pieces of additional data, then, are the fact that |F| and |U| are indexed functors, so we have natural isomorphisms |F^f : \mathcal C(f)\circ F^J \to F^I\circ \mathcal D(f)| and |U^f : \mathcal C(f) \circ U^J \to U^I \circ \mathcal D(f)| for each |f : I \to J| in |\mathbf S|. The next pieces of additional data, or rather constraints, are the coherence conditions on |\eta| and |\varepsilon|. These work out to $$\begin{gather} U^I(F^f)^{-1} \circ \eta_{\mathcal D(f)}^I = U_{F^J}^f \circ \mathcal D(f)\eta^J \qquad\text{and}\qquad \varepsilon_{\mathcal C(f)}^I \circ F^I U^f = \mathcal C(f)\varepsilon^J \circ (F_{U^J}^f)^{-1} \end{gather}$$
This doesn’t look too much like the example in the introduction, but maybe some of this additional data is redundant. If we didn’t already know where we end up, one hint would be that |(F^f)^{-1} : F^I \circ \mathcal C(f) \to \mathcal D(f) \circ F^J| and |U^f : \mathcal D(f) \circ U^J \to U^I \circ \mathcal C(f)| look like mates. Indeed, it would be quite nice if they were as mates uniquely determine each other and this would make the reindexing give rise to a morphism of adjunctions. Unsurprisingly, this is the case.
To recall, generally, given adjunctions |F \dashv U : \mathcal C \to \mathcal D| and |F’ \dashv U’ : \mathcal C’ \to \mathcal D’|, a morphism of adjunctions from the former to the latter is a pair of functors |K : \mathcal C \to \mathcal C’| and |L : \mathcal D \to \mathcal D’|, and a natural transformation |\lambda : F’ \circ L \to K \circ F| or, equivalently, a natural transformation |\mu : L \circ U \to U’ \circ K|. You can show that there is a bijection |[\mathcal D,\mathcal C’](F’\circ L, K \circ F) \cong [\mathcal C, \mathcal D’](L \circ U, U’ \circ K)|. Concretely, |\mu = U’K\varepsilon \circ U’\lambda_U \circ \eta’_{LU}| provides the mapping in one direction. The mapping in the other direction is similar, and we can prove it is a bijection using the triangle equalities. |\lambda| and |\mu| are referred to as mates of each other.
In our case, |K| and |L| will be reindexing functors |\mathcal C(f)| and |\mathcal D(f)| respectively for some |f : I \to J|. We need to show that the family of adjunctions and the coherence conditions on |\eta| and |\varepsilon| force |(F^f)^{-1}| and |U^f| to be mates. The proof is as follows: $$\begin{align} & U^I \mathcal C(f) \varepsilon^J \circ U^I(F_{U^J}^f)^{-1} \circ \eta_{\mathcal D(f)U^J}^I & \qquad \{\text{coherence of }\eta \} \\ = \quad & U^I \mathcal C(f) \varepsilon^J \circ U_{F^JU^J}^f \circ \mathcal D(f)\eta_{U^J}^J & \qquad \{\text{naturality of }U^f \} \\ = \quad & U^f \circ \mathcal D(f)U^J\varepsilon^J \circ \mathcal D(f)\eta_{U^J}^J & \qquad \{\text{functoriality of }\mathcal D(f) \} \\ = \quad & U^f \circ \mathcal D(f)(U^J\varepsilon^J \circ \eta_{U^J}^J) & \qquad \{\text{triangle equality} \} \\ = \quad & U^f & \end{align}$$
The next natural question is: if we know |(F^f)^{-1}| and |U^f| are mates, do we still need the coherence conditions on |\eta| and |\varepsilon|? The answer is “no”. $$\begin{align} & U_{F^J}^f \circ \mathcal D(f)\eta^J & \qquad \{\text{mate of }U^f \} \\ = \quad & U^I \mathcal C(f) \varepsilon_{F^J}^J \circ U^I(F_{F^J}^f)^{-1} \circ \eta^I_{\mathcal D(f)U^I} \circ \mathcal D(f)\eta^J & \{\text{naturality of }\eta^I \} \\ = \quad & U^I \mathcal C(f) \varepsilon_{F^J}^J \circ U^I(F_{F^J}^f)^{-1} \circ U^I F^I D(f)\eta^J \circ \eta_{\mathcal D(f)}^I & \{\text{naturality of }U^I(F^f)^{-1} \} \\ = \quad & U^I \mathcal C(f) \varepsilon_{F^J}^J \circ U^I\mathcal C(f)F^J\eta^J \circ U^I (F^f)^{-1} \circ \eta_{\mathcal D(f)}^I & \{\text{functoriality of }U^I\mathcal C(f) \} \\ = \quad & U^I \mathcal C(f)(\varepsilon_{F^J}^J \circ F^J\eta^J) \circ U^I(F^f)^{-1} \circ \eta_{\mathcal D(f)}^I & \{\text{triangle equality} \} \\ = \quad & U^I (F^f)^{-1} \circ \eta_{\mathcal D(f)}^I & \end{align}$$ Similarly for the other coherence condition.
We’ve shown that if |U| is an indexed functor it has a left adjoint exactly when each |U^I| has a left adjoint, |F^I|, and for each |f : I \to J|, the mate of |U^f| with respect to those adjoints, which will be |(F^f)^{-1}|, is invertible. This latter condition is the Beck-Chevalley condition. As you can quickly verify, an invertible natural transformation doesn’t imply that its mate is invertible. Indeed, if |F| and |F’| are left adjoints and |\lambda : F’\circ L \to K \circ F| is invertible, then |\lambda^{-1} : K \circ F \to F’ \circ L| is not of the right form to have a mate (unless |F| and |F’| are also right adjoints and, particularly, an adjoint equivalence if we want to get an inverse to the mate of |\lambda|).
We’ve answered questions 1 and 2 from above, but 3 is still open, and we’ve generated a new question: what is the indexed functor whose left adjoint we’re finding? The family of reindexing functors isn’t indexed by objects of |\mathbf S| but, most obviously, by arrows of |\mathbf S|. To answer these questions, we’ll consider a more general notion of indexed (co)products.
A comprehension category is a functor |\mathcal P : \mathcal E \to \mathbf S^{\to}| (where |\mathbf S^{\to}| is the arrow category) such that |p = \mathsf{cod} \circ \mathcal P| is a (Grothendieck) fibration and |\mathcal P| takes (|p|-)cartesian arrows of |\mathcal E| to pullback squares in |\mathbf S^{\to}|. It won’t be necessary to know what a fibration is, as we’ll need only a few simple examples, but fibrations provide a different, and in many ways better, perspective1 on indexed categories and being able to move between the perspectives is valuable.
A comprehension category can also be presented as a natural transformation |\mathcal P : \{{-}\} \to p| where |\{{-}\}| is just another name for |\mathsf{dom} \circ \mathcal P|. This natural transformation induces an indexed functor |\langle\mathcal P\rangle : \mathcal C \circ p \to \mathcal C \circ \{{-}\}|2 where |\mathcal C| is an |\mathbf S|-indexed category. We have |\mathcal P|-(co)products when there is an indexed (left) right adjoint to this indexed functor.
One of the most important fibrations is the codomain fibration |\mathsf{cod} : \mathbf S^{\to} \to \mathbf S| which corresponds to |Id| as a comprehension category. However, |\mathsf{cod}| is only a fibration when |\mathbf S| has all pullbacks. In particular, the cartesian morphisms of |\mathbf S^{\to}| are the pullback squares. However, we can define the notion of cartesian morphism with respect to any functor; we only need |\mathbf S| to have pullbacks for |\mathsf{cod}| to be a fibration because a fibration requires you to have enough cartesian morphisms. However, given any functor |p : \mathcal E \to \mathbf S|, we have a subcategory |\mathsf{Cart}(p) \hookrightarrow \mathcal E| which consists of just the cartesian morphisms of |\mathcal E|. The composition |\mathsf{Cart}(p)\hookrightarrow \mathcal E \to \mathbf S| is always a fibration.
Thus, if we consider the category |\mathsf{Cart}(\mathsf{cod})|, this will consist of whatever pullback squares exist in |\mathbf S|. The inclusion |\mathsf{Cart}(\mathsf{cod}) \hookrightarrow \mathbf S^{\to}| gives us a comprehension category. Write |\vert\mathsf{cod}\vert| for that comprehension category. The definition in the introduction is now seen to be equivalent to having |\vert\mathsf{cod}\vert|-coproducts. That is, the indexed functor |\langle\vert\mathsf{cod}\vert\rangle| having an indexed left adjoint. The Beck-Chevalley condition is what is necessary to show that a family of left (or right) adjoints to (the components of) an indexed functor combine together into an indexed functor.
Specifically, the pullback square |f \circ h = g \circ k| is a morphism |(h, g) : k \to f| of |\mathsf{Cart}(\mathsf{cod})|. This makes |\langle\vert\mathsf{cod}\vert\rangle| an indexed functor with components |\langle\vert\mathsf{cod}\vert\rangle^k = k^* : \mathcal C^K \to \mathcal C^I|. The morphism |(h, g) : k \to f| induces the isomorphism |\langle\vert\mathsf{cod}\vert\rangle^{(h, g)} : h^* \circ f^* \cong k^* \circ g^*|. If |\Sigma^k \dashv k^* = \langle\vert\mathsf{cod}\vert\rangle^k| and similarly for |f|, then the “canonical morphism” is the mate of |\langle\vert\mathsf{cod}\vert\rangle^{(h, g)}|, namely |\Sigma^k \circ h^* \to g^* \circ \Sigma^f|. If this is invertible for every arrow of |\mathsf{Cart}(\mathsf{cod})|, then we can make the collection of left adjoints |\{\Sigma^f\}_{f \in \mathsf{Ob}(\mathsf{Cart}(\mathsf{cod}))}| into an indexed functor by defining |\Sigma^{(h,g)} : g^* \circ \Sigma^f \cong \Sigma^k \circ h^*| as the inverse of the mate of |\langle\vert\mathsf{cod}\vert\rangle^{(h, g)}|.
Indexed categories are, in some sense, a presentation of fibrations which are the more intrinsic notion. This means it is better to work out concepts with respect to fibrations and then see what this means for indexed categories rather than the other way around or even using the “natural” suggestions. This is why indexed categories are pseudofunctors rather than either strict or lax functors. For our purposes, we have an equivalence of 2-categories between the 2-category of |\mathbf S|-indexed categories and the 2-category of fibrations over |\mathbf S|. See Exercise 9.3.8 of Bart Jacobs’ Categorical Logic and Type Theory and for a formulation of |\mathcal P|-(co)products as a fibered adjunction.↩︎
This is just whiskering, |\mathcal C_{\mathcal P^{op}}|, but |\mathcal P^{op} : p^{op} \to \{{-}\}^{op}|.↩︎