Last night I finally wrapped my head around a definition of fibration which has been confusing me for a while. I thought I'd know how it worked until I didn't, only to realize my confusion stemmed from the fact I was looking at two subtly different definitions which are nonetheless equivalent. This made me angry enough to write a post.
A (cloven Grothendieck) fibration, or fibered category, is a functor \( p: \cal E \to C \) equipped with a structure called a cleavage, which amounts to say that when we look at the way the fibers of \( p \) (which are the categories \( p^{-1}X \) for \( X: \cal C \)) are acted upon (or reindexed) by the morphisms of \( \cal C \), they behave basically as nicely as you can ask.
In fact, in general, a morphism \( f:X \to Y \) in \( \cal C \) induces a mere profunctor \( p^{-1}f : p^{-1}X \)⇸\( p^{-1}Y \) between the fibers of its ends. Such a profunctor takes an object \( X' \) over \( X \) and an object \( Y' \) over \( Y \) and returns the set of maps \( f' : X' \to Y' \) in \( \cal E \) over \( f \). Here 'over' means 'mapped by \( p \) to'. Moreover, when you put together these profunctors, you realize they don't even compose nicely: they organize in a (unitary) lax functor \( p^{-1} : \cal C \to \bf Prof \). This story is told here, and with some more detail in the references given there.
So a fibration is a functor for which reindexing is much better behaved: it is functorial and respects composition up to coherent iso! In other words, taking fibers is now a pseudofunctor \( p^{-1} : \cal C \to \bf Cat \). The structure of a cleavage is thus the data one needs to prove this, which can be more or less effective depending on your taste towards constructiveness.
Usually one gives a cleavage by proving every morphism \( f:X \to Y \) in \( \cal C \) has a so-called cartesian lift (a name which is very bad until you realize is very good). A lift of \( f \) would be a morphism \( f':X' \to Y' \) in \( \cal E \) such that \( p(f') = f \). A cartesian lift is a lift enjoying a universal property, thus making it 'the best lift' according to some criterion.
When you unpack this universal property, it can be rather unwieldy. It feels like a drunk version of the universal property of a pullback. Here's the relevant diagram:
So you start with a morphism \( f \) in \( \cal C \) like above, and you fix a \( Y' : \cal E \) to lift to. This is sort of an anchor, think of it as the right leg of a pullback. This is the data in black in the diagram. Now the cartesian lift is the red morphism \( f_{Y'} : f^*Y' \to Y' \). Here \( f^*Y' \) is just notation for 'an object we obtained by reindexing \( Y' \) along \( f \)'. Its universal property is expressed against the blue data, which consists of another morphism \( h:Z \to Y' \) into \( Y' \) and a morphism \( k: p(Z) \to X \) chosen as to factor \( p(h) \) through \( f \) (hopefully you notice the slightly different shades of blue). Then \( f_{Y'} \) is cartesian iff there exists a unique morphism \( \langle h, k \rangle : Z \to f^*Y' \) in \( \cal E \) that (1) factors \( h \) through \( f_{Y'} \) and (2) is over \( k \), i.e. \( p\langle h,k \rangle = k \).
Ugh, what a ride!
It's not easy to wrap one's head around this universal property the first time one encounters it. In my opinion, it is better given in other ways, and funnily enough, it is not the original definition of Grothendieck fibration (given in SGA by, you guessed it, Grothendieck). The original one is given in terms of weak cartesian morphisms (the modern terminology 'cartesian morphism' denotes what Grothendieck called 'strong cartesian morphism'), which satisfy a more intuitive universal property plus the requirement to compose up to coherent isomorphisms. This weaker universal property is then seen, quite straightforwardly actually, to correspond to the fact reindexing can be expressed by representable profunctors, aka functors, while the second requirement makes reindexing pseudofunctorial.
If you don't fancy reading SGA, I found John Gray gave a detailed, well-written and English exposition of the same material in the first sections of his paper Fibred and cofibred categories (a paper which, regrettably, is freely available on SciHub). This is even more remarkable when you realize Gray's paper is from 1965, just a few years after SGA was published, and the exposition of so many category theory papers from back then hasn't aged that well.
Apart from the fact Gray did a great job already in explaining Grothendieck's original definition of fibration, I'm not lingering on it mainly because I want to talk about another, slicker way to define fibrations, due to Chevalley.
As I anticipated these are actually two subtly different ways. Their main advantage is to be applicable to define fibrations in any cartesian 2-category \( \cal K \). But for now, let's stick to \( \bf Cat \).
The definition goes like this: \( p:\cal E \to C \) is a fibration iff you can exhibit the right adjoint dashed in the following commutative diagram:
This might look a bit confusing at first, but I promise it's actually very intuitive once we introduce all the characters.
On the right, \( C/p \) is a comma category, or the slice of \( C \) over \( p \). Hence its objects are pairs of an object \( Y': E \) and an arrow \( f:X \to p(Y') \) of \( C \), and its morphisms are exactly what you expect (the data here is \( h \) and \( k \), and the commutativity of the square is a condition):
The functor \( u \) out of \( C/p \) forgets about the data of an object in \( E \), and only remembers the arrow.
On the left, we have \( p^\downarrow : \cal E^\downarrow \to C^\downarrow \), the functor \( p \) 'on arrows'. It takes an arrow in \( \cal E \) and sends it to an arrow in \( \cal C \), using \( p \), and does the same for squares.
Finally, on top we have basically the same functor as \( p^\downarrow \): it sends an arrow of \( \cal E \) to the pair of its codomain and the arrow of \( \cal C \) obtained by applying \( p \) to it:
Now, what does a functor \( \ell : {\cal C}/p \to \cal E^\downarrow \) do? When you think about it, it gives explicit lifts. Indeed, objects of \( {\cal C}/p \) are 'lifting problems': arrows in \( \cal C \) with a specified object of \( \cal E \) over its codomain. Then a lift would send such a thing to an arrow of \( \cal E \), and since \( \ell \) has to make the triangle over \( \cal C^\downarrow \) commute, we know that it must send \( f \) to a morphism over it, thus a lift!
Asking for \( \ell \) to be right adjoint to what is, in practice, \( p \) on morphisms, assures its choice of lifts is cartesian. In fact, we are going to prove it amounts to giving to the lifts the universal property explained above.
Suppose the adjunction is given by a natural isomorphism \( {\cal E}^\downarrow (h_1, \ell (f)) \cong {\cal C}/p(p(h_1), f) \) (pardon the weird name for \( h_1 \), you'll see in a moment why I've chosen that). In one direction, is very simple (\( {\cal E}^\downarrow \) on the left, \( {\cal C}/p \) on the right):
In the other direction, we can read the universal property of \( \ell (f) \) as cartesian lift of \( f \):
The existence and uniqueness of \( \langle h_1 ; h_2, k \rangle \) (whose name is, so far, just notation) are consequences of stating that the two mappings just exhibited are inverse to each other. Why is this the same \( \langle h_1 ; h_2, k \rangle \) we've seen in stating the universal property of cartesian lift? Well, if you put \( h = h_1 ; h_2 \), then we are saying that for all morphisms \( h:Z' \to Y' \) and \( k \) (such that \( p(h) = k ; f \)) there exists a unique \( \langle h, k \rangle \) that factors \( h \) through \( \ell f \).
Ta-dah!
While the counit of this adjunction is boring (since \( p(\ell (f)) = f \)), the unit is quite interesting: it takes a map \( f' \) in \( \cal E^\downarrow \) and gives us a square \( f' \to \ell (p(f')) \), obtained as the mate of the identity of \( p(f') \):
Observe that on the left we actually have a triangle, whose 'long side' is \( f' \), and whose short side exhibit a factorization in \( \ell (p(f)) \) and \( \eta _{f'} \). By construction, these are, respectively, a cartesian map (i.e. a map obtained by lifting something from \( \cal C \)) and a vertical map (i.e. a map over an identity). So the unit of this adjunction provides the vertical part in the vertical-cartesian factorization system we have on \( \cal E \)! This factorization system is really useful, and you can read more about it here.
Now the reason for my confusion is that if you look at classical sources, like the nLab or Street's Fibrations in bicategories, they would tell you \( p:\cal E \to C \) is a fibration iff you can exhibit the right adjoint dashed in the following commutative diagram:
And this diagram looks so similar to the aforementioned one I've never really bothered with it. Only after I end up very confused I realized the two are different definitions! Notice, in fact, that on the left side of the above diagram appears \( p \), not \( p^\downarrow \)!
So how come two definitions which are so close to each other both give us the same answer?
The reason is we can recover one from the other by composing the incriminated adjunctions with the mother of all adjunctions, \( \rm cod \dashv id \dashv dom : \cal E \to E^\downarrow \). For instance, one gets the second definition from the first by doing:
This is saying that \( \ell \), in the second definition, maps a morphism \( f:X \to p(Y') \) to the domain of its cartesian lift.
Dually, we can get the first one from the second:
To see how this works, one first has to convince oneself that the second definition I gave you works. The trick is, despite the fact \( \ell \) only gives us the domain of the (alleged) cartesian lift, its action on morphisms can be used to obtain the entire cartesian lift. See here for a proof that this is sufficient (in the slightly more general case of Street fibrations).
This latter definition might feel less intuitive but has the benefit of being a bit simpler to state (no \( p^\downarrow \) involved) and to use in abstract.
For instance, here's another way to see the fibrations induce a factorization system on their total category \( \cal E \) using this latter definition. For similar reasons as before, the counit of \( \langle 1, p \rangle \dashv \ell \) is trivial, which means \( p \) is fully faithful. Since \( \ell \) also has a left adjoint, it exhibits \( {\cal C}/p \) as a reflective subcategory of \( \cal E \), and thus induces a factorization system on it. If you look at the way this happens, you quickly realize this is indeed the vertical-cartesian factorization system on \( \cal E \). Brilliant!
The true power of this definition, however, is that it exhibits fibrations, as the algebras of a colax idempotent 2-monad. This has many nice consequences, the most immediate being fibrational structure is property-like, meaning there's at most one (up to equivalence) way for a given functor to be a fibration.
That's a great, great piece of category theory which deserves a better exposition than what I can do now before going to lunch, so let's leave for next time! If you're hungry for answers though, the story is sketched on the nLab and in full in Street's Fibrations in bicategories (beware, this latter paper is not for the squeamish).