If a monad in a 2-category admits a terminal resolution, does it admit an Eilenberg–Moore object? Let $T = (t, \mu, \eta)$ be a monad on an object $A$ of a 2-category $\mathcal K$. In The formal theory of monads, Street proves (Theorem 3) that if $l \dashv r$ is the canonical adjunction associated to an Eilenberg–Moore object, then $l \dashv r$ is terminal amongst adjunctions inducing $T$. Is there a reference or simple proof of the converse, i.e. that if $l \dashv r$ is terminal amongst adjunctions inducing $T$, then $r$ exhibits an Eilenberg–Moore object for the induced monad? Alternatively, is there a counterexample?

Presumably the following universal property is the key, but I don't see quite how the proof would go. An Eilenberg–Moore object for $T$ has the universal property that $\mathcal K[X, A^T] \cong \mathcal K[X, A]^{\mathcal K[X, T]}$ 2-natural in $X$ (Theorem 8). Consequently, an adjunction $l \dashv r$ is the canonical adjunction associated to an Eilenberg–Moore object (cf. Theorem 2) if and only if $\mathcal K[X, l] \dashv \mathcal K[X, r]$ is monadic in $\mathbf{Cat}$ in the usual sense (Corollary 8.1). Supposing that $l \dashv r$ is terminal, we wish to show that $\mathcal K[X, l] \dashv \mathcal K[X, r]$ is terminal. However, applying $\mathcal K[X, {-}]$ does not seem sufficient, since there may be adjunctions inducing $\mathcal K[X, T]$ that are not of the form $\mathcal K[X, l'] \dashv \mathcal K[X, r']$, in which case we cannot apply terminality of $l \dashv r$.
 A: I don't know the answer to the original question, but I don't think I'd be alone in arguing that the condition "there is an adjunction terminal among those inducing $T$" doesn't "feel" like "the right condition". Let me argue that you can massage this into a "nicer" condition which still expresses the universal property of the EM construction in terms of adjunctions:
Claim: Let $\mathcal K$ be a 2-category. Then $\mathcal K$ admits Eilenberg-Moore objects if and only if the forgetful functor $Adj(\mathcal K) \to Mnd(\mathcal K)$ has a right adjoint.
Here $Mnd(\mathcal K)$ is defined as usual, and $Adj(\mathcal K)$ is the 2-category of adjunctions in $\mathcal K$, where a 2-cell is a 2-cell between the right adjoints.
Proof: As you say, Street proves one direction, so we prove the other. We have forgetful 2-functors
$$ Mnd(\mathcal K) \leftarrow Adj(\mathcal K) \xleftarrow{const} \mathcal K $$
By hypothesis, the leftmost of these has a right adjoint. We wish to show that the composite (sending $K \in \mathcal K$ to the identity monad on $K$) has a right adjoint (this characterization of EM objects is of course also due to Street in the same paper). It will suffice to show that the rightmost 2-functor has a right adjoint. And it does -- the right adjoint sends $(L : C {}^\to_\leftarrow D : R) \mapsto D$.

Notes:

*

*If you think about the proof above, you'll see it also shows that this is true for a particular universal adjunction / EM object, even if these constructions aren't assumed to exist in general.


*(The funny thing here is that the diagram above doesn't seem to be induced in an obvious way by somehow "homming" some diagram into $\mathcal K$. At least $Mnd(\mathcal K)$ is the lax Gray internal hom $[[ Mnd, \mathcal K]]$ -- or equally the lax functor category $Fun^{lax}(1, \mathcal K)$ -- but I don't know how to construct $Adj(\mathcal K)$ except "by hand". As a result, the verifications in the above also need to be done "by hand". But it works out!)


*The condition that there be a terminal adjunctions inducing given monads $T$ says that the fiber of $Adj(\mathcal K) \to Mnd(\mathcal K)$ over $T$ has a terminal object. The condition that the right adjoint to $Adj(\mathcal K) \to Mnd(\mathcal K)$ exist is stronger in one sense. But it's also weaker, unless we have some way of knowing that this right adjoint should be fully faithful -- a question which Street's proof of the other direction of the Claim should shed some light on (er-- I suppose this follows representably from the fact that it's fully faithful in the case $\mathcal K = Cat$).
