A functor is monadic if it looks like the forgetful functor from a category of algebras over a monad.
The monadicity theorem characterizes monadic functors.
Given a pair of adjoint functors , , with unit and counit , one constructs a monad setting , .
Consider the Eilenberg–Moore category of -algebras (-modules) in . Clearly is a -action. In fact there is a canonical comparison functor given on objects by . We then say that we have a monadic adjunction.
A functor is monadic (resp. strictly monadic) if it has a left adjoint and the comparison functor is an equivalence of categories (resp. an isomorphism of categories). In other words, up to equivalence, monadic functors are precisely the forgetful functors defined on Eilenberg–Moore categories for monads, and strictly monadic functors are the same as these forgetful functors up to isomorphism. A category is monadic over a category if there is a functor which is monadic.
Various versions of Beck’s monadicity theorem (old-fashioned name of some schools: tripleability theorem) give sufficient, and sometimes necessary, conditions for a given functor to be monadic. There are also dual, comonadic versions.
A monadic functor is strictly monadic if and only if it is also an amnestic isofibration: clearly, a strictly monadic functor is an amnestic isofibration; and if a monadic functor is amnestic, then the comparison functor is also amnestic, and if is a monadic isofibration, so is ; therefore in this case must be an isomorphism of categories.