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: learning: questions

Topic: Free Algebras of Multisorted Equational Theories

Alex Goodlad (Aug 01 2021 at 02:09):

So I've been looking to write a (hopefully publishable) paper related to universal (co)algebras and category theory, and one of the things I've always wondered since I was a senior in college writing my undergrad thesis is what the heck is a "free cartesian (closed) category" generated by a graph (or whatever other object that forgets some kind of structure). My undergrad adviser really wanted me to use this construction at the time, but I was just not satisfied with Lambek and Scott's justification that they exist (and still am not completely), let alone the exposition of them. And for the longest time (not really knowing about adjunctions at that time didn't help matters), I've never found an answer that completely satisfied me.

Fastforward five years later. I of course gained some knowledge about the adjoint functor theorem being able to show the existence of a right adjoint $R: \mathcal{C} \to \mathcal{D}$ of a certain "forgetful functor" $U: \mathcal{D} \to \mathcal{C}$ (that satisfies the hypotheses of the theorem), which seems to be the most powerful tool to justify the existence of a "free object $RX$ of category $\mathcal{D}$ generated by an object $X$ of category $\mathcal{C}$". However, it doesn't provide much of an idea what a given free object is other than the initial object of the comma category $X/U$, but that begs the question of "what exactly is that particular initial object that we know exists."

What I seem to be looking for is an explicit construction of an object in a given comma category--such as how the group of "words" of a set $X$ (i.e. strings of elements of $x \in X$ and "inverse-elements" $x^{-1}$) that turns out to be the "free group generated by $X$"--that we can point to and say "that's the initial object".

Concerning free categories with extra structure (such as products, coproducts, monoids, and exponentials) generated by a graph, I think I've stumbled upon a way on my own to do it that is similar to the explicit "free group", "free module", and even "free category" construction, and this method generalizes to any category that is a variety $\mathcal{V}_T$ of an equational theory $T$ of a (possibly multisorted) signature $\Sigma$. To make the long story short, it involves observing that there is a quotient functor $Q: Alg_\Sigma \to \mathcal{V}_T$ that splits the subfunctor $\mathcal{V}_T \hookrightarrow Alg_\Sigma$, and observing that $Q$ being full implies preservation of initial objects. We know that the initial object of $Alg_\Sigma$ are the $\Sigma$-terms, so the initial object of $\mathcal{V}_T$ are the $\Sigma$ terms-modulo the theory $T$. This fact along with the fact that for the forgetful functor $U:Alg_\Sigma \to Set^n$ ($n$ the number of sorts of $\Sigma$) and $\mathbf{X}:=(X_1,\ldots,X_n) \in Set^n$, we have

$\mathbf{X}/U \cong Alg_{P_{\Sigma}+\mathbf{X}} \cong Alg_{\Sigma(\mathbf{X})},$

where $P_{\Sigma}:Set^n \to Set^n$ is the (multivariable) polynomial functor of $\Sigma$ and $\Sigma(\mathbf{X})$ is the signature containing $\Sigma$ along with a $k$-sorted constant symbol for every $x_k \in X_k$, we end up with an explicit construction of "free algebras of a multisorted equational theory" that is to my personal satisfaction.

This construction I'm pretty sure works for categories (with any additional structure) since category theory can be formalized as a 2-sorted equational theory (granted this construction requires some accommodation for the fact that composition is a partial function but this accommodation I'm very certain can be done), and graphs are exactly the 2-sorted algebras with the signature of two "source" and "target" function symbols. I've even heard categories can be 1-sorted equational theories as well, but personally I find it most natural (and hopefully you all do as well) to talk about category theory in a 2-sorted language. And it seems you can go as far as topoi with what kind of added structure (like products and coproducts) you add to your theory while still keeping it equational.

I guess my question is--as one who honestly does not have as good a handle on what literature is out there on equational logic and universal algebra as I should--what has currently been published about this kind of stuff, and what perspective have I possibly discovered here that's new and/or interesting? I know that MaClane V.6 talks about free equational algebras of a theory $T$ (of a one sorted signature) existing, and implicitly proves their existence in VI.8 (basically a corollary of Theorem 1 and the Adjoint Functor Theorem). This extends pretty easily to multiple sorts. And I know Lambek and Scott (as I referred to before) does give a similar kind of explicit construction that I am (except phrased from a logical perspective as "proof equivalence classes" rather than "term equivalence classes"). But what else have people done involving explicit constructions of free algebras, as well as looking at category theory from an equational perspective to talk about say, the free cartesian closed category generated by a graph? And what sort of literature should I further inquire?

Not sure if this question more fits the "learning: recommendations" or "learning: questions" stream. It could go either way depending on whether the answers of this thread end up centering more around my personal discoveries, or more around literature recommendations that fits this research interest.

Patrick Nicodemus (Aug 01 2021 at 04:41):

Do you have any experience with applications of monads in universal algebra? The book "Algebraic Theories" by Manes might be relevant. I don't think it deals with the multisorted case.

Morgan Rogers (he/him) (Aug 01 2021 at 10:39):

There is a LOT of work on constructing free algebras for equational theories, as Patrick says. Explicit constructions of free "categories with structure", however, are lacking; @Nathanael Arkor and I have an ongoing backburner project on that topic.
The reason the algebraic approach doesn't extend easily is not the multisortedness of the theory of categories or the fact that the operations are partial, but rather that the structure involved is not merely equational. You can produce the formal setting to present "pullback" as an operation; it takes a cospan and outputs a suitable span, but the universality requirement on the span is not equational, since it requires talking about "all suitable spans".

Most of the constructions of "free categories with structure" (e.g. with finite colimits) take advantage of the Yoneda embedding, and the result is very much not explicit, so I understand your motivation.

It's worth giving a word of caution that you must be aware of the difference between "free category with X" and "free X-completion of a category". The former ignores any existing X structure in the category, while the latter preserves the existing X structure (so is typically idempotent if it exists). You might already be familiar with that idea, but it's always worth pointing out, since the Yoneda embedding is good for building free limit completions of categories, and on the other hand for building free categories with colimits on a given category; you need to perform the dual Yoneda embedding or a combination of the two for other types of free structure.

Fawzi Hreiki (Aug 01 2021 at 10:57):

Awodey's category theory book has a (partial) equational presentation of the theory of Cartesian closed categories.

Fawzi Hreiki (Aug 01 2021 at 10:58):

More generally, if I recall correctly, Freyd’s ‘Aspects of Topoi’ notes have equational presentations of CCCs and of toposes

Fawzi Hreiki (Aug 01 2021 at 11:04):

There's a theorem that essentially equational theories are precisely those theories given by chains of monads over $\text{Set}$. For example how the category of (small) categories is monadic over reflexive directed graphs.

Nathanael Arkor (Aug 01 2021 at 16:45):

One paper I'd recommend, which sounds relevant to your motivating interest, is Nishizawa–Power's Lawvere theories enriched over a general base, where they give an explicit presentation of a 2-monad for cartesian-closed categories. This is the free cartesian-closed category on a category, rather than a graph, but it should be straightforward to adapt to your setting.