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: Categorical treatments for Palmgren & Vickers' Cartϖ

Yuto Ikeda (Dec 20 2025 at 12:49):

In Section 8.2 in Palmgren and Vickers' "Partial Horn logic and cartesian categories", they consider a unary operation $\mathrm{Cart\varpi}$ on quasi-equational theories (which are equiavelnt to essentially algebraic theories). For a quasi-equational theory $\mathbb{T}$, another, denoted $\mathrm{Cart\varpi} \mathbb{T}$, is designed as follows: models of $\mathrm{Cart\varpi} \mathbb{T}$ in $\mathbf{Set}$ are pairs $(\mathcal{C}, M)$ of a cartesian category $\mathcal{C}$ and a model $M$ of the theory $\mathbb{T}$ in $\mathcal{C}$. (Here, cartesian categories refers to categories with finite limits.) In short, $\mathrm{Cart\varpi} \mathbb{T}$ is "the theory of cartesian categories equipped with a model of $\mathbb{T}$".

Although their motivation for introducing $\mathrm{Cart\varpi} \mathbb{T}$ is to obtain a simple construction of classifying (syntactic) categories, if we abstract away from this motivation and identify quasi-equational theories with their classifying categories, $\mathrm{Cart\varpi}$ can be viewed as an operation on cartesian categories. I wonder if there are any categorical treatments (characterization or known properties) on this operation $\mathrm{Cart\varpi}$.

For instance, $\mathrm{Cart\varpi}$ seems to naturally form an endofunctor on the (2-)category of cartesian categories. Moreover, it seems to be a pointed endofunctor (i.e., there is a natural transformation $\mathrm{id} \Rightarrow \mathrm{Cart\varpi}$) via an "externalization" process: for pairs $(\mathcal{C}, M)$ as described above, we obtain a $\mathbf{Set}$-model $\Gamma_\mathcal{C} [M]$ of $\mathbb{T}$ by sending $M$ along the global section functor $\Gamma_\mathcal{C} = \mathcal{C} (1, -) \colon \mathcal{C} \to \mathbf{Set}$. This sends $\mathbf{Set}$-models of $\mathrm{Cart\varpi} \mathbb{T}$ to $\mathbf{Set}$-models of $\mathbb{T}$, which suggests it is induced by a morphism of theories $\mathbb{T} \to \mathrm{Cart\varpi} \mathbb{T}$. However, I don't know if $\mathrm{Cart\varpi}$ forms a (2-)monad.

Thanks for any suggestions!

John Baez (Dec 20 2025 at 14:03):

Am I correct that the quasi-equational theory $\mathbb{T}$ gives a finite limits category $\cal{T}$ (what you call a cartesian category) such that the category of models of $\mathbb{T}$ in any finite limits category $\mathcal{C}$ is equivalent to $[\mathcal{T}, \mathcal{C}]$ which is the category where

• objects are finite-limits-preserving functors $\mathcal{T} \to \mathcal{C}$
• morphisms are natural transformations

? If so, this is a hom-category in $\mathbf{Cart}$, the 2-category of finite limits categories.

(I avoid using "[[cartesian category]]" to mean a category with finite limits, since it's widely used to mean something else - click the link to see what I mean. But above I'm going along with you in using $\mathbf{Cart}$ to mean the 2-category of categories with finite limits.)

John Baez (Dec 20 2025 at 14:06):

If so, it seems that a pair $(\mathcal{C}, M)$ of the sort you're talking about - a finite limits category $\mathcal{C}$ and a model $M$ of the theory $\mathbb{T}$ in $\mathcal{C}$ - is the same as an object in $\mathcal{T} \downarrow \mathbf{Cart}$, the 2-category of finite limits categories equipped with a finite-limits-preserving functor from $\mathcal{T}$. This is an "under 2-category" or "coslice 2-category". And that's a good thing.

Yuto Ikeda (Dec 20 2025 at 15:01):

Thank you for the reply.

John Baez said:

Am I correct that the quasi-equational theory $\mathbb{T}$ gives a finite limits category $\cal{T}$ (what you call a cartesian category) such that the category of models of $\mathbb{T}$ in any finite limits category $\mathcal{C}$ is equivalent to $[\mathcal{T}, \mathcal{C}]$ which is the category where

• objects are finite-limits-preserving functors $\mathcal{T} \to \mathcal{C}$
• morphisms are natural transformations

?

Yes, this is exactly what I mean by the "classifying (or syntactic) category" of the theory $\mathbb{T}$. (Strictly speaking, the original paper defines classifying categories not merely up to equivalence but as specific strict categories, and distinguishes them from syntactic categories in terms of functors preserving finite limits strictly. But this point is not central to my question, so I use the terms interchangeably.)

John Baez said:

If so, it seems that a pair $(\mathcal{C}, M)$ of the sort you're talking about - a finite limits category $\mathcal{C}$ and a model $M$ of the theory $\mathbb{T}$ in $\mathcal{C}$ - is the same as an object in $\mathcal{T} \downarrow \mathbf{Cart}$, the 2-category of finite limits categories equipped with a finite-limits-preserving functor from $\mathcal{T}$. This is an "under 2-category" or "coslice 2-category". And that's a good thing.

