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.
Chaitanya Leena Subramaniam (Dec 01 2021 at 04:28):Given a single-sorted algebraic theory (aka a Lawvere theory) , there seems to be a multisorted algebraic theory whose category of algebras/models is the slice category , where is the category of single-sorted algebraic theories. Has anybody worked on this? @John Baez perhaps?
Something similar holds for categories of suitably "sorted" essentially algebraic theories (where such a category is the category of finitary monads on a presheaf category).
I'm asking because I'm interested in finding a general notion of "opetope" that should include something like this, in particular opetopes that arise from invertible unary operations (I could try to draw the picture in my head of what such an opetope might look like if someone wants me to).
John Baez (Dec 01 2021 at 12:15):I don't know anyone who has studied this.
John Baez (Dec 01 2021 at 12:19):But I haven't been paying careful attention to everything people are doing with opetopes these days!
I'm completely convinced of your claim in the case where is the terminal Lawvere theory: that is, there's a multisorted algebraic theory whose category of algebras is the category of Lawvere theories.
John Baez (Dec 01 2021 at 12:21):In this paper we proved something similar:
John Baez (Dec 01 2021 at 12:22):Namely, we showed there's a multisorted algebraic theory whose category of algebras is the category of props.
John Baez (Dec 01 2021 at 12:23):A prop is a strict symmetric monoidal category whose set of objects is the natural numbers, with the tensor product being addition. So, a Lawvere theory is the same as a prop where the monoidal product is cartesian.
John Baez (Dec 01 2021 at 12:25):We proved this theorem because we wanted to reason with props the way people reason with groups or rings: defining them using generators and relations, taking quotients of them by adding extra relations, etc.
John Baez (Dec 01 2021 at 12:25):I think we noted that there's also a multisorted algebraic theory whose algebras are Lawvere theories, but if so it was an offhand comment in an appendix, not something we needed.
John Baez (Dec 01 2021 at 12:26):Indeed for any set of sorts, there's a multisorted Lawvere theory whose algebras are -sorted Lawvere theories. You will want to reason at this level of generality if you want to iterate the slice construction and think about "cartesian opetopes".
Nathanael Arkor (Dec 01 2021 at 13:41):This is true, though I haven't seen it explicitly studied somewhere. For a proof, recall that the categories of models for multisorted algebraic theories are precisely the [[locally strongly finitely presentable]] (LSFP) categories. is LSFP, as mentioned by John. Furthermore, the slice of a LSFP category is LSFP (see, for instance, Remark 3 of Centazzo–Rosický–Vitale's A characterization of locally -presentable categories, taking to be the class of finite discrete categories). Therefore, for any algebraic theory , the slice category is LSFP and hence the category of models for some multisorted algebraic theory . The same is true for essentially algebraic theories for the same reason (here taking to be the class of finite categories). However, I suspect that it would be difficult to find a syntactic characterisation of the algebraic theory in question (conversely, coslices of are relatively straightforward to describe syntactically, but more difficult to characterise categorically).
Mike Shulman (Dec 01 2021 at 13:59):Doesn't the case of general follow formally from the case , using the fact that a slice of a monadic functor is monadic?
Nathanael Arkor (Dec 01 2021 at 15:11):To spell it out a little more explicitly, you're saying that, since is monadic (for some ), that is monadic (and the latter is again a power of , exhibiting as the category of models for a multisorted algebraic theory). Is that right? That also seems like a nice argument – I hadn't considered that the slice adjunction preserves monadicity.
John Baez (Dec 01 2021 at 15:57):I think we need something like "the slice of a finitary monadic functor is finitary monadic", since it's finitary monads that correspond to Lawvere theories.
I don't know such a result, but it's probably true....
Mike Shulman (Dec 01 2021 at 17:11):Nathanael Arkor said:
That also seems like a nice argument – I hadn't considered that the slice adjunction preserves monadicity.
To give credit where it's due, this argument was suggested by @Chaitanya Leena Subramaniam in an email; I just observed that the slice adjunction does in fact preserve monadicity.
Mike Shulman (Dec 01 2021 at 17:14):John Baez said:
I think we need something like "the slice of a finitary monadic functor is finitary monadic", since it's finitary monads that correspond to Lawvere theories.
Yes, I think so. A forgetful functor is "finitary monadic" iff it is monadic and finitely accessible (since left adjoints are always cocontinuous), and the slice of a finitely accessible functor is finitely accessible (since colimits in slice categories are created in the base).
Chaitanya Leena Subramaniam (Dec 01 2021 at 19:39):Thanks everyone! The case of the terminal -sorted Lawvere theory is in Bénabou's Structures algébriques dans les catégories (cf. paragraph III of the Introduction and Section 3.2). As @Mike Shulman mentioned, the general case follows since slicing preserves monadicity and finitariness.
I'm actually interested in a dependently sorted version of this, where a dependently sorted algebraic theory is a finitary monad on presheaves on what Makkai calls a "simple one-way" category. Since the category of elements of a presheaf on a simple category is once again a simple category, the same argument shows that the Baez-Dolan slice construction exists for dependently sorted algebraic theories.