Given a category $\mathcal{C}$, its free coproduct completion (or free sum completion) is the category $PSh_{\sqcup}(\mathcal{C})$ (often denoted $Fam(\mathcal{C})$, for families in $\mathcal{C}$) obtained by freely adjoining coproducts of all objects of $\mathcal{C}$.
Here are a few concrete realizations of free coproduct completions.
The following explicit description of the coproduct completion is pretty immediate and seems to be part of category theory folklore (for instance the way it is referred to in Carboni, Lack & Walters (1993), Proof of Prop. 2.4). Early references include BΓ©nabou (1985), Β§3, see also Hu & Tholen (1995), p. 281, 286.
An explicit description of the free coproduct completion $PSh_{\sqcup}(\mathcal{C})$ of a category $\mathcal{C}$ is:
Its objects are dependent pairs consisting of
an $I$-indexed set $\big( X_i \in \mathcal{C} \big)_{i \in I}$ of objects of $\mathcal{C}$.
Its morphisms $\big( X_i \big)_{i \in I} \xrightarrow{ \; ( \phi_i )_{i \in I} \; } \big( Y_j \big)_{j \in J}$ pairs consisting of
a function of index sets $f \,\colon\, I \to J$.
an $I$-indexed set of morphisms $\phi_i \,\colon\, X_i \xrightarrow{\;} Y_{f(j)}$ in $\mathcal{C}$.
The composition-law and identity morphisms are the evident ones.
The following is also pretty immediate and essentially discussed in BΓ©nabou (1985), Β§3 (though without mentioning of the term βGrothendieck constructionβ).
The free coproduct completion of a category $\mathcal{C}$ is equivalently the Grothendieck construction
on the contravariant pseudofunctor on Set which sends a set $S$ to the $S$-indexed product category of $\mathcal{C}$ with itself (equivalently: to the functor category into $\mathcal{C}$ out of the discrete category on $S$):
where the base change-functors $f^\ast$ are given (on functor categories by precomposition with $f$, hence) by:
Namely, by definition of the Grothendieck construction
its objects are dependent pairs of the form
its morphisms
are dependent pairs consisting of a map
and a morphism in $\underset{s \in S}{\prod} \mathcal{C}$ of the form
where, by definition (1) of $f^\ast$ and the nature of product categories, the latter is an $S$-indexed set $(\phi_s)_{s \in S}$ of morphisms in $\mathcal{C}$ of the form
But this is manifestly the same as the explicit description of $PSh_{\sqcup}(\mathcal{C})$ above.
The free coproduct completion of $\mathcal{C}$ is equivalently the full subcategory
of the category of presheaves over $\mathcal{C}$ on those which are coproducts of representables. The latter is the free cocompletion of $\mathcal{C}$ under all small colimits.
The Yoneda embedding hence factors through the free coproduct completion
Notice that the first inclusion here does not preserve coproducts (coproducts are freely adjoined irrespective of whether $\mathcal{C}$ already had some coproducts), but the second does. Both inclusions preserve those limits that exist.
Fairly immediate from the explicit definition above is:
A category $\mathcal{B}$ with small-indexed coproducts is equivalent to a free coproduct completion $PSh_{\sqcup}(\mathcal{C})$ for a small category $\mathcal{C}$ if
$\mathcal{C} \xhookrightarrow{\;} \mathcal{B}$ is a full subcategory of connected objects,
i.e. $X \,\in\, \mathcal{C} \hookrightarrow \mathcal{B}$ means that the hom-functor $\mathcal{B}(X,-) \,\colon\, \mathcal{B} \to Set$ preserves coproducts
(which when $\mathcal{C}$ is extensive means equivalently that if $X$ is a coproduct, then one of the summands is initial, by this Prop.);
each object of $\mathcal{B}$ is a coproduct of objects in $\mathcal{C} \hookrightarrow \mathcal{B}$.
Since, by assumption, the objects of $\mathcal{B}$ are already presented by indexed sets $\big(X_s\big)_{s \in S}$ of objects in $\mathcal{C}$, it is sufficient to see that under this presentation the morphisms
in $\mathcal{B}$ correspond bijectively to indexed sets of morphisms in $\mathcal{C}$ according to the explicit description of the free coproduct completion above. Indeed, using
the general fact that hom-functors take coproducts in the first argument to products
the defining property that the resulting hom-functors out of connected objects take coproducts in the second argument to coproducts,
we obtain the following sequence of natural bijections
The free coproduct completion of an accessible category is itself accessible.
Any free coproduct completion is an extensive category.
For $\mathcal{C}$ a category with all Cartesian products, its free coproduct completion $PSh_{\sqcup}(\mathcal{C})$ also has products and they distribute over the coproducts.
This is readily seen by component inspection, but it may be instructive to see it from more abstract reasoning:
Namely, with the free cocompletion understood as a Grothendieck construction, $PSh_{\sqcup}(\mathcal{C}) \,\simeq\, \int_{S \in Set} \mathcal{C}^S$ discussed above, its cartesian produducts are computed by the general formula for limits in Grothendieck constructions (here) as the βexternal cartesian productβ (here, we now show binary products only, just for ease notation):
Of course this comes down to the expected component formula
Similarly, the component formula for the free coproduct is
Using all this, distributivity is verified as follows:
It seems plausible, that, more abstractly, Prop. follows because the 2-monad for free product completion would distribute over the 2-monad for free coproduct cocompletion; the composite 2-monad would exhibit the free distributive category-construction. We donβt currently have a proof or reference for these statements, though.
The following examples follow as special cases of Prop. :
The category Set is the free coproduct completion of the terminal category.
(skeletal groupoids form the free coproduct completion of groups)
The 1-category of skeletal groupoids among that of all strict groupoids is the free coproduct completion of the category of 1-object delooping groupoids which (as 1-categories) is equivalently the category of groups:
($G$-sets are the free coproduct completion of $G$-orbits)
Let $G \,\in\, Grp(Set)$ be a discrete group. Write
$G Set$ for its category of group actions on sets,
$G Orbt \xhookrightarrow{\;} G Set$ for its orbit category, the full subcategory on the transitive actions, hence the sets of cosets $G/H$, for subgroups $H \subset G$.
Since every G-set $X$ decomposes as a disjoint union of transitive actions, namely of orbits of elements of $X$, this inclusion exhibits $G Set$ as the free coproduct completion of G Orbt.
(coproduct completion of extensive categories)
While Prop. says that every free coproduct completion is extensive, if a category $\mathcal{C}$ is already extensive to start with then its free coproduct completion may equivalently be described as the category of $\mathcal{C}$-bundles over sets, the latter regarded as objects of $\mathcal{C}$ via the unique coproduct-preserving functor $\iota_{Set} \,\colon\, Set \longrightarrow \mathcal{C}$, hence as the comma category $\mathcal{C}_{Set} \,\coloneqq\, \big(id_{\mathcal{C}}, \iota_{Set}\big)$:
where on the right we are indicating a generic morphism of such bundles.
Namely, since every set is the coproduct of singleton sets indexed by its elements, and due to the defining property of an extensive category that the coproduct functors are equivalences between (products of) slice categories
it follows that:
every object $X_S$ of $\mathcal{C}_{\iota(S)}$ is of the form shown in (2) hence determined by a family $(X_s)_{s \in S}$,
morphisms as shown in (2) are equivalently (by the universal property of the pullback) morphisms of the form
(where we used pullback stability of coproducts in an extensive category, see there, to deduce that $f^\ast Y_S \,\simeq\, \underset{s \in S}{\coprod} f^\ast(Y_S)_s \,\simeq\, \underset{s \in S}{\coprod} Y_{f(s)}$)
which by extensitivity are equivalently $S$-indexed families $\phi_s\,\colon\, X_s \longrightarrow Y_{f(s)}$.
This is again manifestly the explicit description of the free coproduct completion from above.
Conversely this gives a sense that if a category $\mathcal{C}$ is not extensive, so that the notion of bundles with total spaces and fibers in $\mathcal{C}$ does not make sense, its free coproduct completion may be understood as the closest stand-in for that category of $\mathcal{C}$-bundles over sets.
Early discussion of the concept:
On accessibility of free coproduct completions:
On limits in free coproduct completions:
In the context of regular and exact completions:
In the general context of extensive categories:
As categorical semantics for dependent linear type theories (in the context of quantum programming languages with βdynamic liftingβ, such as proto-Quipper), the free coproduct completion of symmetric closed monoidal categories is considered in
Francisco Rios, Peter Selinger, Β§3.2 in: A Categorical Model for a Quantum Circuit Description Language, EPTCS 266 (2018) 164-178 [arXiv:1706.02630, doi:10.4204/EPTCS.266.11]
Peng Fu, Kohei Kishida, Peter Selinger, Linear Dependent Type Theory for Quantum Programming Languages, LICS β20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer ScienceJuly 2020 Pages 440β453 (arXiv:2004.13472, doi:10.1145/3373718.3394765, pdf, video)
and its followups.
Algebras in the free coproduct completion are considered in:
Last revised on May 31, 2024 at 12:47:51. See the history of this page for a list of all contributions to it.