Dear David, I think maybe the most relevant paper for this is: - Kelly, G. M., & Power, A. J. Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads. Journal of Pure and Applied Algebra, 1993(89), 163–179. which shows that "every finitary monad on a locally-finitely-presentable enriched category A admits a presentation in terms of basic operations and equations between derived operations, the arities here being the finitely-presentable objects of A." This is exactly the opposite of what you requested; you want to know that anything admitting a presentation gives a finitary monad. But Section 5 of op. cit. explains how to do the direction you want: you take a coequaliser of maps between free monads, and exploit the existence of "endomorphism monads". This is something that originated with Max Kelly, who used it a lot, going all the way back to SLNM420. It's not a general result, but this paper of Steve Lack: https://arxiv.org/pdf/math/0702535 works through (in Section 5) a bunch of examples of presenting monads in this style. All the best, Richard David Yetter <dyetter@ksu.edu> writes:
I'm hoping to avoid having to prove by hand that a particular category is monadic, by a finitary monad, over another.
It seems to me there should be a very general theorem that if one has an extension of essentially (many sorted) algebaric theories. then the category of models of the extension is monadic, by a finitary monad, over the category of models of the original theory.
I'd be happy with some restrictions on the extension: the same set of sorts, no new equations imposed on the operations in the original theory, just new operations and equations on these.
Does anyone have a citation for such a result? (Or one equivalent to it phrased in terms of sketches?) Such a result with additional hypotheses (which may or may not apply in my circumstance)? Or a result that obviously implies a result of the sort I want, but is stated in different terms?
Best Thoughts, D.Y.