Dialectica categories and polynomial functors (Part 1)
Like many stories in math, this one is about building bridges: uniting the dialectica categories from Valeria’s 1991 doctoral thesis with David’s work on polynomial functors. I’ve been working with David on polynomial functors for two years now, so when I was placed in Valeria’s team at the AMS’s 2022 Mathematics Research Communities Conference Week on Applied Category Theory, it was only natural that I try to tie their two perspectives together. There, under the guidance of Valeria and her trusty deputy Jérémie Koenig, I had the pleasure of leading a mini-research team consisting of Samantha Jarvis and Joseph Dorta in connecting dialectica categories to polynomial functors. Our launchpad was Sean Moss’s talk from the 2022 Workshop on Polynomial Functors. In this first post of a series, I’ll start by reviewing his work, before giving you a peek at what we found; we’ll have even more to share next time.
1 Introduction
Like many stories in math, this one is about building bridges: uniting the dialectica categories from Valeria’s 1991 doctoral thesis with David’s work on polynomial functors. I’ve been working with David on polynomial functors for two years now (see our book draft or our lecture series), so when I was placed in Valeria’s team at the AMS’s 2022 Mathematics Research Communities Conference Week on Applied Category Theory, it was only natural that I try to tie their two perspectives together. There, under the guidance of Valeria and her trusty deputy Jérémie Koenig (Yale), I had the pleasure of leading a mini-research team consisting of Samantha Jarvis (Graduate Center, City University of New York) and Joseph Dorta (Louisiana State) in connecting dialectica categories to polynomial functors. Our launchpad was Sean Moss’s talk (and slides) from the 2022 Workshop on Polynomial Functors. In this first post of a series, I’ll start by reviewing his work, before giving you a peek at what we found; we’ll have even more to share next time.
2 Free sum and product completions
One of my favorite things about category theory is that if you want something, you can often get it for free.
Say you have a category \mathbb{C}, and you want it to have all (small) products, regardless of what products may or may not already exist in \mathbb{C}. So for every indexed family of objects (c_a)_{a\in A} in \mathbb{C}, we’ll just freely form their product \prod_{a\in A}c_a. As a product, \prod_{a\in A}c_a should come with projection maps \prod_{a\in A}c_a\to c_{a'} for each a'\in A. Then if \mathbb{C} already had a map c_{a'}\to d for some d\in\mathbb{C}, we could compose it with the projection map to get a composite map \prod_{a\in A}c_a\to c_{a'}\to d out of the product. But any such d could itself be part of a freely-formed product, and by the universal property of products, if we have an indexed family of such composite maps \left(\prod_{a\in A}c_a\to c_{a_b}\to d_b\right)_{b\in B} with each a_b\in A, these maps induce a single map \prod_{a\in A}c_a\to\prod_{b\in B}d_b with the data of the maps c_{a_b}\to d_b from the original \mathbb{C} for each b\in B.
When we freely add products to \mathbb{C}, the maps \prod_{a\in A}c_a\to\prod_{b\in B}d_b we just described are the only maps we can get. After all, when we get things for free, we mustn’t be greedy—we obtain only the consequences of what we asked for and nothing more. We call the category of these free products and the maps between them the free product completion of \mathbb{C}, denoted by \Pi\mathbb{C}. To summarize, an object in \Pi\mathbb{C} consists of
- an index set A and
- an indexed family of objects (c_a)_{a\in A} from \mathbb{C},
denoted as a product \prod_{a\in A}c_a; while a morphism \prod_{a\in A}c_a\to\prod_{b\in B}d_b consists of
- a backward function B\to A sending b\mapsto a_b and
- a forward morphism c_{a_b}\to d_b from \mathbb{C} for each b\in B.
Notice that the original category \mathbb{C} embeds into \Pi\mathbb{C} as a full subcategory under the identification c\mapsto\prod_{\ast\in\{\ast\}}c; in fact we will use c as shorthand for the object \prod_{\ast\in\{\ast\}}c from \Pi\mathbb{C}. Then it’s routine to check that \prod_{i\in I}c_i really is the categorical product of (c_i)_{i\in I} in \Pi\mathbb{C}. In fact, \Pi\mathbb{C} has all products—just merge the product signs: \prod_{i\in I}\prod_{a\in A_i}c_{i,a}\cong\prod_{(i,a)\in\sum_{i'\in I}\{i'\}\times A_{i'}}c_{i,a}. The isomorphism above is the first example of what will become a trend throughout this series: nested product signs (and, as it will turn out, sum signs) behave as you’d expect from working with products (and sums) of sequences.
We started with a category \mathbb{C}, freely added any product we could form, and ended up with a category with all products. So it makes sense to call \Pi\mathbb{C} the free product completion of \mathbb{C}: any functor from \mathbb{C} to a category with all products factors uniquely (up to the right notion of equivalence) through \mathbb{C}. If you’ve read David’s blog post on selection categories, this construction may seem very familiar. There, his selection category \left[\begin{smallmatrix}{\vphantom{f}p} \\ {\vphantom{f}p\:\mathbin{\triangleleft}\:\mathbb{C}} \end{smallmatrix}\right] for a (sufficiently expressive) polynomial functor p is a variant of the free product completion of \mathbb{C} that is in some sense internal to the category \mathbf{Poly} of polynomial functors. But we’ll focus on the external version of the story for now.
Meanwhile, we could have taken the free sum (coproduct) completion of \mathbb{C}, denoted by \Sigma\mathbb{C}, in much the same way. By duality, this is the same as taking (\Pi\mathbb{C}^\mathsf{op})^\mathsf{op}: the opposite of the product completion of the opposite of \mathbb{C}. But we denote the objects of \Sigma\mathbb{C} with a sum sign instead of a product sign. A morphism \sum_{i\in I}c_i\to\sum_{j\in J}d_j is then a forward function I\to J and a backward morphism from \mathbb{C} for each i\in I. Again \mathbb{C} embeds into \Sigma\mathbb{C} as a full subcategory; again \Sigma\mathbb{C} has all sums, given by merging nested sum signs.
But what if we want products and sums? Just add both, one at a time: \mathbb{C}\hookrightarrow\Pi\mathbb{C} to get products, \Pi\mathbb{C}\hookrightarrow\Sigma\Pi\mathbb{C} to get sums. We’ll call \Sigma\Pi\mathbb{C} the free sum and product completion of \mathbb{C}, except we won’t, because that’s far too many words, so we’ll stick to the symbols \Sigma\Pi\mathbb{C}. Below, we’ll characterize \Sigma\Pi\mathbb{C} concretely, but try to work it out on your own before you read ahead.
An object in \Sigma\Pi\mathbb{C} consists of
- an index set I of what we call positions,
- an indexed family of sets (A_i)_{i\in I} of what we call directions, and
- a doubly-indexed family (c_{i,a})_{i\in I,\,a\in A_i} of objects of \mathbb{C} called predicates,
denoted as a nested sum of products \sum_{i\in I}\prod_{a\in A_i}c_{i,a}. Meanwhile, a morphism \varphi\colon\sum_{i\in I}\prod_{a\in A_i}c_{i,a}\to\sum_{j\in J}\prod_{b\in B_j}d_{j,b} consists of
- a forward on-positions function \varphi\colon I\to J,
- a backward on-directions function \varphi^\sharp_i\colon B_{\varphi i}\to A_i for each i\in I, and
- a forward on-predicates morphism \varphi_{i,b}\colon c_{i,\varphi^\sharp_i b}\to d_{\varphi i,b} from \mathbb{C} for each i\in I and b\in B_{\varphi i}.
We know \Pi\mathbb{C} has all products and \Sigma\Pi\mathbb{C} all sums, but in fact \Sigma\Pi\mathbb{C} also has all products—here, once more, our familiarity with expanding products of sums of numbers serves us well, for we know to apply the distributive property: \prod_{i\in I}\sum_{a\in A_i}c_{i,a}\cong\sum_{\overline{a}\in\prod_{i\in I}A_i}\prod_{i\in I}c_{i,\overline{a}_i}. So whenever we encounter a nested \Pi\Sigma sign, we can turn it into a \Sigma\Pi sign instead. It follows that a product of sums of products can be written as just a sum of products, and therefore as an object in \Sigma\Pi\mathbb{C}.
You may be familiar with the positions and directions terminology used above from David’s work on polynomial functors. In fact, if we forget everything to do with the predicates in \mathbb{C} in our description of \Sigma\Pi\mathbb{C} above, then we are left with exactly the characterization of the category \mathbf{Poly}. Equivalently, we could let \mathbb{C} be the terminal category \mathbf{1} with 1 object and 1 morphism, so that the choices of predicates and on-predicate morphisms are automatic. So \Sigma\Pi\mathbf{1}\cong\mathbf{Poly}; moreover, there is a canonical functor \Sigma\Pi\mathbb{C}\to\mathbf{Poly} that forgets the predicates, sending \sum_{i\in I}\prod_{a\in A_i}c_{i,a}\mapsto\sum_{i\in I}\prod_{a\in A_i}\mathcal{y}\cong\sum_{i\in I}\mathcal{y}^{A_i}. Hence an object of \Sigma\Pi\mathbb{C} can be thought of as a polynomial functor endowed with a predicate from \mathbb{C} at every direction, which we will call a \mathbb{C}-predicated polynomial for short.
Once I learned all this from Sean Moss’s talk, my way forward was clear: check if everything else I knew about \mathbf{Poly} could be generalized to \Sigma\Pi\mathbb{C}.
3 Predicated monomials and dialectica categories
Some of the nicest polynomials \sum_{i\in I}\mathcal{y}^{A_i}\in\mathbf{Poly} are what we call monomials: those for which every A_i is isomorphic to some fixed set A, so that we can write them more compactly as I\mathcal{y}^A. We’ll call the full subcategory of \mathbf{Poly} spanned by these monomials \mathbf{Mo}. These monomials turn out to be quite useful all on their own: \mathbf{Mo} is exactly the category of bimorphic lenses introduced by Jules Hedges in Coherence for lenses and open games (2017) and Limits of bimorphic lenses (2018).
Another way to think about monomials is that they are (up to isomorphism) the objects in the image of the faithful functor \mathbf{Set}\times\mathbf{Set}^\mathsf{op}\to\mathbf{Poly} sending (J,B)\mapsto J\mathcal{y}^B. Notably, this functor has a left adjoint \mathbf{Poly}\to\mathbf{Set}\times\mathbf{Set}^\mathsf{op} sending \sum_{i\in I}\mathcal{y}^{A_i}\mapsto\left(I,\prod_{i\in I}A_i\right). If you’re only concerned with monomials, you could restrict this to an adjunction between \mathbf{Set}\times\mathbf{Set}^\mathsf{op} and \mathbf{Mo}. We’ll see why this adjunction is interesting to us shortly.
What does all this look like when we generalize from \mathbf{Poly}\cong\Sigma\Pi\mathbf{1} to \Sigma\Pi\mathbb{C}? A sensible definition for a \mathbb{C}-predicated monomial would then be a \mathbb{C}-predicated polynomial of the form \sum_{i\in I}\prod_{a\in A}c_{i,a}, where the set A no longer depends on the index i\in I. We could call the full subcategory of \Sigma\Pi\mathbb{C} spanned by the \mathbb{C}-predicated monomials \mathbf{Mo}(\mathbb{C}) (so \mathbf{Mo}(\mathbf{1})\cong\mathbf{Mo}).
So if \Sigma\Pi\mathbb{C} generalizes \mathbf{Poly}, and \mathbf{Mo}(\mathbb{C}) generalizes \mathbf{Mo} as a full subcategory of \mathbf{Poly}, then what generalizes \mathbf{Set}\times\mathbf{Set}^\mathsf{op} and its adjunction with \mathbf{Poly} above? Here’s what we propose: we define a category that we will rather mysteriously call \mathbf{Gd}(\mathbb{C}) (we’ll explain this name later) as follows. An object in \mathbf{Gd}(\mathbb{C}) consists of
- an index set I,
- an index set A, and
- a doubly-indexed family (c_{i,a})_{i\in I,\,a\in A} of objects in \mathbb{C},
denoted as a triple (I,A,c); while a morphism \psi\colon(I,A,c)\to(J,B,d) consists of
- a function \psi^\flat\colon I\to J,
- a function \psi^\sharp\colon B\to A, and
- a morphism \psi_{i,b}\colon c_{i,\psi^\sharp b}\to d_{\psi^\flat i,b} from \mathbb{C} for each i\in I and b\in B.
Notice that this is just like the characterization of \Sigma\Pi\mathbb{C}, except here neither the set A nor the function \psi^\sharp\colon B\to A depends on the index i\in I. Also note that \mathbf{Gd}(\mathbf{1})\cong\mathbf{Set}\times\mathbf{Set}^\mathsf{op}, so we are on the right track. Indeed, there is a faithful functor \mathbf{Gd}(\mathbb{C})\to\Sigma\Pi\mathbb{C} sending (J,B,d)\mapsto\sum_{j\in J}\prod_{b\in B}d_{j,b}, so that (up to isomorphism) the objects in its image are the \mathbb{C}-predicated monomials. It turns out this functor has a left adjoint \Sigma\Pi\mathbb{C}\to\mathbf{Gd}(\mathbb{C}) sending \sum_{i\in I}\prod_{a\in A_i}c_{i,a}\mapsto\left(I,\prod_{i\in I}A_i,\tilde{c}\right), where for each i'\in I and (a_i)_{i\in I}\in\prod_{i\in I}A_i we define \tilde{c}_{i',(a_i)_{i\in I}}=c_{i',a_{i'}}. Moreover, this adjunction restricts to an adjunction between \mathbf{Gd}(\mathbb{C}) and \mathbf{Mo}(\mathbb{C}).
And here is where Valeria’s research comes into play: if we take \mathbb{C}=\mathbf{2}, the walking arrow category with 2 objects and exactly 1 non-identity morphism between them, then \mathbf{Mo}(\mathbf{2}) and \mathbf{Gd}(\mathbf{2}) are precisely the dialectica categories \mathbf{D}(\mathbf{Set}) and \mathbf{G}(\mathbf{Set}), respectively, from Valeria’s thesis. (Hence the name \mathbf{Gd}: it hints at Girard, who inspired the construction of \mathbf{G}(\mathbf{Set}), and after whom \mathbf{G}(\mathbf{Set}) is named; at Gödel, on whose dialectica interpretation the dialectica categories are based; and also a bit at Valeria de Paiva herself.) Moreover, the idea to replace \mathbf{2} with some other category \mathbb{C} is not a new one: in Categorical multirelations, linear logic and petri nets, Valeria takes \mathbb{C} to be a monoidal closed poset (i.e. a lineale) \mathbb{L} and uses \mathbf{Gd}(\mathbb{L}) (which she denotes by \mathbf{M}_{\mathbb{L}}\mathbf{Set}) in order to study Petri nets—a notion she revisited much later with co-authors Elena Di Lavore and Wilmer Leal in Dialectica Petri nets.
In description: we found that Jules Hedges’s category \mathbf{Mo} of bimorphic lenses and Valeria’s dialectica category \mathbf{D}(\mathbf{Set}) are special cases of \mathbf{Mo}(\mathbb{C}) for \mathbb{C}=\mathbf{1} and \mathbb{C}=\mathbf{2}. In turn, \mathbf{Set}\times\mathbf{Set}^\mathsf{op}, as well as Valeria’s dialectica variants \mathbf{G}(\mathbf{Set}) and \mathbf{M}_{\mathbb{L}}\mathbf{Set}, are special cases of \mathbf{Gd}(\mathbb{C}) for \mathbb{C}=\mathbf{1} as well as \mathbb{C}=\mathbf{2} and \mathbb{C}=\mathbb{L} (in fact, \mathbf{1} and \mathbf{2} are themselves lineales). There is then a faithful right adjoint functor \mathbf{Gd}(\mathbb{C})\to\mathbf{Mo}(\mathbb{C}) which, when composed with the fully faithful functor identifying \mathbf{Mo}(\mathbb{C}) as a full subcategory of \Sigma\Pi\mathbb{C}, yields another faithful right adjoint \mathbf{Gd}(\mathbb{C})\to\Sigma\Pi\mathbb{C}. To cap it all off, \mathbf{Poly} is a special case of \Sigma\Pi\mathbb{C} for \mathbb{C}=\mathbf{1}. So the category of polynomial functors, the category of bimorphic lenses, and the dialectica categories are all variants of the same concept—the category \Sigma\Pi\mathbb{C} of \mathbb{C}-predicated polynomials; the category \mathbf{Gd}(\mathbb{C}) with which \Sigma\Pi\mathbb{C} forms an adjunction; or the full subcategory \mathbf{Mo}(\mathbb{C}) of \Sigma\Pi\mathbb{C} spanned by \mathbb{C}-predicated monomials, objects isomorphic to those in the image of the right adjoint \mathbf{Gd}(\mathbb{C})\to\Sigma\Pi\mathbb{C}. This is the bridge between dialectica categories and polynomial functors that we promised: we can think of \Sigma\Pi\mathbb{C} either as a category of \mathbb{C}-predicated polynomials or as a kind of dependent dialectica category. Our familiarity with polynomial functors and dialectica categories will help us discover more general properties of \Sigma\Pi\mathbb{C}.
4 Vertical-cartesian factorization
Before we wrap up, here’s one more property of \mathbf{Poly} that generalizes to \Sigma\Pi\mathbb{C}. Every morphism \varphi\colon\sum_{i\in I}\mathcal{y}^{A_i}\to\sum_{j\in J}\mathcal{y}^{B_j} in \mathbf{Poly} has a forward on-positions function \varphi\colon I\to J and, for each position i\in I, a backward on-directions function \varphi^\sharp_i\colon B_{\varphi i}\to A_i. If the on-positions function \varphi\colon I\to J is a bijection, we say that the original morphism \varphi in \mathbf{Poly} is vertical; if every on-directions function \varphi^\sharp_i\colon B_{\varphi i}\to A_i is a bijection, we say that \varphi is cartesian. Notice that every isomorphism in \mathbf{Poly} is both vertical and cartesian; in addition, vertical morphisms are closed are composition, as are cartesian ones. Most crucially, every morphism \varphi\colon\sum_{i\in I}\mathcal{y}^{A_i}\to\sum_{j\in J}\mathcal{y}^{B_j} factors uniquely (up to isomorphism) into a vertical morphism \varphi_\mathsf{vert}\colon\sum_{i\in I}\mathcal{y}^{A_i}\to\sum_{i\in I}\mathcal{y}^{B_{\varphi i}} whose every on-directions function is \varphi^\sharp_i\colon B_{\varphi i}\to A_i and a cartesian morphism \varphi_\mathsf{cart}\colon\sum_{i\in I}\mathcal{y}^{B_{\varphi i}}\to\sum_{j\in J}\mathcal{y}^{B_j} whose on-positions function is \varphi\colon I\to J. We say that \mathbf{Poly} admits vertical-cartesian factorization.
In the more general setting of \Sigma\Pi\mathbb{C}, where a morphism \varphi\colon\sum_{i\in I}\prod_{a\in A_i}c_{i,a}\to\sum_{i\in J}\prod_{b\in B_j}d_{j,b} has on-predicates morphisms in addition to on-positions and on-directions functions, we have to expand the definitions a little to make this work. A vertical morphism in \Sigma\Pi\mathbb{C} will still be a morphism \varphi whose on-positions function \varphi\colon I\to J is a bijection. But a cartesian morphism in \Sigma\Pi\mathbb{C} will be a morphism \varphi whose every on-directions function \varphi^\sharp_i\colon B_{\varphi i}\to A_i is a bijection and whose every on-predicates morphism \varphi_{i,b}\colon c_{i,\varphi^\sharp_i b}\to d_{\varphi i,b} is an isomorphism in \mathbb{C}. (Of course, in the special case of \mathbb{C}=\mathbf{1}, every morphism in \mathbf{1} is an isomorphism, so we recover the original definition of a cartesian morphism in \mathbf{Poly}.) We can verify that every isomorphism in \Sigma\Pi\mathbb{C} is both vertical and cartesian, that vertical and cartesian morphisms are each closed under composition, and that every morphism \varphi\colon\sum_{i\in I}\prod_{a\in A_i}c_{i,a}\to\sum_{j\in J}\prod_{b\in B_j}d_{j,b} from \Sigma\Pi\mathbb{C} factors uniquely (up to isomorphism) into a vertical morphism \varphi_\mathsf{vert}\colon\sum_{i\in I}\prod_{a\in A_i}c_{i,a}\to\sum_{i\in I}\prod_{b\in B_{\varphi i}}d_{\varphi i,b}, whose every on-directions function is \varphi^\sharp_i\colon B_{\varphi i}\to A_i and every on-predicates morphism is \varphi_{i,b}\colon c_{i,\varphi^\sharp_i b}\to d_{\varphi i,b}; and a cartesian morphism \varphi_\mathsf{cart}\colon\sum_{i\in I}\prod_{b\in B_{\varphi i}}d_{\varphi i,b}\to\sum_{j\in J}\prod_{b\in B_j}d_{\varphi i,b}, whose on-positions function is \varphi\colon I\to J. Hence \Sigma\Pi\mathbb{C} admits vertical-cartesian factorization in general. The significance of this factorization system is that whenever we are analyzing a morphism in \Sigma\Pi\mathbb{C}, we can always separate out its behavior on positions from its behavior on directions and predicates and study each individually before composing them back together.
5 A look ahead
In this post, we introduced \Sigma\Pi\mathbb{C} and discovered its role in generalizing both polynomial functors and the dialectica categories. This led us to port over the concepts of monomials and vertical-cartesian factorization from \mathbf{Poly} to \Sigma\Pi\mathbb{C}.
Next time, we’ll delve into what happens when \mathbb{C} is a monoidal category. We’ll see how each monoidal structure on \mathbb{C} induces several interesting monoidal structures on \Sigma\Pi\mathbb{C}, and how these monoidal structures play nicely with vertical-cartesian factorization.