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.
Martti Karvonen (Mar 26 2021 at 14:21):In a category of models of some algebraic theory, one can recognize finitely presentable (generated) models as those for which preserves filtered colimits (of monics). Is there a similar story to be told about when an algebraic theory can be finitely generated/presented? The concrete syntactic features I'm curious about so characterizing amount to "the theory can be given using finitely many (finitary) operations" or that+finitely many axioms. Besides algebraic theories, I'm curious about answers for e.g. finite-limit sketches or even more general notions of theories.
John Baez (Mar 26 2021 at 15:02):I think we can tackle your question using this idea: "there's an algebraic theory whose algebras are algebraic theories". But I only know how to make that idea precise (and true) if we work with multisorted Lawvere theories - that is, categories with finite products, equipped with a fixed set of of objects called sorts such that every object is
a finite product of these sorts:
It's pretty easy to prove that for any set there is a set such that there's a -sorted Lawvere theory whose models are -sorted Lawvere theories. I don't know if this is true, but I'm willing to bet that it is:
If so, an -sorted algebraic theory A will be finitely presentable (or finitely generated) iff hom(A,-) preserves filtered colimits (of monics).
Here I'm treating -sorted Lawvere theories 1-categorically, meaning that we have chosen finite products of the sorts, and the morphisms between -sorted Lawvere theories must preserve these "on the nose". One might prefer to work 2-categorically.
Ben Sprott (Mar 27 2021 at 14:31):Is there any way to do something similar to this definition in Lawvere theories but with monads instead?
Fawzi Hreiki (Mar 27 2021 at 14:37):Lack has a paper on the monadicity of finitary monads so perhaps one could define a finitely presented finitary monad in the usual way from that.
Ben Sprott (Mar 27 2021 at 14:48):Lack has a paper on the monadicity of finitary monads so perhaps one could define a finitely presented finitary monad in the usual way from that.
Sorry, if I have not understood. What I meant was, I want to address the idea of finitely presented theory but instead in terms of monads. Is it the case that you are taking a monad to "be" an algebraic theory? That is language I am seeing around the literature, though it's a bit of a mystery to me.
John Baez (Mar 27 2021 at 16:54):Ben: finitary monads on correspond perfectly to Lawvere theories, and sometimes people get sloppy and call Lawvere theories algebraic theories. If someone is taking a monad to "be" an algebraic theory, this is what they must be doing.
Fawzi was making an interesting suggestion based on the equivalence between finitary monads on set and Lawvere theories: any concept that can be defined for one can also be defined for the other.
Nathanael Arkor (Mar 28 2021 at 10:21):sometimes people get sloppy and call Lawvere theories algebraic theories
Lawvere called "Lawvere theories" algebraic theories :)
Fawzi Hreiki (Mar 28 2021 at 10:52):But that was before the shift to regarding any category with finite products as an algebraic theory
Nathanael Arkor (Mar 28 2021 at 11:18):I just disagree that it's "sloppy". I think it's justifiable to reserve "algebraic theory" for "Lawevere theory", since it has the closest correspondence with actual universal algebra.
Jules Hedges (Mar 28 2021 at 11:24):If forced to make a choice, I'd prefer to reserve the term "algebraic theory" for something in model theory, like a set of first order sentences in the universally quantified fragment
Jules Hedges (Mar 28 2021 at 11:24):That's surely closer to what the term intuitively means to someone who's not a logician
Fawzi Hreiki (Mar 28 2021 at 11:30):Ah but would you say a group is a set of symbols and words in those symbols
Fawzi Hreiki (Mar 28 2021 at 11:31):The problem with the ‘set of first order sentences’ is that it obscures what the structure of the theory, itself an algebraic structure, is
Jules Hedges (Mar 28 2021 at 11:32):Fawzi Hreiki said:
Ah but would you say a group is a set of symbols and words in those symbols
No, I would say that a group is a model of the FO theory of groups, and the FO theory of groups is a set of symbols and words in those symbols
Fawzi Hreiki (Mar 28 2021 at 11:34):But why set up this distinction between the way the structures in mathematics (groups, vector spaces, etc) are treated and the way the structures in logic (algebraic theories, first order theories) are treated?
Fawzi Hreiki (Mar 28 2021 at 11:35):An algebraic theory (category with finite products) is itself a model of a ‘doctrine’
Fawzi Hreiki (Mar 28 2021 at 11:35):For example, how would someone define a map between algebraic theories thinking about them as ‘sets of sentences’
Jules Hedges (Mar 28 2021 at 11:36):I'm not arguing against Lawvere theories, Lawvere theories are a great idea and probably the right way to do things
Fawzi Hreiki (Mar 28 2021 at 11:53):Sure, but beyond that I'm saying that we should really think of the categories containing the universal models as the theories themselves and we should view the syntactic presentations as just that - presentations.
What convinced me of this is the example of -rings, which are classified by the finite product category of Cartesian spaces and smooth maps. There isn't much use looking at this example syntactically but it's still worth regarding it as an algebraic theory since we can then study its interactions with other algebraic theories. For example, the inclusion of the theory of -algebras into induces a relative free-forgetful adjunction between -algebras and -rings.
Fawzi Hreiki (Mar 28 2021 at 11:55):Logicians may be more comfortable viewing theories as sets of sentences, but the theories-as-categories POV brings logic much closer to how the rest of mathematics operates which is certainly not a bad thing.
John Baez (Mar 28 2021 at 17:24):Nathanael Arkor said:
I just disagree that it's "sloppy". I think it's justifiable to reserve "algebraic theory" for "Lawevere theory", since it has the closest correspondence with actual universal algebra.
Unfortunately, "algebraic theory" is also widely very used to mean "category with finite products, regarded as a kind of theory" while Lawvere theory is always used to mean "category with finite products where the objects are in bijective correspondence with the natural numbers, their product corresponding to addition".
So, if you say "algebraic theory" and mean "Lawvere theory", there's a good chance people won't understand that's what you mean.
John Baez (Mar 28 2021 at 17:28):It seems most people agree that "essentially algebraic theory" means "category with finite limits, regarded as a kind of theory".
Thus, for consistency of terminology, it's good for people use "algebraic theory" to mean "category with finite products, regarded as a kind of theory". And a lot of people actually do use the term this way.
I'm not one to fight lost causes when it comes to terminology. But this is not a lost cause. So, I'm going to urge people not to waste the term "algebraic theory" by using it to mean the exact same thing as "Lawvere theory".
Fawzi Hreiki (Mar 28 2021 at 17:33):So by Lawvere theory you mean what exactly? A single sorted algebraic theory?
John Baez (Mar 28 2021 at 17:35):I mean what everyone else means:
https://ncatlab.org/nlab/show/Lawvere+theory#definition
John Baez (Mar 28 2021 at 17:35):https://en.wikipedia.org/wiki/Lawvere_theory#Definition
John Baez (Mar 28 2021 at 17:36):There are some small differences in how people present this idea, but they are purely cosmetic.
dusko (Mar 28 2021 at 19:46):oooh, the concept of "everyone means the same" is extremely prone to abuse. we all agree that john is not a candidate to abuse it, but every politician claims that everyone means the same, and nowadays they prove it by some website links. everyone except the village fool.
standardized terminology is certainly a matter of life and death e.g. for the meerkats: when the lookout spots danger, it is important that the cry "eagle" and the cry "cobra" are recognized by everyone in the clan, and that they all run in the same direction. but people usually don't mean the same thing by the same word all the time, so they invented sentences.
i think the useful difference between presenting algebraic (ie equational) theories by monads and by lawvere theories is that a monad requires that there are free algebras, and algebras for lawvere theories exist even when there are no representable ones. e.g. small complete lattices have an equational presentation and can be viewed as product-preserving functors. but the free ones are not small, and there is no monad for them.
i am sure this common knowledge in the web times, but i hope it won't hurt if i mention it.
Mike Shulman (Mar 28 2021 at 21:55):Fawzi Hreiki said:
Sure, but beyond that I'm saying that we should really think of the categories containing the universal models as the theories themselves and we should view the syntactic presentations as just that - presentations.
It's indisputable that syntactic presentations of theories are presentations of categories. I think it's also hard to argue with the fact that in general both syntactic presentations and the categories they present are important objects to study. As to which deserves the name "theory", well, as I opined elsewhere, why steal the name "algebraic theory" to mean "category with finite products" and force people to say "presentation of an algebraic theory" for the syntactic gadget, when we already have a perfectly good term "category with finite products" to use when that's what we mean?
John Baez (Mar 28 2021 at 21:59):That's fine except it's got 9 syllables instead of 3, which makes me run out of air when I'm talking, and it doesn't indicate the use I'm putting it to. For example, "category of models of a category with finite products" sounds funny to me - maybe it's just a matter of habit, but I like to talk about models of a "theory".
I sometimes use "finite products theory", which gets us down to 6 syllables.
Fawzi Hreiki (Mar 28 2021 at 22:25):Mike Shulman said:
Fawzi Hreiki said:
Sure, but beyond that I'm saying that we should really think of the categories containing the universal models as the theories themselves and we should view the syntactic presentations as just that - presentations.
It's indisputable that syntactic presentations of theories are presentations of categories. I think it's also hard to argue with the fact that in general both syntactic presentations and the categories they present are important objects to study. As to which deserves the name "theory", well, as I opined elsewhere, why steal the name "algebraic theory" to mean "category with finite products" and force people to say "presentation of an algebraic theory" for the syntactic gadget, when we already have a perfectly good term "category with finite products" to use when that's what we mean?
Of course. I never meant that syntactic presentations aren't important objects of study.
Mike Shulman (Mar 29 2021 at 03:36):What are you comparing it to that has 3 syllables? I count 6 syllables in "algebraic theory". And something like "fp-category" is not that uncommon and also has 6.
Mike Shulman (Mar 29 2021 at 03:37):You could also say "fp-sketch" which has 3 syllables and indicates both that it's a category (rather than syntax) and that you're interested in its "models".
John Baez (Mar 29 2021 at 03:54):I forget why I said "3 syllables".
I'd think an "fp-sketch" was not a category with finite products but the presentation of a category with finite products - something more syntactic. Like writing down the finite products category for groups by writing down , and some equations.
Mike Shulman (Mar 29 2021 at 14:16):https://ncatlab.org/nlab/show/sketch
Fawzi Hreiki (Mar 29 2021 at 14:33):But the category of sketches (for some specific limit/colimit doctrine) is not equivalent to the category of theories (for the same limit/colimit doctrine) right?
Mike Shulman (Mar 29 2021 at 17:48):Where by "theory" you mean... ?
Fawzi Hreiki (Mar 29 2021 at 21:39):I just meant categories with those relevant limits/colimits.
John Baez (Mar 29 2021 at 21:53):I don't know the "official" definition of the (2-)category of, say, limit sketches. But I can imagine a definition where nonisomorphic (or inequivalent) limit sketches gives isomorphic (or equivalent) categories with limits. In this case the (2-)category of limit sketches would not be equivalent to the (2-)category of categories with limits.
Mike Shulman (Mar 30 2021 at 01:25):Sure. But when you have a particular fp-category in hand and you want to talk about its models, you can call it an fp-sketch, because it is one. I thought that's what you were concerned about. When talking about the category of all fp-categories, why not just call it that?
John Baez (Mar 30 2021 at 01:53):Btw, I was just answering Fawzi's latest question, not trying to discuss this terminology issue.
Fawzi Hreiki (Mar 30 2021 at 06:55):Sure. I’m not trying to argue about terminology as such. Practically speaking categories with finite products will be called just that. I just meant more about the attitude towards logic in general.