Take the 2-minute tour ×

Consider the diagonal functor $\Delta_\mathcal{J} : \mathrm{Set} \to \mathrm{Set}^\mathcal{J}$, given by $\Delta_{\mathcal{J}}(X) = J \mapsto X$. This has left and right adjoints, which in the case that $\mathcal{J}$ is discrete we may call $\Sigma_{\mathcal J} \dashv \Delta_{\mathcal J} \dashv \Pi_{\mathcal J}$; these represent "$\mathcal J$-indexed coproduct" and "$\mathcal J$-indexed product" of sets, respectively. For example, $\Sigma_{\mathcal J} F = \coprod_{j \in \mathcal J} F(j)$.

Now consider the groupoid $\mathbb{B}$ of finite sets and bijections. Unlike $\mathrm{Set}$, $\mathbb{B}$ has no products or coproducts (any category with all products or coproducts is necessarily connected). However, it is monoidal in (at least) two ways, given by disjoint union and Cartesian product of finite sets. For discrete $\mathcal J$ with a finite set of objects, we can construct an analogue to $\Sigma_{\mathcal J}$ in $\mathbb{B}$, namely, $\Sigma^{\mathbb{B}}_{\mathcal J} : \mathbb{B}^{\mathcal J} \to \mathbb{B}$, which intuitively "acts just like $\Sigma_{\mathcal J}$"; this works because disjoint union is functorial in $\mathbb B$ and preserves finiteness. However, I am not sure how to formally relate $\Sigma_{\mathcal J}$ and $\Sigma^{\mathbb{B}}_{\mathcal J}$. Since $\mathbb B$ does not have coproducts, $\Sigma^{\mathbb B}_{\mathcal J}$ does not arise as a left adjoint to $\Delta_{\mathcal J}$. We can define a functor $\Sigma_{\mathcal J}(U \circ -) : \mathbb B^{\mathcal J} \to \mathrm{Set}$ (where $U : \mathbb B \to \mathrm{Set}$ is the forgetful functor), but extending this to a functor $\mathbb B^{\mathcal J} \to \mathbb B$ seems problematic since there are no interesting functors $\mathrm{Set} \to \mathbb B$; intuitively, $\Sigma_{\mathcal J}(U \circ -)$ "forgets" too much.

Is there a "nice" way to construct $\Sigma^{\mathbb B}_{\mathcal J}$? My real goal is to generalize this to other categories besides $\mathbb B$; so, more generally, what properties does a monoidal category $(\mathcal{C},\oplus,0)$ need to have in order to be able to define some sort of "indexed monoidal product" $\bigoplus_{\mathcal J} : \mathcal C^{\mathcal J} \to \mathcal C$?

share|improve this question
Check out ncatlab.org/nlab/show/copower –  John Wiltshire-Gordon Apr 29 '14 at 17:09
Care to expand on how copowers fit in? As far as I can tell, the main theorems that show that they exist fail in Brent's setup as described above. [I can see that they are related, just not that they actually answer the question as posed.] –  Jacques Carette Apr 29 '14 at 19:49
Brent, I have no idea of what you are trying to achieve, but I can tell you what you are doing. First, forget about $\mathbf{Set}$, because you are talking about finite sets. So, you have observed that the category of finite sets $\mathbf{FinSet}$ has finite products. Finite products in $\mathbf{FinSet}$ are generated by the (strong) monidal structure $\langle 1, \times \rangle$ on $\mathbf{FinSet}$. (cont) –  Michal R. Przybylek Apr 29 '14 at 20:48
Because your grupoid $\mathbb{B}$ consists of all objects from $\mathbf{FinSet}$, and every functor preserves isomorphisms, this (strong) monoidal structure restricts to a monoidal structure on $\mathbb{B}$. Now, what kind of generalization are you looking for? Obviously, you may replace $\mathbf{FinSet}$ by any category with any (strong) monoidal structure, and everything will remain true. –  Michal R. Przybylek Apr 29 '14 at 20:48
@BrentYorgey: you say in the first comment that you don't want to use the "pick some ordering of J, then use this to take the J-iterated monoidal product" approach, because you're working in a constructive setting. However, what definition of "finite" are you using for J? In such settings there are several options for this‌​? If you assume that J is cardinal-finite, then you can use the indexed-monoidal-product approach without difficulty. In fact, I may expand this into an answer. –  Peter LeFanu Lumsdaine Apr 29 '14 at 21:50

1 Answer 1

up vote 5 down vote accepted

You say you are working in a constructive setting, so I will do the same.

Suppose $J$ is a cardinal-finite set; that is, there exists some $n \in \mathbb{N}$ such that $J \cong \{1,\ldots,n\}$.

Then for any symmetric monoidal category $\newcommand{\C}{\mathcal{C}} (\C,\otimes,\mathbb{1})$, there is an anafunctor $\otimes_J : \C^{J} \to \C$, implementing the "$J$-indexed monoidal product". If $\otimes$ is binary product (resp. coproduct), then $\otimes_J$ will be the $J$-indexed product (resp. coproduct) in $\C$. Moreover, this is pseudo-functorial in bijections $\sigma : J \to J'$, and also associative and unital in appropriate senses.

An anafunctor $F : \C \to \mathcal{D}$ is a span of categories and functors $\C \leftarrow \bar{F} \rightarrow \mathcal{D}$, such that $\bar{F} \to \C$ is full, faithful, and surjective on objects; intuivitively, it is a functor whose values are defined only up to isomorphism, with $\bar{F}$ being the category of "objects of $\C$ together with a chosen value of $F(\C)$".

(Assuming AC, such $\bar{F} \to \C$ must admit a section, and hence any anafunctor can be replaced by an actual functor. Without AC, however, anafunctors are for many purposes a better notion.)

In our case, define $\overline{\otimes_J}$ to be the category in which an object $(\vec{C},n,b)$ consists of an object $\vec{C}$ of $\C^J$, together with a natural number $n$ and a bijection $b : J \to \{1,\ldots,n\}$; while an arrow $(f,g) : (\vec{C},n,b) \to (\vec{C}',n',b')$ consists of an arrow $f \colon \vec{C} \to \vec{C}'$ in $\C^J$, together with a bijection $g \colon \{1,\ldots,n\} \to \{1,\ldots,n'\}$ such that $g \circ b = b'$. The left leg $\overline{\otimes_J} \to \C^J$ then simply forgets most of the data, while the right leg $\overline{\otimes_J} \to \C$ constructs iterated monoidal products using the orderings provided by the $(n,b)$ part.

As other commenters have mentioned, powers and copowers (aka cotensors and tensors) are an alternative direction in which you can generalise finite products and coproducts. However, I don't know a way to see your example $\mathbb{B}$ as an instance of these.

share|improve this answer
Thanks! This isn't the first time the issue of constructive finiteness has come up for me, but I hadn't quite yet made the connection. Indeed, I have been using cardinal-finiteness, so this fits perfectly. –  Brent Yorgey Apr 29 '14 at 23:52

Your Answer


