You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Ambroise (Aug 23 2024 at 13:38):The left adjoint of a monoidal functor is oplax monoidal: this can be proven directly, or one can use Kelly's general setting of doctrinal adjunction, but for that one needs to show that monoidal categories are algebras of a 2-monad. I looked a bit at the literature for presentations of 2-monads from generators and relations, but they mainly seem to focus on 2-monads on the category of small categories. In the end you get doctrinal adjunction but only for small monoidal categories, while the direct proof does not have this restriction. Is there a satisfying way of getting rid of this size restriction?
Todd Trimble (Aug 23 2024 at 14:40):I imagine so (but how satisfying it is I don't know): if the 2-monad is finitary in nature, extend the 2-monad to locally small categories by expressing any such as a union of small full subcategories, apply the 2-monad, and take the union of the result. Something similar should apply for 2-monads of bounded rank.
I'm thinking this should be easy to formalize under a one-universe assumption currently being discussed elsewhere. :-)
Obviously I don't know where to find this in the literature.
Nathanael Arkor (Aug 23 2024 at 17:46):Conceptually, there's nothing size-specific going on with the free monoidal category construction: the 2-monad on the 2-category of small categories extends to a 2-monad on the 2-category of large categories, assuming you can quantify over classes. So Kelly's general result applies directly. Perhaps the simplest solution to avoid worrying about classes is to assume a single universe, and call things in that universe "small", and things not in the universe "large", as Todd suggests. Then you can simply use the usual 2-monad on set-sized categories.
Ambroise (Aug 28 2024 at 05:40):Thank you for your explanations! It would be nice if Todd's statement that accessible 2-monads extend to 2-monads on CAT was explicitly proven somewhere :) Anyway, assuming a universe may indeed be the simplest way to solve my question, although I was hoping for another solution (afterall, the direct proof of doctrinal adjunction for monoidal categories does not require a universe)
Nathanael Arkor (Aug 28 2024 at 19:34):The proof of doctrinal adjunction doesn't require a universe because you have allowed yourself to quantify over all large categories: this is also a foundational assumption you have made. Similarly, one can define a 2-monad without actually being able to construct a huge categories of large categories: you simply specify all the data of the 2-monad (i.e. for every large category , a large category , etc.). This uses the same foundational assumptions you use for doctrinal adjunction.
Nathanael Arkor (Aug 28 2024 at 19:35):As far as I can see, Todd's approach does not avoid the need for universes, because in order to construct the 2-monad in question from smaller pieces, you still need to have a huge category of large categories.
Nathanael Arkor (Aug 28 2024 at 19:37):But I don't really see that allowing quantification over classes has many advantages over simply using a universe. It's not more general in any practical sense.
Todd Trimble (Aug 28 2024 at 21:59):I sort of generally assume that mathematicians in the street feel a little uneasy around classes (what operations are or are not allowed), but much less uneasy around sets, so that they can relax a little if the only thing to keep straight is sets versus small sets. That would be mostly a pedagogical or psychological thing. (Plus, a one-universe assumption feels so piddlingly modest, compared to what real set theorists are willing to consider.)
(Of course, my general assumption might be wrong.)
The one-universe assumption is the tack Mac Lane takes in his Categories for the Working Mathematician.
Madeleine Birchfield (Aug 29 2024 at 02:29):Classes feel like a concept that only exists in set theory, whether via class-set theories like Morse-Kelley or via algebraic set theory or as first-order formulas which are not sets.
In dependent type theory, one would just explicitly postulate a universe of some sort as part of the inference rules, and I think the same might be true of simply typed higher order logics.
Ambroise (Aug 29 2024 at 12:21):Thanks for the clarification @Nathanael Arkor ! Actually, there may be a way of avoiding the detour through 2-monads by exploiting a "construction" of the 2-category of monoidal categories from inserters and equifiers, starting from Cat in 2-Cat. Kelly's doctrinal adjunction can certainly be adapted for inserters (and maybe for a wide class of marked 2-limits), for example.
Mike Shulman (Aug 29 2024 at 16:58):Put differently, it should be possible to prove doctrinal adjunction generally for the 2-category of algebras for any suitable kind of "theory", independently of whether free algebras for that theory exist.
Ambroise (Aug 29 2024 at 18:35):when you say "theory", do you have something precise in mind?
Mike Shulman (Aug 30 2024 at 00:16):There are many ways one could make it precise, such as a Cat-operad or Cat-enriched Lawvere theory. I didn't have a particular one in mind.
Tom Hirschowitz (Aug 30 2024 at 11:52):Ambroise said:
Actually, there may be a way of avoiding the detour through 2-monads by exploiting a "construction" of the 2-category of monoidal categories from inserters and equifiers, starting from Cat in 2-Cat. Kelly's doctrinal adjunction can certainly be adapted for inserters (and maybe for a wide class of marked 2-limits), for example.
This sounds really cool, but I don't understand. What would the statement look like, e.g., for inserters?
Ambroise (Aug 30 2024 at 14:43):I haven't checked the details, but here is the idea. An inserter diagram in 2-Cat consists in two parallel 2-functors F and G. From this data, you can define the 2-category of strict/lax/colax algebras: the objects are always the same (an object consists of a 1-cell Fa --> Ga) but the 1-cells are squared filled with identites/2-cells(in one direction or another). Then you can state doctrinal adjunction as in the usual 2-monadic case.
Ambroise (Aug 30 2024 at 14:44):I think that those 2-categories of algebras are all marked limits in some (generalised) sense, so they make sense for any inserter diagram in any 3-category, but I don't know how to state doctrinal adjunction in this more general situation
Tom Hirschowitz (Aug 30 2024 at 15:52):Oh, nice, thanks. I'd never heard of marked limits before.