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>