Documentation

Mathlib.CategoryTheory.Monad.Monadicity

Monadicity theorems #

We prove monadicity theorems which can establish a given functor is monadic. In particular, we show three versions of Beck's monadicity theorem, and the reflexive (crude) monadicity theorem:

G is a monadic right adjoint if it has a right adjoint, and:

Tags #

Beck, monadicity, descent

TODO #

Dualise to show comonadicity theorems.

If G is monadic, it creates colimits of G-split pairs. This is the "boring" direction of Beck's monadicity theorem, the converse is given in monadicOfCreatesGSplitCoequalizers.

Instances For

    Beck's monadicity theorem. If G has a right adjoint and creates coequalizers of G-split pairs, then it is monadic. This is the converse of createsGSplitOfMonadic.

    Instances For

      An alternate version of Beck's monadicity theorem. If G reflects isomorphisms, preserves coequalizers of G-split pairs and C has coequalizers of G-split pairs, then it is monadic.

      Instances For