nLab functor of descent type

Idea

A functor is of descent type if it satisfies “half” of the condition to be monadic.

Definition

A functor U:BAU:B\to A is of descent type (or is premonadic) if

  1. it has a left adjoint F:ABF:A\to B, and
  2. for all bBb\in B the canonical fork FUFUbFUϵϵFUFUbϵbF U F U b \underoverset{F U \epsilon}{\epsilon F U}{\rightrightarrows} F U b \xrightarrow{\epsilon} b is a coequalizer.

The second condition is equivalent to asking that the comparison functor BA UFB \to A^{U F} from BB to the Eilenberg-Moore category of the monad UFU F is fully faithful. When the comparison functor is essentially surjective (hence an equivalence of categories), UU is of effective descent type or monadic.

Examples

By monadic descent, a morphism ff in the base of a fibration is a descent morphism if and only if f *f^* is of descent type. This is presumably the origin of the terminology; ff is an effective descent morphism when f *f^* is monadic.

Last revised on November 3, 2023 at 13:24:10. See the history of this page for a list of all contributions to it.