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.
Dan Doel (Apr 05 2020 at 23:12):Perhaps a related problem is that mathematicians don't study enough multi-sorted algebras.
Todd Trimble (Apr 05 2020 at 23:36):Dan Doel said:
Perhaps a related problem is that mathematicians don't study enough multi-sorted algebras.
Yes. There is a traditional bias toward one-sorted theories. Thus you don't hear as much about modules as two-sorted, rings+abelian groups they act on; usually the ring is given in advance and you talk about modules over that ring. Here, too, we could think of each element of as parametrizing a binary operation , and that would fit better the traditional prejudice. It would be a matter of (perhaps silly) debate which is the more useful point of view: a single multisorted ternary operation, or a family of one-sorted binary operations.
(One could also cook up contrived examples, using ternary trees, etc. But to me that's not too "convincing" an example.)
Dan Doel (Apr 06 2020 at 00:13):Ah, yeah. I suppose there's very little you couldn't massage into that format. It reminds me of reading the papers on algebraic effects. I was expecting it to involve many-sorted algebraic theories, but instead it used single-sorted theories where the arities could be infinitary, or even have additional structure (like being a poset).
Nathanael Arkor (Apr 06 2020 at 00:19):I was expecting it to involve many-sorted algebraic theories, but instead it used single-sorted theories
this seems particularly surprising considering that algebraic effects originate in computer science, where multisorted algebras tend to be much more readily treated as first-class
Dan Doel (Apr 06 2020 at 00:25):There is, at least, a plausible explanation in the papers in that case.
Morgan Rogers (he/him) (Apr 06 2020 at 10:20):Dan Doel said:
Perhaps a related problem is that mathematicians don't study enough multi-sorted algebras.
I enjoy the irony of saying this on a category theory forum :joy:
Morgan Rogers (he/him) (Apr 06 2020 at 10:25):Any theory (possibly with some caveats; certainly any finite-sorted, bounded-arity theory) is equivalent to a single-sorted one, roughly by imposing relations that divide the single sort into pieces corresponding to the sorts of the original theory, so if those are easier to deal with theoretically there's actually no loss to doing so. You just get a completely different (and usually obfuscating) perspective when you do this, which is why no one does category theory using the one-sorted formulation of categories that Freyd and Scedrov give at the start of Categories, Allegories. It's also why so few people have read past the first few pages of that book :upside_down:
Dan Doel (Apr 06 2020 at 14:49):Okay, well, that explanation reveals a bias that explains why computer scientists come up with this stuff, I guess.
Dan Doel (Apr 06 2020 at 14:51):There is "no loss" to people studying the properties of the algebraic theory. This is like the logician saying, "it's much easier for us to analyze first-order logic, so we should try to turn all theories first-order." Whereas someone just working in a logic will say, "it's much easier to work in a higher-order logic."
Nathanael Arkor (Apr 06 2020 at 14:54):Any theory (possibly with some caveats; certainly any finite-sorted, bounded-arity theory)
I think there are some caveats about the models too: e.g. either all the sorts must be uninhabited, or all the sorts must be inhabited
Dan Doel (Apr 06 2020 at 14:58):Although speaking of single sorted categories, I've seen someone do an interesting thing with that.
Dan Doel (Apr 06 2020 at 15:00):You can remove the requirement that and so on. And then you get a structure with arbitrarily many levels. It might be related somehow to -categories, but I'm not certain how.
T Murrills (Apr 06 2020 at 15:27):huh, I was thinking about this (out loud) on twitter the other day! it’s nice to know I’m not the only one!
It also seems like Categories, Allegories (which I’m only just starting to read!) requires that anything that is the domain of something else is necessarily an identity morphism. This immediately roots us firmly in the land of 1-categories—all the other relational structure that actually provides the important part of category theory may as well be of a different sort.
This is something I feel is true in general about category theory right now: its constructions are “allowed” to be built out of non-categorical parts, sort of, and then only identified retrospectively as part of the categorical story. Consider the explicit construction of comma categories, or the way natural transformations are suddenly allowed to map objects to arrows. We later find that comma categories are a certain kind of 2-limit, and natural transformations are 2-arrows. But once we’ve moved to this view, we’ve lost the “bones” of these constructions—or at least, I have! Afaik, there’s no sort of unified, systematic way of corresponding “nuts and bolts” definitions, like that of the comma category, with its categorical (often universal property) realization, without proving things out in individual cases. (This might just be my lack of experience talking, but...)
Contrast this situation to an extent with type theory, where things at least appear to be more foundational: all of our notation “knows what it is”, and isn’t an opaque object potentially shielding details below it. On one hand, that’s one of the great capabilities of category theory: to abstract away the details and let us work in a more relational way. On the other hand, it would be nice to have a more systematic dictionary between the two perspectives, somehow!
Morgan Rogers (he/him) (Apr 06 2020 at 15:30):Dan Doel said:
There is "no loss" to people studying the properties of the algebraic theory. This is like the logician saying, "it's much easier for us to analyze first-order logic, so we should try to turn all theories first-order." Whereas someone just working in a logic will say, "it's much easier to work in a higher-order logic."
There are loads of really powerful theorems that apply to first order theories, which mean that if you know that your theory can be expressed as a first order one, you get a tonne of results 'for free' (in that someone has already done the work for you), and it informs what type of functors preserve your structures when you look at models of them in a topos, say. This is why having a geometric logic formulation for local rings is so handy, for example: it means that the inverse image functors of geometric morphisms send local rings to local rings.
More generally, you don't express a theory as first-order or single-sorted it in order to restrict how you concretely reason about their models, you do it so it falls into a class that you can analyse simultaneously at a greater level of generality. I don't suddenly ignore the unique maximal ideal of a local ring just because I can remove it from my axioms!
Reid Barton (Apr 06 2020 at 15:48):But doesn't the translation from a multisorted theory to a single-sorted theory destroy some of those properties of a theory, like being a universal Horn theory or whatever?
Morgan Rogers (he/him) (Apr 06 2020 at 15:53):Reid Barton said:
But doesn't the translation from a multisorted theory to a single-sorted theory destroy some of those properties of a theory, like being a universal Horn theory or whatever?
I don't know. I hope a logician would be careful enough not to try to collapse everything at once, though.
Reid Barton (Apr 06 2020 at 15:53):In fact my impression is that in the context of category theory people are more likely to consider multisorted theories because they need them in order to have the correct structural results (e.g. a category is locally presentable iff its the category of models of some specific kind of theory I don't recall right now).
Reid Barton (Apr 06 2020 at 15:56):I also have the impression that restricting to single-sorted theories is basically an artificial device to reduce the complexity of notation
Reid Barton (Apr 06 2020 at 15:58):Like, logicians know that the theory of "a ring and a module over it" really "should" have two sorts, but for some purposes (but maybe not all purposes, basically depending on how powerful your logic/syntax is) you can get away with stuffing them into a single sort.
Morgan Rogers (he/him) (Apr 06 2020 at 16:04):Like how we don't name the binary operation in a group unless we really have to, sure.
Dan Doel (Apr 06 2020 at 16:10):@T Murrills https://arxiv.org/abs/1803.00180
Joe Moeller (Apr 06 2020 at 17:24):Modules over an algebra should be like 3-sorted, right?
Nathanael Arkor (Apr 06 2020 at 17:30):@Joe Moeller: what are the three sorts you're thinking of?
Nathanael Arkor (Apr 06 2020 at 17:31):or are you thinking of an algebra over a field, rather than a universal algebra?
Joe Moeller (Apr 06 2020 at 17:44):right, the latter. field acts on vectorspace acts on module
Nathanael Arkor (Apr 06 2020 at 17:50):yes, this should be 3-sorted
Philip Zucker (Apr 06 2020 at 18:10):Somewhat related to this thread, there's something that's been intriguing me about trying to do category theory in first order (probably single sorted) logic, that there seems like a larger possibility that one could use off the shelf automated theorem provers like E or Vampire for simple properties than is the case for higher order logic. The TPTP project has a couple different simple axiom sets for a category. http://www.tptp.org/cgi-bin/SeeTPTP?Category=Axioms&File=CAT002-0.ax . I think there's a decent shot that it could prove that the pullback of a monic is monic for example. I've been finding it very difficult to enforce and formulate the appropriate side conditions that correspond to correct typing on the sorts.