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://url.au.m.mimecastprotect.com/s/zqN8C91W8rCkv6xlvIofDuq_ghm?domain=sc.... 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://url.au.m.mimecastprotect.com/s/MDQCC0YKgRsGK947KhDhJu9X0DW?domain=ou... [2] https://url.au.m.mimecastprotect.com/s/3sEWCgZ05JfArjNoru2ipu4jaZP?domain=ou... [3] https://url.au.m.mimecastprotect.com/s/MjfXCjZ12Rfn2wAB2u7sVumY8qv?domain=ak...