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.
David Tanzer (Mar 11 2024 at 05:34):Is every variety in universal algebra, defined as an equational class, a complete and/or co-complete category?
I see that the category of fields is not complete, but that's not relevant, is it is not definable by a set of term equations (since division is only a partial operation).
Evan Patterson (Mar 11 2024 at 05:53):Yes: every variety is an "algebraic category" (a category equivalent to the category of models of an algebraic theory), and algebraic categories are complete and cocomplete. One place you can find these results is the book Algebraic Theories by Adamek, Rosicky, and Vitale.
David Tanzer (Mar 11 2024 at 06:10):Good to know, and thanks for the reference!
John Baez (Mar 11 2024 at 15:37):Note this result is actually a slick way to show that fields aren't definable by operations obeying equations. It may seem obvious - after all, division is only partially defined - but it's actually hard to show directly that no variety is equivalent to the category of fields: maybe some elaborate collection of operations obeying weird equations could give a category that's secretly equivalent to the category of fields? The quick way to rule this out is to show that the category of fields lacks properties that varieties all have.
John Baez (Mar 11 2024 at 15:54):It's worth knowing that the nLab uses the term [[algebraic category]] in a more general sense than Evan is using it. I like Evan's usage, and I think it's widespread, but the nLab calls this kind of category "finitary monadic".
John Onstead (Mar 12 2024 at 00:12):John Baez said:
It's worth knowing that the nLab uses the term [[algebraic category]] in a more general sense than Evan is using it. I like Evan's usage, and I think it's widespread, but the nLab calls this kind of category "finitary monadic".
Interesting, I always took "algebraic" to mean "finitary monadic" since finitary monadic categories are exactly the categories of models of Lawvere theories. In the nlab case, "algebraic categories" are apparently equivalent to categories of algebras of quasi-varieties as opposed to varieties (which correspond to monadic ones). But what kinds of theories are quasi-varieties and how do they relate to other notions of "algebraic theory"? For instance, are algebraic categories special cases of locally presentable categories, categories of models of essentially algebraic theories? If so, which essentially algebraic theories give rise to quasi-varieties (and thus which locally presentable categories are algebraic)? (it seems the connection might be given by Horn theories since every Horn theory is essentially algebraic and quasivarieties require Horn clauses for the equational axioms, but I don't know of any more concrete connection)
John Onstead (Mar 12 2024 at 02:33):On further thought this is directly relevant to the above question because nlab algebraic categories being locally presentable means that not only are varieties cocomplete, but quasi-varieties must be as well (since locally presentable categories are cocomplete, and therefore nlab algebraic categories are too). I will show this in detail below in one of my first "proofs" of sorts I've attempted, so please do let me know if I did anything wrong as I'm trying to learn this important mathematical skill! And if everything looks good, maybe this info (cocompleteness and being locally presentable) could be added to the nlab page on "algebraic categories" under "properties"?
Here's my proof that all nlab algebraic categories are locally presentable. First, nlab algebraic categories ~ categories of algebras of quasi-varieties as per the page and AHS 24.11. Then, under Wikipedia's article on Horn theories (which cites from Burris and Sankappanavar 1981) it states "classes of algebras definable by a set of quasi-identities [Horn clauses] are called quasi-varieties". Thus, quasi-varieties ~ Horn theories (since Horn theories are just sets of Horn clauses) and so categories of algebras of quasivarieties ~ categories of models of Horn Theories. Lastly, under nlab "essentially algebraic theory" (citing a paper by Barr and Palmgren, Vickers) it states that "Horn theory is essentially algebraic... essentially algebraic theories are equivalent to partial Horn theories". Thus, Horn theories < partial Horn theories ~ essentially algebraic theories. By Gabriel-Ulmer duality, locally presentable categories ~ categories of models of essentially algebraic theories and so categories of models of Horn theories < locally presentable categories. Completing this proof by combining everything we get: categories of algebras of quasi-varieties ~ nlab algebraic categories < locally presentable categories.
Kevin Arlin (Mar 12 2024 at 03:04):This is close to true, but nLab algebraic categories entertain the possibility of a proper class of operations and/or axioms, which gives a kind of category which, like compact Hausdorff spaces, may be algebraic or even monadic without being locally presentable.
John Baez (Mar 12 2024 at 03:12):By the way, in Corollary 1.52 of Adámek & Rosický's book they show any locally presentable category is the category of models of a limits sketch - i.e., it's the category of small-limit-preserving functors from a small category with small limits to .
John Onstead (Mar 13 2024 at 14:35):@Kevin Carlson (aka Arlin) So after a little more thought I realized this discussion reminds me of the one from yesterday where large sketches were mentioned, and so I wanted to know if they are indeed related. More precisely: As Dr. Baez points out here, locally presentable categories are categories of models of small limit sketches, as well as categories of models of generalized/essentially algebraic theories (which include Horn theories). There are thus two ways of generalizing the situation. First, as you mention here, we can expand beyond considering small sets of operations and axioms in our Horn theories (or more generally the generalized algebraic theories) to include classes. Secondly, at the same time, we can extend small limit sketches to large limit sketches, giving things like strongly compact categories. My ultimate question is then: is this the same process; do these two generalizations converge? Is extending from small to large sketches "equivalent" (in the sense of categories of models) to extending from theories with sets to theories with classes? In effect, are all algebraic categories sketchable by large limit sketches?
John Baez (Mar 13 2024 at 17:15):Could someone list a few simple examples of mathematical gadgets that are described by Horn theories but not (small) limits theories? I think that could give us some intuition on @John Onstead's question.
Kevin Carlson (aka Arlin) (Mar 13 2024 at 17:28):Up to picking size parameters there are no such examples--specifically, finite limit theories strictly subsume Horn theories in the language where only finite conjunctions are allowed. For instance Cat is the models of a finite limit theory but not of a Horn theory, because Cat doesn't have enough regular projectives.
Kevin Carlson (aka Arlin) (Mar 13 2024 at 17:30):This is from Barr's short paper cited on the nLab page: https://www.math.mcgill.ca/barr/papers/horn.pdf
John Baez (Mar 13 2024 at 18:58):I see. So is the similar question for choices of size parameters other than "finite limit theory" and "Horn theory with finite conjunctions" still open? I guess that's exactly what John Onstead was asking, but now I understand the question a bit better.
Kevin Carlson (aka Arlin) (Mar 13 2024 at 19:04):Yeah, it's not quite clear to me, there are lots of little variations and I don't understand them all super well.
John Onstead (Mar 13 2024 at 20:58):I guess I can try to clarify. Various types of sketches and theories have equivalences between them for complicated reasons I do not fully understand. For instance, there is a correspondence between generic sketches and basic first order theories, or limit sketches and generalized algebraic theories in that their categories of models in Set are equivalent. I was asking if there was a sketch-theory equivalence of this form between specifically large limit sketches and large generalized algebraic theories (which have proper classes of symbols and axioms rather than the usual bounded small sets). If so, then because algebraic categories are categories of models of (potentially large) Horn theories, and Horn theories are cases of generalized algebraic theories, this would imply algebraic categories are sketchable by large limit sketches.
John Baez (Mar 13 2024 at 21:35):John Onstead said:
I guess I can try to clarify. Various types of sketches and theories have equivalences between them for complicated reasons I do not fully understand. For instance, there is a correspondence between generic sketches and basic first order theories, or limit sketches and generalized algebraic theories in that their categories of models in Set are equivalent.
I don't know the definition of "generic" sketch or "basic" first order theory. As for limit sketches and generalized algebraic theories, the relation doesn't seem too mysterious. I may be missing a lot of subtleties, but:
I looked at how you can define the concept of category using a generalized algebraic theory: you start with a type Ob and a dependent type Hom(a,b) depending on a,b:Ob, and then define composition from Hom(a,b) x Hom(b,c) to Hom(a,c), etc. More generally a generalized algebraic theory allows finite iteration of dependence when forming dependent types.
I know how you can define the concept of category using a limits sketch: you start with objects Ob and Mor, and say that composition of morphisms is defined on a pullback involving these, etc. More generally a limits sketch allows you finite iteration of forming new objects as limits of diagrams involving old ones.
Given this, it doesn't seem shocking that Cartmell found a translation procedure for going back and forth between generalized algebraic theories and limits sketches.
John Baez (Mar 13 2024 at 21:41):I would find it less mentally stressful if Cartmell were restricting himself to generalized algebraic theories with finitary operations and claiming these were equivalent to finite limits theories. From the nLab article (which is all I've read - not Cartmell's paper alas) it sounds like no such restriction is being imposed. So I'm guessing that his claim is that generalized algebraic theories with "smallary" operations are equivalent to "small limit sketches" (which most people just call limit sketches).
Mike Shulman (Mar 13 2024 at 21:59):In the context of relating GATs to limit sketches and essentially algebraic theories, two related threads of work are Chaitanya Leena Subramaniam's thesis on dependently typed algebraic theories and Jonas Frey's work on clans. Cartmell's definition of GAT is, IIRC, rather syntactic and harder to understand category-theoretically; I find these more recent repackagings easier to think about.
John Onstead (Mar 13 2024 at 22:05):@John Baez A generic sketch is just the general definition of a sketch: a directed graph equipped with a set of diagrams, cones, and cocones. A "basic" or "suitable" first order theory is a one such that the category of models is an accessible category, which are also the categories of models of generic sketches. There might be non-basic first order theories, in which case the category of models might not be accessible, but the category of models restricted to elementary embeddings will be accessible. I'm not exactly fully clear on what that exactly means, but it is what I have seen.
Cartmell's paper does not mention sketches. The main result was that his generalized algebraic theories had equivalent categories of models as essentially algebraic theories. Regardless, I am interested if a theory-sketch translation procedure does indeed exist that works in generality rather than on a case-by-case basis. If so I could apply it to "large theories" to see if they are "equivalent" to large sketches. Unfortunately, I do not have full access to most works detailing relationships between theories and sketches (there's a section in Johnstone's Sketches of an Elephant about it, as well as it being a key subject in both Makkai and Pare's work "Accessible Categories" and in Adamek and Rosicky's work "Locally Presentable and Accessible Categories")
@Mike Shulman I'll look into these, thanks!
John Baez (Mar 13 2024 at 22:31):There's a bunch of elementary material on sketches and theories in the free book Toposes, Triples and Theories, starting on page 123, the chapter called "Theories". At first they consider sketches with only cones, not cocones. Later they include cocones.
They define "finite products sketches" and their models, and they show any finite products sketch has a corresponding category with finite products such that models of correspond to finite-product-preserving functors .
Then they do the same for finite limits sketches, which they call "left exact sketches". For each such sketch they construct a category with finite limits such that models of correspond to finite-imit-preserving functors . I would call a category with finite limits an "essentially algebraic theory" but it seems that many people here weaken the finiteness restriction when discussing essentially algebraic theories.
I don't see them doing some similar relating arbitrary small limits sketches to categories with small limits.
All this stuff is very old. I'd hope there are more complete treatments by now. But it's pretty easy to read.
Nathanael Arkor (Mar 13 2024 at 22:50):John Baez said:
I would find it less mentally stressful if Cartmell were restricting himself to generalized algebraic theories with finitary operations and claiming these were equivalent to finite limits theories.
Cartmell's generalised algebraic theories are finitary, and he does claim these are equivalent in a suitable sense to finite limit theories, though I would argue the claim was not actually proven until much later (e.g. in Chaitanya Leena Subramaniam's thesis).
John Baez (Mar 13 2024 at 22:56):Oh, good! About the finitarity, that is. Since the nLab uses "algebraic theory" to mean something more general than I do (I mean a category with finite products), I assumed they were doing the same for "essentially algebraic theory". But lo and behold, they're using "essentially algebraic theory" to mean "finite limits theory". I'm relieved, and I hope nobody there decides to make up a new definition.
Mike Shulman (Mar 13 2024 at 23:06):We could open a conversation about changing the nLab's notion of "algebraic theory".