The theorem (Bénabou-Roubaud 70) identifies the Eilenberg-Moore category of algebras over the monad induced from a base change adjoint triple for some bifibration satisfying the Beck-Chevalley condition with the category of descent data along this morphism. This is the basis for the monadic reformulation of descent theory: monadic descent.
A functor is a Grothendieck opfibration if is a Grothendieck fibration, and a functor is a bifibration if is both a Grothendieck opfibration and fibration (no additional compatibility asked!). Thus we can talk about cartesian and cocartesian arrows in .
In a bifibered category, automatically for any morphism in the base, the “inverse image” (or “pullback” or “restriction”) functor is right adjoint to the “pushforward” functor ; with unit and counit .
(Note that in topos theory and algebraic geometry, functors called “inverse images” usually have right adjoints . This situation can be reconciled with the setup of bifibrations either by taking fiberwise opposites, so that left and right adjoints are switched, or by taking opposites of both the base and total categories, so that the direct and inverse images are switched. However, there are also many bifibrations arising in other contexts in which has both a left adjoint and a right adjoint , although the latter cannot then be described cleanly in fibrational terms.)
The adjunction generates a monad in the usual way: the functor is , the multiplication is , and the unit is just the unit of the adjunction. Denote by the Eilenberg–Moore category of modules (algebras) over the monad , with canonical forgetful functor and canonical comparison functor .
in such that its image in is a pullback square, if and are cartesian and is cocartesian then is cocartesian.
An equivalent way to state the condition is that for any pullback square
in , the canonical transformation is an isomorphism. In the Bénabou–Roubaud paper this is called the Chevalley property and said to make into a Chevalley functor.
Denote by the pullback of along itself, with the canonical projections . Now consider the lift of the cartesian square defining to in such a way that is lifted to a cartesian arrow, to a cocartesian arrow, and to a cocartesian arrow. Then by the universality there is a lift of completing the square, and by the Beck–Chevalley property it is cartesian. Together with the isomorphism given by adjunction this gives a morphism
One checks that an invertible morphism satisfies the cocycle equation (making it into a descent datum) iff is an action of on , and similarly for the unitality axiom.
Denote by the category of descent data for the fibration along the morphism ; it comes with canonical functors
The Bénabou–Roubaud theorem asserts that this induces an equivalence of categories between and .
In addition, this equivalence satisfies some naturality properties, including that it commutes appropriately with the canonical functors to the fibers and . Combining this theorem with Beck’s monadicity theorem, it becomes a practical tool for establishing a descent property in bifibrations, with variants in some other setups (to be covered later).
There are several characterizations of a Beck-Chevalley property for bifibrations:
(Duško Pavlović, in Category theory Como 1990, LNM 1488, Springer 1991)
Let be a bifibration, a square in such that , and a square in such that , with , , and . The following conditions are equivalent:
a) if and are cartesian and if is cocartesian then must be cocartesian;
b) if and are cocartesian and if is cartesian then must be cartesian;
c) if is cartesian and if is cocartesian then is cartesian iff is cocartesian.
If some inverse image functors and and some direct image functors and are chosen, then every square over satisfies conditions (a-c) iff there is a canonical natural isomorphism
X. Guo, thesis, p. 58 of Monadicity, purity and descent equivalence, [pdf] (http://www.collectionscanada.gc.ca/obj/s4/f2/dsk2/ftp02/NQ59136.pdf)
There has been some historical discussion on this in the category list; Zoran’s response is here.