categories - Category Theory list
 help / color / mirror / Atom feed
* Monadicity of extensions of essentially algebraic theories
@ 2025-10-19 21:50 David Yetter
  2025-10-20  0:29 ` Richard Garner
                   ` (2 more replies)
  0 siblings, 3 replies; 8+ messages in thread
From: David Yetter @ 2025-10-19 21:50 UTC (permalink / raw)
  To: Categories List

[-- Attachment #1: Type: text/plain, Size: 1537 bytes --]

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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Leave group<https://outlook.office365.com/mail/deeplink/groupActions?source=EscalatedMessage&action=leave&smtp=categories%40mq.edu.au&bO=true&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Learn more about Microsoft 365 Groups<https://aka.ms/o365g>


[-- Attachment #2: Type: text/html, Size: 5675 bytes --]

^ permalink raw reply	[flat|nested] 8+ messages in thread

* Re: Monadicity of extensions of essentially algebraic theories
  2025-10-19 21:50 Monadicity of extensions of essentially algebraic theories David Yetter
@ 2025-10-20  0:29 ` Richard Garner
  2025-10-20 13:40   ` Ivan Di Liberti
  2025-10-20 20:24   ` Eduardo J. Dubuc
  2025-10-20  4:58 ` Michael Shulman
  2025-10-20 12:47 ` henry
  2 siblings, 2 replies; 8+ messages in thread
From: Richard Garner @ 2025-10-20  0:29 UTC (permalink / raw)
  To: David Yetter; +Cc: Categories List


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.


^ permalink raw reply	[flat|nested] 8+ messages in thread

* Re: Monadicity of extensions of essentially algebraic theories
  2025-10-19 21:50 Monadicity of extensions of essentially algebraic theories David Yetter
  2025-10-20  0:29 ` Richard Garner
@ 2025-10-20  4:58 ` Michael Shulman
  2025-10-20  7:36   ` Till Mossakowski
  2025-10-20 12:47 ` henry
  2 siblings, 1 reply; 8+ messages in thread
From: Michael Shulman @ 2025-10-20  4:58 UTC (permalink / raw)
  To: David Yetter; +Cc: Categories List

[-- Attachment #1: Type: text/plain, Size: 2786 bytes --]

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<https://url.au.m.mimecastprotect.com/s/V-y_C5QP8ySZoK222CzfOukXK4-?domain=outlook.office365.com>   |   Leave group<https://url.au.m.mimecastprotect.com/s/qmSKC6XQ68frE9qqqf6h4u5jrjv?domain=outlook.office365.com>   |   Learn more about Microsoft 365 Groups<https://url.au.m.mimecastprotect.com/s/3_dyC71R63CAv6wwwhBiDuoSdJI?domain=aka.ms>



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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Leave group<https://outlook.office365.com/mail/deeplink/groupActions?source=EscalatedMessage&action=leave&smtp=categories%40mq.edu.au&bO=true&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Learn more about Microsoft 365 Groups<https://aka.ms/o365g>


[-- Attachment #2: Type: text/html, Size: 8659 bytes --]

^ permalink raw reply	[flat|nested] 8+ messages in thread

* Re: Monadicity of extensions of essentially algebraic theories
  2025-10-20  4:58 ` Michael Shulman
@ 2025-10-20  7:36   ` Till Mossakowski
  0 siblings, 0 replies; 8+ messages in thread
From: Till Mossakowski @ 2025-10-20  7:36 UTC (permalink / raw)
  To: Michael Shulman, David Yetter; +Cc: Categories List

[-- Attachment #1: Type: text/plain, Size: 3038 bytes --]

For negative examples and discussion, see chapter 23 of http://katmat.math.uni-bremen.de/acc/acc.pdf<https://url.au.m.mimecastprotect.com/s/swmLCRONg6svJlYDEt9fYu12yHw?domain=katmat.math.uni-bremen.de>

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<https://url.au.m.mimecastprotect.com/s/LsEvCVARmOHx7KBn3czhKuELoz_?domain=outlook.office365.com>   |   Leave group<https://url.au.m.mimecastprotect.com/s/Jln4CWLVn6i52Y3LOSKiruoOew4?domain=outlook.office365.com>   |   Learn more about Microsoft 365 Groups<https://url.au.m.mimecastprotect.com/s/5EFoCXLW6DiX1NAP2cks0uW2oYW?domain=aka.ms>



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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Leave group<https://outlook.office365.com/mail/deeplink/groupActions?source=EscalatedMessage&action=leave&smtp=categories%40mq.edu.au&bO=true&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Learn more about Microsoft 365 Groups<https://aka.ms/o365g>


[-- Attachment #2: Type: text/html, Size: 9264 bytes --]

^ permalink raw reply	[flat|nested] 8+ messages in thread

* Re: Monadicity of extensions of essentially algebraic theories
  2025-10-19 21:50 Monadicity of extensions of essentially algebraic theories David Yetter
  2025-10-20  0:29 ` Richard Garner
  2025-10-20  4:58 ` Michael Shulman
@ 2025-10-20 12:47 ` henry
  2025-10-21 16:17   ` Michael Shulman
  2 siblings, 1 reply; 8+ messages in thread
From: henry @ 2025-10-20 12:47 UTC (permalink / raw)
  To: David Yetter; +Cc: Categories List

[-- Attachment #1: Type: text/plain, Size: 4014 bytes --]


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=sciencedirect.com. 
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=outlook.office365.com
> [2] 
> https://url.au.m.mimecastprotect.com/s/3sEWCgZ05JfArjNoru2ipu4jaZP?domain=outlook.office365.com
> [3] https://url.au.m.mimecastprotect.com/s/MjfXCjZ12Rfn2wAB2u7sVumY8qv?domain=aka.ms

[-- Attachment #2: Type: text/html, Size: 5111 bytes --]

^ permalink raw reply	[flat|nested] 8+ messages in thread

* Re: Monadicity of extensions of essentially algebraic theories
  2025-10-20  0:29 ` Richard Garner
@ 2025-10-20 13:40   ` Ivan Di Liberti
  2025-10-20 20:24   ` Eduardo J. Dubuc
  1 sibling, 0 replies; 8+ messages in thread
From: Ivan Di Liberti @ 2025-10-20 13:40 UTC (permalink / raw)
  To: Richard Garner; +Cc: David Yetter, Categories List

[-- Attachment #1: Type: text/plain, Size: 3482 bytes --]

I would suggest to check the scientific production of Yuto Kawase.

https://arxiv.org/a/kawase_y_1.html<https://url.au.m.mimecastprotect.com/s/cnJtCyoj8PurgQJP8HRs6ux3zzL?domain=arxiv.org>.

> On 20 Oct 2025, at 02:29, Richard Garner <richard.garner@mq.edu.au> 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<https://url.au.m.mimecastprotect.com/s/GVsaCzvkmpfM3ynYkcotAu93LL4?domain=arxiv.org>
>
> 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.
>

Best,
Ivan.

——————————————
Ivan Di Liberti
Assistant Professor in Logic
Coordinator of the Master in Logic
Göteborgs universitet
https://diliberti.github.io<https://url.au.m.mimecastprotect.com/s/E4W9CANpnDCNgPVKwtMu1uG7pck?domain=diliberti.github.io>


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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Leave group<https://outlook.office365.com/mail/deeplink/groupActions?source=EscalatedMessage&action=leave&smtp=categories%40mq.edu.au&bO=true&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Learn more about Microsoft 365 Groups<https://aka.ms/o365g>


[-- Attachment #2: Type: text/html, Size: 5866 bytes --]

^ permalink raw reply	[flat|nested] 8+ messages in thread

* Re: Monadicity of extensions of essentially algebraic theories
  2025-10-20  0:29 ` Richard Garner
  2025-10-20 13:40   ` Ivan Di Liberti
@ 2025-10-20 20:24   ` Eduardo J. Dubuc
  1 sibling, 0 replies; 8+ messages in thread
From: Eduardo J. Dubuc @ 2025-10-20 20:24 UTC (permalink / raw)
  To: Richard Garner, David Yetter; +Cc: Categories List

[-- Attachment #1: Type: text/plain, Size: 3156 bytes --]

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<https://url.au.m.mimecastprotect.com/s/QqFeCK1DOrC2lYyQ6ivh1u5XTRj?domain=arxiv.org>
>
> 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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Leave group<https://outlook.office365.com/mail/deeplink/groupActions?source=EscalatedMessage&action=leave&smtp=categories%40mq.edu.au&bO=true&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Learn more about Microsoft 365 Groups<https://aka.ms/o365g>


[-- Attachment #2: Type: text/html, Size: 5466 bytes --]

^ permalink raw reply	[flat|nested] 8+ messages in thread

* Re: Monadicity of extensions of essentially algebraic theories
  2025-10-20 12:47 ` henry
@ 2025-10-21 16:17   ` Michael Shulman
  0 siblings, 0 replies; 8+ messages in thread
From: Michael Shulman @ 2025-10-21 16:17 UTC (permalink / raw)
  Cc: Categories List

[-- Attachment #1: Type: text/plain, Size: 7525 bytes --]

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<https://url.au.m.mimecastprotect.com/s/wO2tCgZ05JfAr3y08TNfpu4LjPH?domain=arxiv.org>), 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)<https://url.au.m.mimecastprotect.com/s/LL32Ck815RCO7EBWgsQiVuGwrm8?domain=sciencedirect.com>.
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=EscalatedMessage&amp;action=files&amp;smtp=categories%40mq.edu.au&amp;bO=true&amp;GuestId=99bfc175-8542-4550-848c-9319f8c1e283<https://url.au.m.mimecastprotect.com/s/xshxClx1OYU2yrEnLCqsWuzQXY-?domain=outlook.office365.com>
> [2]
> https://outlook.office365.com/mail/deeplink/groupActions?source=EscalatedMessage&amp;action=leave&amp;smtp=categories%40mq.edu.au&amp;bO=true&amp;GuestId=99bfc175-8542-4550-848c-9319f8c1e283<https://url.au.m.mimecastprotect.com/s/ftxACmO5wZsjZxlJvIQtruRDASp?domain=outlook.office365.com>
> [3] https://aka.ms/o365g<https://url.au.m.mimecastprotect.com/s/Llk-Cnx1Z5U7zEDOnsEuvuJS3Ql?domain=aka.ms>


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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Leave group<https://outlook.office365.com/groups/groupsubscription?source=EscalatedMessage&action=leave&smtp=categories%40mq.edu.au&bO=true&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Learn more about Microsoft 365 Groups<https://aka.ms/o365g>


[-- Attachment #2: Type: text/html, Size: 10553 bytes --]

^ permalink raw reply	[flat|nested] 8+ messages in thread

end of thread, other threads:[~2025-10-21 19:02 UTC | newest]

Thread overview: 8+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2025-10-19 21:50 Monadicity of extensions of essentially algebraic theories David Yetter
2025-10-20  0:29 ` Richard Garner
2025-10-20 13:40   ` Ivan Di Liberti
2025-10-20 20:24   ` Eduardo J. Dubuc
2025-10-20  4:58 ` Michael Shulman
2025-10-20  7:36   ` Till Mossakowski
2025-10-20 12:47 ` henry
2025-10-21 16:17   ` Michael Shulman

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).