A paper relevant to this is the following: E. J. Dubuc, M. kelly, A presentation of Topoi as Algebraic relative to Categories or Graphs, Journal of Algebra, Vol 81-2, (1983) greetings e.d. On 19/10/2025 20:29, Richard Garner wrote:

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.

You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files<https://outlook.office365.com/mail/deeplink/groupActions?source=EscalatedMessage&action=files&smtp=categories%40mq.edu.au&bO=true&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Leave group<https://outlook.office365.com/mail/deeplink/groupActions?source=EscalatedMessage&action=leave&smtp=categories%40mq.edu.au&bO=true&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>

For negative examples and discussion, see chapter 23 of http://katmat.math.uni-bremen.de/acc/acc.pdf Am 20.10.25 um 06:58 schrieb Michael Shulman: Unless I'm confused, I don't think this is true, not if you really meant (as you said) *essentially* algebraic theories. If it were, then for any essentially algebraic theory T, you could form the theory T0 with the same sorts and no equations, so that T is an extension of T0 in your sense. But the category of T0-models is just a power of Set, and the category of models of the essentially algebraic theory T is not usually monadic over a power of Set. For instance, if T is the two-sorted essentially algebraic theory of categories, then T0-Mod is Set x Set, and Cat is not monadic over Set x Set. On Sun, Oct 19, 2025 at 2:53 PM David Yetter <dyetter@ksu.edu<mailto:dyetter@ksu.edu>> wrote: 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. You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files | Leave group | Learn more about Microsoft 365 Groups You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files<https://outlook.office365.com/mail/deeplink/groupActions?source=EscalatedMessage&action=files&smtp=categories%40mq.edu.au&bO=true&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Leave group<https://outlook.office365.com/mail/deeplink/groupActions?source=EscalatedMessage&action=leave&smtp=categories%40mq.edu.au&bO=true&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>

While not exactly a syntactic version of the condition as Simon stated it, the notion of "dependently typed algebraic theory", introduced in Chaitanya Leena Subramaniam's thesis "From dependent type theory to higher algebraic structures" (https://arxiv.org/abs/2110.02804), can be used to address these issues in many naturally-occurring situations. In place of the *set* of sorts of an Essentially Algebraic Theory, a DTAT has a *direct category* of sorts, whose morphisms represent "dependency" relations between sorts such as the dependency of arrows on objects in a category. The operations and axioms are formulated syntactically using dependent type theory built on these sorts with these dependencies, and thus their domains are restricted to those definable from the dependency relations only. Thus a DTAT can be regarded as a special kind of EAT (more specifically, a special kind of Generalized Algebraic Theory). But the restriction ensures that the category of models of the DTAT is finitary monadic over the category of presheaves on its direct category of sorts. Indeed, just as Lawvere theories are *equivalent* to finitary monads on Set (or on a power of Set, in the multi-sorted case), DTATs are equivalent to finitary monads on categories of presheaves on direct categories. Moreover, every EAT can be presented by *some* DTAT. In particular, therefore, if we have an extension T -> T' of DTATs that have the same underlying direct category of sorts C, then Mod(T) and Mod(T') are both finitary monadic over Psh(C). So it follows by the "cancellation lemma" for monadic functors that Mod(T') -> Mod(T) is also finitary monadic. For example, monoidal categories are monadic over categories, since both are monadic over quivers. This doesn't encompass all the situations described by Simon's condition, e.g. given a DTAT T with sorts C, there could be an extension of EATs T -> T' such that the domains of the operations and axioms of T' are definable in T but not in C, so that T' would not be presentable by a DTAT with sorts C, but nevertheless Simon's condition would apply. However, I think it does include many cases arising in practice, and it has the advantage of using the convenient syntax of dependent type theory. On Mon, Oct 20, 2025 at 12:14 PM henry <henry@phare.normalesup.org<mailto:henry@phare.normalesup.org>> wrote: If I'm remembering well, The correct criterion, in the context of quasi-equational theories (I.e. algebraic theory with partially defined operations), is that given an extension T' of T, then the forgetful functor from Mod(T') to Mod(T) is monadic if and only if T' can be axiomatized (as an extention of T) in a way so that: - T' has the same sorts as T. - All the new terms and terms equations are written in domain (/context) that are definable in T. There are no problems with having equation between terms of T (it will just mean that your monad is not faithful) For example, if you consider the theory of categories written as a single sorted quasi-equational theories, the composition operation is defined in context "f,g,t(f) = s(g)" and the associativity axiom is written in context "f,g,h,t(f)=s(g),t(g)=s(h)", these are definable in the theory T of "reflexive graphs" (the subtheory with only the operation s and t and corresponding equation), but not in the theory of sets. So the criterion show that categories are monadic over reflexive graph but does not show that cat are monadic over set. (it unfortunately doesn't quite show that they are not though as there could be a different axiomatization of cat...) I could be wrong, but I don't think a syntactic version of a criterion like this appears in the litterature, I however remember an old, short paper in french of Christian Lair that showed a version of this in the language of sketches, but I've spent the last hour and a half trying to find this paper, unsuccessfully. So if anyone know which paper I'm talking about please let tel me! In any case, it is not too hard to prove, especially the fact that this is a sufficient condition for monadicity (which is what we mostly care about). It can probably be obtained using Beck criterion (that's what Lair was doing in my memory), but the simplest proof I know rellies on Bourke and Garner theory of "Nervous monads" (Monads and theories in AiM https://www.sciencedirect.com/science/article/pii/S0001870819302580). The key idea being that contexts in T corresponds to finitely presented models of T and adding terms and equations to T in such context can be described as taking colimits of Garner and Bourke's basic operations monads. Bests, Simon Le 2025-10-19 17:50, David Yetter a écrit :

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.

You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message.

View group files [1] | Leave group [2] | Learn more about Microsoft 365 Groups [3]

Links: ------ [1] https://outlook.office365.com/mail/deeplink/groupActions?source=EscalatedMes... [2] https://outlook.office365.com/mail/deeplink/groupActions?source=EscalatedMes... [3] https://aka.ms/o365g

You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files<https://outlook.office365.com/groups/groupsubscription?source=EscalatedMessage&action=files&smtp=categories%40mq.edu.au&bO=true&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Leave group<https://outlook.office365.com/groups/groupsubscription?source=EscalatedMessage&action=leave&smtp=categories%40mq.edu.au&bO=true&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>