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.
Introduction
When one talks about “indexed (co)products” in an indexed category, it is often described as follows:
Let be an -indexed category,
i.e. a pseudofunctor
where is an ordinary category.
Write for and for
where . The functors will be called reindexing functors. has -indexed
coproducts whenever
each reindexing functor has a left adjoint , and
the Beck-Chevalley condition holds, i.e. whenever is a pullback square in , then the canonical
morphism is an isomorphism.
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:
Where does the Beck-Chevalley condition come from?
What is this “canonical morphism”?
Why do we care about pullback squares in particular?
Indexed Functors and Indexed Natural Transformations
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 , an indexed
functor consists of a functor for
each object of and a natural isomorphism
for each in .
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 of , we have a natural transformation
such that for each the following diagram commutes where the isomorphisms are the isomorphisms from the pseudonaturality of and .
Indexed Adjunctions and Beck-Chevalley
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 , 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
and such that in an indexed sense. That means we have
and as indexed natural transformations. The first pieces of additional
data, then, are the fact that and are indexed functors, so we have natural
isomorphisms
and for each in .
The next pieces of additional data, or rather constraints, are the coherence conditions on and .
These work out to
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
and 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 and , a
morphism of adjunctions from the former to the latter is a pair of functors
and , and a natural transformation or,
equivalently, a natural transformation . You can show that there is a
bijection .
Concretely, 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.
and are referred to as mates of each other.
In our case, and will be reindexing functors and respectively for
some . We need to show that the family of adjunctions and the coherence conditions on and
force and to be mates. The proof is as follows:
The next natural question is: if we know and are mates, do we still need the coherence conditions on
and ? The answer is “no”. Similarly for the other coherence condition.
We’ve shown that if is an indexed functor it has a left adjoint exactly when each has a left adjoint, , and
for each , the mate of with respect to those adjoints, which will be , 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 and are left adjoints and is invertible,
then is not of the right form to have a mate (unless and are also right
adjoints and, particularly, an adjoint equivalence if we want to get an inverse to the mate of ).
Comprehension Categories
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
but, most obviously, by arrows of . To answer these questions, we’ll consider a more general notion of
indexed (co)products.
A comprehension category
is a functor (where
is the arrow category)
such that is a (Grothendieck) fibration
and takes (-)cartesian arrows of to pullback
squares in . 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 where is
just another name for . This natural transformation induces an indexed
functor 2
where is an -indexed category. We have -(co)products
when there is an indexed (left) right adjoint to this indexed functor.
One of the most important fibrations is the codomain fibration which
corresponds to as a comprehension category. However, is only a fibration when has
all pullbacks. In particular, the cartesian morphisms of are the pullback squares. However, we
can define the notion of cartesian morphism with respect to any
functor; we only need to have pullbacks for to be a fibration because a fibration requires
you to have enough cartesian morphisms. However, given any functor , we
have a subcategory which consists of just the cartesian morphisms of .
The composition is always a fibration.
Conclusion
Thus, if we consider the category , this will consist of whatever pullback squares
exist in . The inclusion gives us
a comprehension category. Write for that comprehension category. The definition in the
introduction is now seen to be equivalent to having -coproducts. That is, the indexed
functor 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 is a morphism
of . This makes
an indexed functor with components .
The morphism induces the isomorphism
.
If and similarly for , then
the “canonical morphism” is the mate of ,
namely . If this is invertible for every
arrow of , then we can make the collection of left adjoints
into an indexed functor
by defining as the inverse
of the mate of .
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 -indexed categories and the 2-category of
fibrations over . See Exercise 9.3.8 of Bart Jacobs’ Categorical Logic and Type Theory
and for a formulation of -(co)products as a fibered adjunction.↩︎