I see the point. In this language, I am interested in the (2-?) endofunctor $P: \mathbf{Cart} \to \mathbf{Cart}$ satisfying $[P(\mathcal{T}), \mathbf{Set}] \simeq \mathcal{T} \downarrow \mathbf{Cart}$ for any $\mathcal{T} \in \mathbf{Cart}$. This $P$ corresponds to the Palmgren-Vickers' $\mathrm{Cart\varpi}$ construction. I wonder if it is known or has been studied in a purely categorical context.

Edit: By the size problem, $\mathbf{Set} \not\in \mathbf{Cart}$ must hold, so the left-hand side $[P(\mathcal{T}), \mathbf{Set}]$ is not a hom-category in $\mathbf{Cart}$. I abuse this notation for large categories.

(I agree that the term "cartesian category" is somewhat ambiguous. Please allow me to stick to the terminology used in the original paper.)

Morgan Rogers (he/him) (Dec 25 2025 at 08:52):

@Yuto Ikeda I don't know why you brought Set into the picture (also, the equivalence in your last message doesn't look right to me, since the LHS is a 1-category while the second looks more naturally like a 2-category) but the size issue you observe applies nonetheless. Nonetheless, supposing you circumvent that by putting some constraints in, it's fun to consider whether this might be a monad (or perhaps a relative pseudomonad?)
The result of applying your functor is a finite limit category classifying internal categories containing a model of $\mathbb{T}$. So iterating, we have a model in an internal category in an internal category in some (external) category $\mathcal{C}$. So a "multiplication" to make this into a monad would need to take an internal category in an internal category and externality it in a way that preserves models of theories.
I think this amounts to an internal version of the Grothendieck construction and that the preservation of models of finite limit theories will be automatic BUT I think the existence of the internal Grothendieck construction depends on the existence of some colimits which are not assumed to exist, so I don't know how things will look for a generic finite limit category.
Perhaps someone else can weigh in :innocent:

Yuto Ikeda (Dec 29 2025 at 05:45):

@Morgan Rogers (he/him) Sorry for the late reply, and thank you for your important suggestions!

I agree with your point in general, and I am not sure if my formulation is the best. I think that the mismatch in the equivalence you pointed out arises from treating "the theory of categories" as a quasi-equational theory (1-theory), not as a 2-theory. Naively, the operation considered here should increase the dimension of the category: for a (1-)theory $\mathbb{T}$, then the theory of "categories equipped with an internal model of $\mathbb{T}$" seems to be appropriate to be viewed as a 2-theory.

However, the original paper constructs $\mathrm{Cart}\varpi \mathbb{T}$ as a specific quasi-equational theory (1-theory) to allow the general theory to be applied. Above all, in order to expect the functor to be a monad, it seems necessary to "strictify" $\mathrm{Cart}\varpi \mathbb{T}$ and treat it as a 1-category. Perhaps this might be a major hurdle for a purely categorical formulation.

Regarding multiplication, your suggestion sounds interesting. I had been focusing on functors induced on models, which led me to think about the construction in the opposite direction: that is, how to construct a "category equipped with an internal category equipped with an internal model" from just a "category equipped with an internal model". It would be great if the Grothendieck construction on the theory side works as you suggest, but I need to think further about it.

Nathanael Arkor (Dec 30 2025 at 18:00):

Morgan Rogers (he/him) said:

Yuto Ikeda I don't know why you brought Set into the picture (also, the equivalence in your last message doesn't look right to me, since the LHS is a 1-category while the second looks more naturally like a 2-category)

By definition, the models for an essentially algebraic theory are given by functors into Set. And there's no issue considering CartCat as a 1-category rather than a 2-category.

Nathanael Arkor (Dec 30 2025 at 18:07):

I think there are two relevant constructions here, from which the one Palmgren and Vickers consider is derived. The first is that there exists an finite limit theory $\mathcal L$ such that $\mathbf{Mod}(\mathcal L) \cong \mathbf{LexCat}$ (let me avoid "cartesian" because I think that should be reserved for finite products only). The second is that, given any finite limit theory $\mathcal T$ and any $\mathcal T$-model $M$, there exists a finite limit theory $\mathcal T[M]$ such that $\mathbf{Mod}(\mathcal T[M]) \cong M/\mathbf{Mod}(\mathcal T)$.

This second construction, then, corresponds to the statement that coslices of locally finitely presentable categories are themselves locally finitely presentable. One place this is studied in detail is @Axel Osmond's On coslices and commas of locally finitely presentable categories.

Nathanael Arkor (Dec 30 2025 at 18:09):

The construction you are interested in is then $\mathcal L[{-}] : \mathbf{LexCat} \to \mathbf{LexCat}$, which satisfies $\mathbf{Mod}(\mathcal L[{-}]) \cong ({-})/\mathbf{LexCat}$.

Nathanael Arkor (Dec 30 2025 at 19:03):

(I don't see that this sheds much light on whether $\mathcal L[{-}]$ is a monad; I would be interested to know if it turns out to be one.)