Category Theory
Zulip Server
Archive

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.

Stream: theory: category theory

Topic: Value of HSP theorem

Ralph Sarkis (Aug 01 2024 at 16:37):

Birkhoff's HSP (or variety) theorem states that any class of algebras (on the same signature) that is closed under homomorphic images, subalgebras, and products is a variety, namely, it can be defined by a set of equations. More succinctly, we could write

$$\mathbf{HSP}(\mathcal{K}) = \mathbf{Mod}(\mathbf{Eq}(\mathcal{K})).$$

This is a fundamental result in universal algebra that, amongst other results in these two papers by Birkhoff, revived an old field and spawned many new branches of research (as far as I can understand, it is also thanks to the modern language that Birkhoff used to state these results). A few years ago, I wondered about the importance of the HSP theorem and after coming back to this question several times, I am still not entirely convinced by what I have read here and there. This does not sit right with me because I feel like very smart people I know/read value the HSP theorem more than they should (from my perspective). My PhD defense is coming up, so I wanted to ask you two questions to help me prepare my answers to this line of questioning. The first is general and the second more specific.

1. How would you best communicate the value of the HSP theorem to category theorists (specifically to me :laughing:)?
2. In trying to answer a question posed by a reviewer of my thesis, I stumbled upon the following statement by Barr (in the abstract):

[The HSP theorem] does not hold as it does in sets, primarily because the axiom of choice (in the form that epimorphisms split) totally fails in posets.

