Two-dimensional monadicity (Q2445311)

Monads are good for general theory of algebraic structures, but particular monads are often hard to describe explicitly. However, if we know the category of algebras for a desired monad, we can use a monadicity theorem to verify that the monad exists. In 2-monad theory, there are multiple kinds of morphisms between algebras -- strict, pseudo, lax, or colax -- but until now, essentially the only way to identify these morphisms for a particular 2-monad has been to use an explicit presentation of it. The present paper remedies this problem by extending the monadicity theorem to deal with these more general morphisms. That is, if we can guess what the pseudo, lax, or colax morphisms should be (which is often easy) we can use the ``2-dimensional monadicity theorem'' to verify our guess. The 2-dimensional monadicity theorem is formulated in the language of \(\mathcal{F}\)-categories, introduced by \textit{S. Lack} and the reviewer [Adv. Math. 229, No. 1, 294--356 (2012; Zbl 1236.18006)]. An \(\mathcal{F}\)-category is an enhancement of a 2-category that includes two different kinds of morphisms between its objects, such as the strict and lax morphisms between algebras for a 2-monad. The 2-dimensional monadicity theorem gives conditions on an \(\mathcal{F}\)-functor ensuring that it is the forgetful functor \(T\text{-}\mathrm{Alg}_\ell \to \mathcal{K}\) from the \(\mathcal{F}\)-category of strict and lax morphisms for a 2-monad (and similarly for the pseudo and colax cases). The form of these conditions is of independent interest. First of all, there is ordinary monadicity of the strict morphisms. Then there is the existence of certain \(\mathcal{F}\)-categorical limits, which are known to exist in \(T\text{-}\mathrm{Alg}_\ell\) [\textit{S. Lack}, Appl. Categ. Struct. 13, No. 3, 189--203 (2005; Zbl 1099.18004)] -- the characterization of all the limits that exist in such categories was the reason for the later introduction of \(\mathcal{F}\)-categories. Finally, there is a lifting property for certain adjunctions, which is also known to hold for \(T\text{-}\mathrm{Alg}_\ell\) [\textit{G. M. Kelly}, Lect. Notes Math. 420, 257--280 (1974; Zbl 0334.18004)]. The theorem then says that an \(\mathcal{F}\)-category satisfying these conditions is the factorization of the forgetful functor \(T\text{-}\mathrm{Alg}_s \to \mathcal{K}\) according to a particular orthogonal factorization system on \(\mathcal{F}\)-categories. In particular, this ensures its uniqueness, which yields the 2-dimensional monadicity theorem, but it also suggests that factorizations with these properties may provide a good notion of ``lax morphism'' even in non-monadic contexts.