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.
Jens Hemelaer (May 19 2020 at 20:01):There seem to be two conventions for the definition of a finitary algebraic theory:
Is the second convention also used elsewhere?
I'm also wondering if the terminology is consistent with the terminology for finitary algebraic varieties. Is a finitary algebraic variety the same as the category of models for a finitary algebraic theory?
John Baez (May 19 2020 at 20:04):The second convention is not very useful in my opinion. What extra theorems do you get from assuming there are finitely many operations? The first convention says a finitary algebraic theory is an object of , the category of (small) categories with finite products. But in fact I'd leave out the word "finitary" here, usually - it's often taken for granted unless one is interested in infinitary operations.
John Baez (May 19 2020 at 20:05):I find this particular nLab article a bit confusing, and not very good at explaining the standard terminology.
Nathanael Arkor (May 19 2020 at 20:08):I believe "finitely presented algebraic theory" is in use for algebraic theories with a finite number of operators and finite number of equations.
Reid Barton (May 19 2020 at 20:08):And a finite number of sorts, I assume.
Reid Barton (May 19 2020 at 20:08):(Or does "algebraic theory" mean one sort?)
Nathanael Arkor (May 19 2020 at 20:10):There are differing conventions regarding whether "algebraic theory" is one-sorted or many-sorted, but in either case a finitely presented theory should have a finite number of sorts :+1:
John Baez (May 19 2020 at 20:19):I like the phrase "finitely presented algebraic theory" - the meaning is clear.
Reid Barton (May 19 2020 at 20:20):I think both concepts are of interest but I would definitely expect a category theorist to understand "finitary algebraic theory" to be the first one. Universal algebra probably has its own conventions which may differ for all I know.
John Baez (May 19 2020 at 20:21):My "algebraic theories" are by default many-sorted, with variable sorts - i.e. a map between them is just a finite-product-preserving functor between categories with finite products. I'd use something like "S-sorted algebraic theory" if I meant to fix the set S of sorts, with maps between such theories preserving the sorts. If there's just one sort I'd say "Lawvere theory".
Nathanael Arkor (May 19 2020 at 20:24):There is also the concept of many-sorted algebraic theories that have specified sets of sorts that are permitted to differ, as with cartesian categories.
Jens Hemelaer (May 19 2020 at 20:25):Thanks! It is good to know that (at least among category theorists) the first notion is the standard one.
Fabrizio Genovese (May 19 2020 at 20:42):Reid Barton said:
(Or does "algebraic theory" mean one sort?)
Unless explicitly stated it's safe to assume that "algebraic theory" means one-sorted. Structures with more than one sort go by different names, e.g. multi-sorted, coloured etc etc etc
John Baez (May 19 2020 at 20:44):Unless explicitly stated it's safe to assume that "algebraic theory" means many-sorted. If people want one sort they always say "Lawvere theory".
Hmm, or maybe it's not safe to assume anything! :upside_down:
Nathanael Arkor (May 19 2020 at 20:44):Fabrizio Genovese said:
Reid Barton said:
(Or does "algebraic theory" mean one sort?)
Unless explicitly stated it's safe to assume that "algebraic theory" means one-sorted. Structures with more than one sort go by different names, e.g. multi-sorted, coloured etc etc etc
Unfortunately, it's not as simple as this: for example, the reference Algebraic Theories: A Categorical Introduction to General Algebra uses "algebraic theory" to mean simply a category with finite products.
Jens Hemelaer (May 19 2020 at 20:47):My question was based on the statement in nlab that finitary algebraic theories are coherent. Does anyone know if you need the set of operations to be finite here?
Fabrizio Genovese (May 19 2020 at 20:51):Nathanael Arkor said:
Fabrizio Genovese said:
Reid Barton said:
(Or does "algebraic theory" mean one sort?)
Unless explicitly stated it's safe to assume that "algebraic theory" means one-sorted. Structures with more than one sort go by different names, e.g. multi-sorted, coloured etc etc etc
Unfortunately, it's not as simple as this: for example, the reference Algebraic Theories: A Categorical Introduction to General Algebra uses "algebraic theory" to mean simply a category with finite products.
Well, for sure in Universal Algebra the standard is to assume things to be single-sorted
Fabrizio Genovese (May 19 2020 at 20:52):I've never really looked much into its categorical counterpart. It's one of the few cases in which I like the traditional framework much much more actually
John Baez (May 19 2020 at 20:56):Universal algebraists tend to study the single-sorted case, but I think they tend to speak of varieties rather than "algebraic theories". Anyway, my remarks above were only about the categorical approach.
Fabrizio Genovese (May 19 2020 at 20:58):Yes, but they also call "theory" the equational theory attached to a variety via Birkhoff's Theorem, I guess algebraic theory still has a clear interpretation in this context?
John Baez (May 19 2020 at 20:58):Jens Hemelaer said:
My question was based on the statement in nlab that finitary algebraic theories are coherent. Does anyone know if you need the set of operations to be finite here?
Could you point me to the page that says that?
Jens Hemelaer (May 19 2020 at 20:59):John Baez said:
Jens Hemelaer said:
My question was based on the statement in nlab that finitary algebraic theories are coherent. Does anyone know if you need the set of operations to be finite here?
Could you point me to the page that says that?
It's on the page about coherent logic: https://ncatlab.org/nlab/show/coherent+logic
In the section "Examples".
Nathanael Arkor (May 19 2020 at 21:02):I don't understand what this is saying. Not every algebraic theory has finite limits, which is necessary for it to be coherent.
John Baez (May 19 2020 at 21:04):But for every algebraic theory (= category with finite products) you can find a coherent theory that has the same models.
Nathanael Arkor (May 19 2020 at 21:07):So the claim is that coherent theories are a conservative extension of algebraic theories, or something like that.
John Baez (May 19 2020 at 21:07):I think that's what the nLab is trying to say.
And to answer the question: this property of coherence holds regardless of whether or not there are just finitely many (generating) operations. The point is that all the laws in an algebraic theory are universally quantified equations. One can easily see that such laws are among those allowed in a coherent theory (see the top of the nLab article, Jens).
Jens Hemelaer (May 19 2020 at 21:12):Ok, thanks!
John Baez (May 19 2020 at 21:16):The confusion about whether or not we need to have just finitely many operations is one of the things I dislike about the nLab page algebraic theory, which may have been improved since I last looked at it. It's important to pick definitions and try to use the same definitions all over the nLab. Of course it's a work in progress!
John Baez (May 19 2020 at 21:17):But right now I see this page uses "algebraic theory" as a synonym for "Lawvere theory", which seems like a waste of a really useful term.
John Baez (May 19 2020 at 21:17):Lawvere theory means something really specific, and useful, so "algebraic theory" should mean something else.
John Baez (May 19 2020 at 21:18):And to me it does: a category with finite products.
Jens Hemelaer (May 19 2020 at 21:22):Now I see that my confusion was already with the term "finitary first-order logic". Apparently it is the same as what is just called "first-order logic" on Wikipedia.
John Baez (May 19 2020 at 21:27):I guess I know about two kinds of "infinitary" first-order logic: one that allows infinitary predicates, and another that allows infinitely long sentences.
John Baez (May 19 2020 at 21:27):But ordinary first-order logic doesn't allow either.
John Baez (May 19 2020 at 21:28):It does allow theories with infinitely many predicates, or function symbols, or axioms.
sarahzrf (May 20 2020 at 08:30):im sure ive seen at least one result that cares about having a finite signature :thinking:
sarahzrf (May 20 2020 at 08:31):certainly the completeness theorem is more convenient to prove for theories over a countable signature!
sarahzrf (May 20 2020 at 08:31):i dont want to learn cardinal arithmetic
John Baez (May 20 2020 at 15:03):Cardinal arithmetic: 1) every set has a number of elements; 2) you can add and multiply them corresponding to disjoint union and cartesian product, 3) numbers can get really big.
sarahzrf (May 20 2020 at 15:06)::bird:
sarahzrf (May 20 2020 at 15:06):you forgot exponents!!!
sarahzrf (May 20 2020 at 15:07):oh i guess that's included in cartesian product if you're admitting indexed ones...
John Baez (May 20 2020 at 16:40):I realized later I should add exponents.