I would like to understand why AC is important here because some of my arguments rely on having epimorphisms that split (I have seen this to be true in other instances like in §3.3 of Manes' Algebraic Theories). The first thing I found when looking into it is that HSP is independent of the axiom of choice. Do you know what Barr meant?

Chris Grossack (they/them) (Aug 01 2024 at 18:33):

Here's one reason to care:

Say you have some collection of algebraic gadgets that you like. It's obvious to wonder if there's some (equational) axiomatization of these gadgets. The first thing the HSP tells you is that there's an easy thing to check! For instance, if fields are your favorite algebraic gadget, the HSP theorem immediately tells you "no, there's no axiomatization". Why? Because fields aren't closed under P (products).

But the HSP theorem gives you more! it tells you that if you start from a family of gadgets you like you can MAKE IT equational (in a "minimal way") by closing it first under Products, then Subobjects, then Homomorphic images (read: quotients). A priori you might need to repeat some of these constructions, but the HSP theorem says if you just close under these operations in this order, that's enough!

So, for our example of fields. First we look at products of fields. Then we look at subalgebras of products of fields. Then we look at quotients of these. The class of these structures will guaranteedly be equationally axiomatizable!

In fact, it's not hard to show that everything in SP(fields), that is every subalgebra of a product of fields, is (commutative) von neumann regular. It's only slightly harder to show that all commutative von neumann regular rings are subalgebras of a product of fields (see here, for instance)! So we learn that SP(fields) = vNReg, and thus HSP(fields) = H(vNReg) = vNReg, since von neumann regular rings are already a variety!

So at the end of the day, the HSP theorem tells us that the variety best approximating fields are the commutative von neumann regular rings (these are sometimes called meadows in the literature, which is a cute pun).

Of course, there's nothing special about fields here, and you can play the same game with you favorite class of algebraic structures to get a "varietal envelope" containing your class. It's kind of a miracle that HSP(structures) is the varietal closure!

Chris Grossack (they/them) (Aug 01 2024 at 18:36):

Why should you as a category theorist care? Well, that's harder to answer, haha. Sticking with the example of fields, it's not obvious what the classifying topos should be. Of course, we know how to build the classifying topos for vNReg, since it's algebraic! Then we can use a (grothendieck) topology to add the geometric axiom that $(x = 0) \lor (x x^{-1} = 1)$ (which identifies the fields among the meadows), and this tells us the classifying topos for the theory of (coherent) fields. For more, see Johnstone's Rings, Fields, and Spectra as well as Caramello and Johnstone's De Morgan's Law and the Theory of FIelds.

Chris Grossack (they/them) (Aug 01 2024 at 18:46):

As for why AC is important, I'm a bit rusty on my proof of HSP and varietal closures, but remember that one big reason to care about varieties is because they admit free models. Also, the operations of HSP were chosen because they're crucial for the development of free models!

After all, how might you build a free model on $\kappa$ generators? Well, here's one idea: look at the family $V_\kappa$ of all $\kappa$-generated models. These are bounded in size (by the max of $\aleph_0$, $\kappa$, and the size of the defining language) so there's only a set of such models (up to isomorphism). This means we can Product them all together, then look at a "generic" Subalgebra. It's not hard to show (using the restrictions of the obvious projections) that the Homomorphic images of this are all the $\kappa$-generated models!

Of course, to make this game work, we secretly used AC! Where? In asserting that the product of all these (nonempty) $\kappa$-models is itself nonemtpy! Remember that AC is equivalent to the assertion that the product of infinitely many nonempty sets is nonempty!

If I remember the proof of the HSP theorem correctly (though again, it's been a lot of years, and for some reason I think there's another proof which is more combinatorial...), we crucially use the fact that HSP(algebras) has free models, and thus we use AC.

Chris Grossack (they/them) (Aug 01 2024 at 18:51):

I don't have time right now to go back and check, but you can read more about all this in Burris and Sankappanavar's excellent A Course in Universal Algebra (freely available here). Just looking at the table of contents you can see that these ideas flow into each other in roughly the way I outlined:

§9 Class Operators and Varieties ..................................... 60
§10 Terms, Term Algebras, and Free Algebras ................. 62
§11 Identities, Free Algebras, and Birkhoff's Theorem ... 71

It might be worth reading these sections to get a better idea of where AC is used (and to get a version of this proof that isn't half-remembered, haha)

Nathanael Arkor (Aug 01 2024 at 18:55):

Chris Grossack (they/them) said:

So at the end of the day, the HSP theorem tells us that the variety best approximating fields are the commutative von neumann regular rings (these are sometimes called meadows in the literature, which is a cute pun).

How does this relate to the fact that the category of algebras for codensity monad of the forgetful functor from fields to sets is the free product completion of the category of fields (e.g. Theorem 4.6 in Pushforward monads)? It sounds like this would just be P(Fields), but then why is it necessary also to close under subalgebras in this example?

Chris Grossack (they/them) (Aug 01 2024 at 19:02):

@Nathanael Arkor I'll be honest, I'm not sure. Somewhat embarrassingly, I still haven't taken the time to learn what the codensity monad even is... I guess you're saying that the varietal closure should be related to the algebras for this codensity monad, and thus should be the free product completion? Maybe I was being overcautious in saying that every meadow is a subdirect product of fields? I think it's true that every finite meadow is actually a product of finite fields, so maybe that's how this gets resolved?

Nathanael Arkor (Aug 01 2024 at 19:25):

Kennison and Gildenhuys sum the codensity monad up nicely:
image.png

So the codensity monad construction gives the minimal (potentially infinitary) variety containing the given category. Unfortunately they don't explicitly mention the relation to the HSP theorem.

Chris Grossack (they/them) (Aug 01 2024 at 19:31):

Oh wow, yeah that's really interesting! I'll have to think about it

Ralph Sarkis (Aug 01 2024 at 21:32):

Thanks! The "closest variety" thing sounds interesting but I am not immediately enticed by the story right now, so let me address the AC question.

I see where AC might be necessary in the proofs I understand (although that book and my preferred reference Universal Algebra for Computer Scientists do not make it explicit). However, that paper I linked above claims it can bypass that.

Now, Barr specifically mentions the AC formulation as "epis split", and I would like to see a proof that directly uses this, because it might make the need for AC in a categorical generalization more obvious. Also, Barr's goal for his generalized HSP theorem is the category of posets where AC fails, but Bloom had already proven an HSP theorem for posets here and Barr does not mention it. I have a feeling this means I don't get the HSP theorem and what I should look for when generalizing it.

Ralph Sarkis (Aug 01 2024 at 21:38):

Chris Grossack (they/them) said:

but remember that one big reason to care about varieties is because they admit free models. Also, the operations of HSP were chosen because they're crucial for the development of free models!

This is another thing that I didn't internalize so thanks for bringing it up. My understanding of universal algebra comes from the syntactical side, so to me, varieties are important because they are equational and the HSP theorem is just an abstract characterization of that. I see why free models might be important, but they come second to the algebraic presentation in my mind. I guess your comment also helps me make sense of something that irked me in universal algebra books: the fact that they introduce equations way later than I would. Btw, you only need subalgebras and products for free models.

Steve Awodey (Aug 01 2024 at 22:12):

The HSP Theorem is a proto-version of Lawvere's theorem that the algebras for a finitary monad on $\mathsf{Set}$ are (equivalent to) the finite-product-preserving, $\mathsf{Set}$-valued functors on the dual of the finitely generated free algebras. This theorem doesn't require that we know the signature in advance.

Chris Grossack (they/them) (Aug 01 2024 at 23:54):

@Steve Awodey How can you use Lawvere's theorem about finite product theories to compute the "varietal closure" of fields? The HSP theorem makes this obvious (just close under H, S, and P) but it's not clear to me how you would go from fields to something equational using just Lawvere's theorem. I'm willing to believe there's a way, I just don't have time to figure it out myself right now

Vincent Moreau (Aug 02 2024 at 01:30):

Chris Grossack (they/them) said:

Say you have some collection of algebraic gadgets that you like. It's obvious to wonder if there's some (equational) axiomatization of these gadgets. The first thing the HSP tells you is that there's an easy thing to check!

I disagree with you there (on a friendly level!). I tried to learn about the HSP theorem a while ago and I was a bit puzzled about how to use it. This is how I understood.

To any (first order) signature $\Sigma = \{a_1 : n_1, \dots, a_l : n_l\}$ of symbols with their associated finite arity, one can associate a category $\mathbf{Alg}(\Sigma)$ whose objects are sets $X$ equipped with functions $X^{n_i} \to X$. Let us suppose that you are interested in a specific category $\mathbf{C}$, and you have a signature $\Sigma$ and a full and faithful functor $E : \mathbf{C} \to \mathbf{Alg}(\Sigma)$ which I think of as an encoding. Then the HSP theorem tells you that the predicate of belonging to the image of $E$ is definable in terms of equations between terms on the signature $\Sigma$ if and only if the image of $E$ is closed under H, S and P.

If you have a specific category $\mathbf{C}$ in mind, and there are natural candidates for $\Sigma$ and $E : \mathbf{C} \to \mathbf{Alg}(\Sigma)$ whose image is not closed by H or S or P, then this only means that you cannot see $\mathbf{C}$ as the full subcategory some $\Sigma$ structures verifying some equations. But this says nothing about other choices of a signature $\Sigma$ and an encoding $E$...

Vincent Moreau (Aug 02 2024 at 01:31):

This is a thought that I developed a bit in isolation, against the usual claims regarding the HSP theorem. Therefore, if someone sees something wrong, please tell me!

Chris Grossack (they/them) (Aug 02 2024 at 05:08):

Sure, but this is a kind of different question! I agree that HSP is more useful if you know in advance what your signature is. But for the kinds of algebraic structures on encounters in practice (or at least, the algebraic structures which classical universal algebraists encountered in practice) you usually have a signature in mind already!

Chris Grossack (they/them) (Aug 02 2024 at 05:10):

This makes me wonder, though -- is there a class of structures which is equational with respect to one signature but not another? The answer is probably yes, but I'm about to go to bed, and we're quickly reaching the outer edges of my universal-algebraic knowledge

Vincent Moreau (Aug 02 2024 at 05:11):

I think that you can take groups and encode them as monoids. This gives you a full subcategory, but it is not stable by subobjects (in the category of monoids). However, if you add the inverse in the signature, it is equational :)

Chris Grossack (they/them) (Aug 02 2024 at 05:11):

This is a more down-to-earth version of the problem you bring up @Vincent Moreau where we think of embedding some abstract category into a category of structures for some signature. But maybe this is down-to-earth enough that some old universal algebraist has thought about it

Chris Grossack (they/them) (Aug 02 2024 at 05:12):

oh wow, that's a really easy example! Thanks ^_^. I guess in that case the equational closure is probably all monoids, right? Being cancellative isn't an equational property

Chris Grossack (they/them) (Aug 02 2024 at 05:13):

yeah, because a free group contains a free monoid as a submonoid, and then you get everything by quotients

Vincent Moreau (Aug 02 2024 at 05:14):

Ah yes, indeed!

Ralph Sarkis (Aug 02 2024 at 06:07):

Steve Awodey said:

The HSP Theorem is a proto-version of Lawvere's theorem that the algebras for a finitary monad on Set are (equivalent to) the finite-product-preserving, Set-valued functors on the dual of the finitely generated free algebras. This theorem doesn't require that we know the signature in advance.

You also need that finitary monads on $\mathsf{Set}$ are precisely the free algebra monads for finitary algebraic theories right? Does the theorem you state already entail this? Or maybe you are saying that the essence of the HSP theorem isn't really about syntax and equations, and we should see this essence in Lawvere's formulation.

Steve Awodey (Aug 03 2024 at 18:28):

Ralph Sarkis said:

Steve Awodey said:

The HSP Theorem is a proto-version of Lawvere's theorem that the algebras for a finitary monad on Set are (equivalent to) the finite-product-preserving, Set-valued functors on the dual of the finitely generated free algebras. This theorem doesn't require that we know the signature in advance.

You also need that finitary monads on $\mathsf{Set}$ are precisely the free algebra monads for finitary algebraic theories right? Does the theorem you state already entail this?

that follows. See e.g. Theorem 1.2.19 in these notes - or many other places.

Ralph Sarkis (Aug 03 2024 at 20:23):

I meant algebraic theory in the classical sense (signature + equations), but thinking about it more, I should have asked another question. In the language of your notes (which btw were the first to make me understand Lawvere theories when I found them): Does the fact that Lawvere algebraic categories are equivalent to $\mathsf{Syn}(\mathbf{T})$ for some algebraic theory $\mathbb{T}$ (you discuss this fact without proof near (1.18)) follow from Theorem 1.2.19?

Again, this comes from my biased point of view that the HSP theorem is about equations, but I understand this is not your point of view. Do you have references for more discussion on seeing the HSP theorem as a proto monad-theory correspondence?

Unfortunately, I don't have a functorial semantics version of my generalization of algebraic theories, neither do I have a monad-theory correspondence (yet? :fingers_crossed:).

Steve Awodey (Aug 03 2024 at 20:49):

Ralph Sarkis said:

I meant algebraic theory in the classical sense (signature + equations), but thinking about it more, I should have asked another question. In the language of your notes (which btw were the first to make me understand Lawvere theories when I found them): Does the fact that Lawvere algebraic categories are equivalent to $\mathsf{Syn}(\mathbf{T})$ for some algebraic theory $\mathbb{T}$ (you discuss this fact without proof near (1.18)) follow from Theorem 1.2.19?

it follows from the construction of a Lawvere algebraic theory $\mathsf{Syn}(\mathbb{T})$ from a (syntactically presented) algebraic theory $\mathbb{T}$ in 1.1.2, and the converse construction described explicitly in the notes near (1.18). There's nothing left "without proof".

Tom Hirschowitz (Aug 06 2024 at 06:53):

Chris Grossack (they/them) said:

Steve Awodey How can you use Lawvere's theorem about finite product theories to compute the "varietal closure" of fields? The HSP theorem makes this obvious (just close under H, S, and P) but it's not clear to me how you would go from fields to something equational using just Lawvere's theorem. I'm willing to believe there's a way, I just don't have time to figure it out myself right now

@Chris Grossack (they/them)'s comment convinces me I don't really understand @Steve Awodey's comment either. Can anyone help?

Matt Earnshaw (Aug 06 2024 at 10:15):

I guess it's helpful (necessary?) to back up from the equivalence to the adjunction from which it restricts, as this gives us the desired 'closure operator'. The adjunction is between theories (considered with their bijective on objects functor from $N(op)$) and the slice $\textbf{Cat}/\text{Set}$ (restricted to those $U$ such that all $[U^n, U]$ are small, sometimes this is called 'tractable'). The induced equivalence restricts the latter to categories monadic over $\text{Set}$ for a finitary monad. But the point is that you can get a theory out of any tractable $A \to \text{Set}$, even when this is not the forgetful functor from a category of models. There are quite a few examples in III.1 of Lawvere's thesis (e.g. division rings), where the details of the adjunction can also be found.

Tom Hirschowitz (Aug 06 2024 at 10:24):

Ah, that's helpful, thanks, we know where to look now!