Re: Monadicity questions

[Paul Levy <p.b.levy@bham.ac.uk>]

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

Dear Jonas,
Regarding powerset and other unranked monads, I don’t know if this is quite what you’re seeking, but you might look at our paper on monad tensorability:
https://lmcs.episciences.org/740<https://protect-au.mimecast.com/s/ZJnCC4QO8xS1k4wEiOHa6g?domain=lmcs.episciences.org>
Section 2 explains the relationship between large theories and monads, and in particular makes the following point.  When considering large theories, we need to distinguish between the property of having small free algebras and the weaker property of having free small algebras.   This leads to two distinct notions of presentation of a monad on Set, which we call  “genuine” and “spurious”.
Best,
Paul


From: Jonas Frey <jonas743@gmail.com>
Date: Monday, 5 February 2024 at 04:30
To: David Yetter <dyetter@ksu.edu>
Cc: categories@mq.edu.au <categories@mq.edu.au>
Subject: Re: Monadicity questions
CAUTION: This email originated from outside the organisation. Do not click links or open attachments unless you recognise the sender and know the content is safe.

Dear David,

Yes, models of single-sorted algebraic theories are always monadic over Set, and such theories correspond precisely to finitary, ie omega-filtered-colimit-preserving monads on Set. If we take the correspondence between single-sorted algebraic theories and Lawvere theories for granted, this is stated eg in Hyland--Power [1], with further references there. More generally, monads preserving alpha-filtered colimits for a higher regular cardinal alpha correspond to algebraic theories with alpha-ary operations; unbounded monads (such as the powerset monad) can be viewed as corresponding to "large theories" with no bound on their arities. The theory corresponding to the powerset monad, eg, is the theory of sup-lattices, ie posets with arbitrary small joins, which is not expressible with operations of bounded arities. Regarding references on these generalizations, I would also be curious.

Concerning your questions on extensions of theories, and more general kinds of theories and base categories, there recently was a long thread on the category theory zulip server [2], which I'll try to summarize: extensions of single-sorted theories by new operations and/or equations are always monadic (regardless of arities); this follows from the fact that monadic functors have the left cancellation property (Proposition 3.3 in [3]). Extensions by new sorts are typically not monadic, eg Set x Set is not monadic over Set. The models of many-sorted theories are monadic over powers of Set, and extensions of many-sorted theories by operations and axioms are also monadic, again by cancellation. Things become more complicated in the generalized/essential algebraic case, since (in the generalized algebraic, ie dependently typed case), adding new operations can create new sorts by substitution, which can lead to successive monadic extensions which are not composable, as Tom Hirschowitz, James Deikun, and possibly others pointed out. In general there's a lot of ongoing work on the dependently typed, ie generalized algebraic case, such as eg Chaitanya Leena Subramaniam's recent PhD thesis representing dependent algebraic theories by finitary monads on presheaf categories over direct categories [4].

[1] https://www.dpmms.cam.ac.uk/~martin/Research/Publications/2007/hp07.pdf<https://protect-au.mimecast.com/s/bE-CC5QP8ySGNkr3tOeX8X?domain=dpmms.cam.ac.uk>
[2] https://categorytheory.zulipchat.com/#narrow/stream/229199-learning.3A-questions/topic/distributive.20laws.20and.20monadic.20functors<https://protect-au.mimecast.com/s/9CwpC6XQ68fKwL47fmA10s?domain=categorytheory.zulipchat.com>
[3] https://ncatlab.org/nlab/show/monadic+functor<https://protect-au.mimecast.com/s/0qt_C71R63Ck7GB2SNvs3g?domain=ncatlab.org>
[4] https://arxiv.org/abs/2110.02804<https://protect-au.mimecast.com/s/FvgeC81Vq2CR4NyWco3f8C?domain=arxiv.org>

On Sun, 4 Feb 2024 at 21:00, David Yetter <dyetter@ksu.edu<mailto:dyetter@ksu.edu>> wrote:
We are all, of course, familiar with Beck's Theorem.  I'm rather hoping that there are results in the literature that will save me from having to prove that the underlying functor U creates coequalizers for U-split pairs in the context of two quite different projects I'm working on.  Thus, I have two questions for the community:


  1.  It seems obvious to me that for the same reason categories of models of finitary algebraic (equational) theories are monadic over Set, if one has (I think I'm using the term correctly here) a conservative extension of an equational theory (by which I mean, add operations and equations in such a way that no new equations are imposed on the operations of the original theory), then the category of models of the extension is monadic over the category of models of the original theory.  Surely this is either explicitly stated and proved somewhere, or follows easily from some result I simply have not encountered.   Citations?


  1.   What is the most general sort of theory whose models are monadic over Set? Or if that is not known, what sorts of theories have monadic categories of models over Set?   Are there multisorted generalizations of any results of that sort, ideally not just to Set^\alpha, where \alpha is the cardinality of a set of sorts, but to things like Graph?  Again some citations would be much appreciated.

Best Thoughts,
David Yetter
University Distinguished Professor
Department of Mathematics
Kansas State University

(That is the first and last time I'll use that signature block in writing to the list, but I thought I'd do it once since I thought the community would be gratified that a categorist was so honored.  After this it's back to David Y. or 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://protect-au.mimecast.com/s/Y4mxC91W8rCB74wAU1KYq7?domain=outlook.office365.com>   |   Leave group<https://protect-au.mimecast.com/s/o_EnC0YKgRs3PNAQHLqK4s?domain=outlook.office365.com>   |   Learn more about Microsoft 365 Groups<https://protect-au.mimecast.com/s/BcryCgZ05Jf2QEzKsK_Fpg?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://protect-au.mimecast.com/s/tRkaCjZ12RfqNoxDSM4Hvd?domain=outlook.office365.com>   |   Leave group<https://protect-au.mimecast.com/s/7v1YCk815RCQG2JAfDRxBj?domain=outlook.office365.com>   |   Learn more about Microsoft 365 Groups<https://protect-au.mimecast.com/s/BcryCgZ05Jf2QEzKsK_Fpg?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/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=files&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b>   |   Learn more about Microsoft 365 Groups<https://aka.ms/o365g>


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