The Bénabou-Roubaud monadic descent theorem via string diagrams
Résumé
One of the essential points concerning Grothendieck's original approach to descent theory consists of identifying the class of effective descent morphisms for a given fibration. In the special case of a bifibration satisfying Beck-Chevalley condition, Bénabou and Roubaud have given such a characterization by means of monadicity: a morphism is an effective descent morphism precisely when its induced pullback functor is monadic.
Typically presented as a commuting diagram (or in some cases even as a table which lists all the relevant morphisms), Grothendieck's cocycle condition laid out in this manner imposes technically complicated calculations and disguises its purpose in the descent data. Consequently, the categorical equivalence which reflects the comparison of the descent in fibered categories with monadic descent is usually not worked out in complete detail in the literature. Our aim is to tell the (complete!) Bénabou-Roubaud story in the language of string diagrams. Indeed, we notice that this proof essentially deals with constructing natural transformations and rewriting them (the latter requiring an alert bookkeeping action), i.e. that it (presumably) constitutes a suitable environment to make the most of the string diagrammatic approach (primarily of its ``free'' bookkeeping virtue).
We will link the monadic and the original viewpoint via another possible definition of the category of descent data. This intermediate step, due to Janelidze and Tholen, involves constructions in internal categories and it provides an interesting illustration on how can one stay in the world of string diagrams even when dealing with morphisms which do not have an explicit string diagram definition. We start by representing Grothendieck's cocycle condition in the special case of the basic fibration of a category, and we ultimately show how should our arguments be ``lifted'' in order to derive the proof for the general case of an arbitrary bibration.