Fix a category $B$ with pullbacks. The category of bifibrations over $B$ satisfying the Beck-Chevalley condition appears to be monadic over $\mathsf{Cat}/B$. Is this discussed somewhere in the literature?

Let $\mathsf{Fib}(B)$ be the category of fibrations and Cartesian functors over $B$. It's well-known that the forgetful functor $\mathsf{Fib}(B) \to \mathsf{Cat}/B$ is monadic; the induced monad $T$ is given by a comma category construction $T: (E \overset{p}{\to} B) \mapsto (B \downarrow p \to B)$. In fact, this monad is colax-idempotent. Dually, the monad $S: (E \overset{p}{\to} B) \mapsto (B \downarrow p \to B)$ is lax-idempotent, with algebras $\mathsf{OpFib}(B)$ given by opfibrations.

Thus far we have required no hypotheses on $B$. Now if $B$ has pullbacks, there appears to be (I have not checked all the coherence conditions) a (pseudo-)distributive law $TS \Rightarrow ST$ which takes a diagram $p(e) \to b \leftarrow b'$ to its pullback. And it looks like an algebra for the composite monad $ST$ is a bifibration (a functor which is simultaneously a fibration and an opfibration) satisfying the Beck-Chevalley condition over all pullback squares.

(Dually, if $B$ has pushouts, then there will be another distributive law in the other direction whose algebras will be bifibrations satisfying a dual Beck-Chevalley condition over pushout squares, but I've never heard of such a thing in nature.)

Not only does it seem good to know that the Beck-Chevalley condition arises from a monad, but this seems like a really cool example of a pseudo-distributive law! In general, it seems like these are a pain to work with because of the number of coherence conditions (even with the simplifications afforded by the (co)lax idempotency). Maybe that's why I've never heard of this one. But pullbacks can be strictified -- perhaps the pseudodistributive law can also be strictified?


Yes, this pseudo-distributive law and the characterization of its algebras as bifibrations appear in section 1.5 of Tamara von Glehn's thesis.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.