mathlib3 documentation

category_theory.monad.monadicity

Monadicity theorems #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

@[protected, instance]

The "main pair" for an algebra (A, α) is the pair of morphisms (F α, ε_FA). It is always a reflexive pair, and will be used to construct the left adjoint to the comparison functor and show it is an equivalence.

@[protected, instance]

The "main pair" for an algebra (A, α) is the pair of morphisms (F α, ε_FA). It is always a G-split pair, and will be used to construct the left adjoint to the comparison functor and show it is an equivalence.

We have a bijection of homsets which will be used to construct the left adjoint to the comparison functor.

Equations

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 monadic_of_creates_G_split_coequalizers.

Equations

To show G is a monadic right adjoint, we can show it preserves and reflects G-split coequalizers, and C has them.

Equations

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 creates_G_split_of_monadic.

Equations

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.

Equations

Reflexive (crude) monadicity theorem. If G has a right adjoint, D has and G preserves reflexive coequalizers and G reflects isomorphisms, then G is monadic.

Equations