Given a category , its free coproduct completion (or free sum completion) is the category (often denoted , for families in , but note the usage of this term also for the category of correspondences in e.g. Lurie 2009) obtained by freely adjoining coproducts of all objects of .
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 of a category is:
Its objects are dependent pairs consisting of
an -indexed set of objects of .
Its morphisms pairs consisting of
a function of index sets .
an -indexed set of morphisms for in .
The composition-law and identity morphisms are the evident ones.
The free coproduct completion of a category is equivalently the following comma category.
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 is equivalently the Grothendieck construction
on the contravariant pseudofunctor on Set which sends a set to the -indexed product category of with itself (equivalently: to the functor category into out of the discrete category on ):
where the base change-functors are given (on functor categories by precomposition with , hence) by:
Namely, by definition of the Grothendieck construction
its morphisms
are dependent pairs consisting of a map
and a morphism in of the form
where, by definition (1) of and the nature of product categories, the latter is an -indexed set of morphisms in of the form
But this is manifestly the same as the explicit description of above.
The free coproduct completion of is equivalently the full subcategory
of the category of presheaves over on those which are coproducts of representables. The latter is the free cocompletion of 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 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 with small-indexed coproducts is equivalent to a free coproduct completion for a small category if
is a full subcategory of connected objects,
i.e. means that the hom-functor preserves coproducts
(which when is extensive means equivalently that if is a coproduct, then one of the summands is initial, by this Prop.);
each object of is a coproduct of objects in .
Since, by assumption, the objects of are already presented by indexed sets of objects in , it is sufficient to see that under this presentation the morphisms
in correspond bijectively to indexed sets of morphisms in 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 a category with all Cartesian products, its free coproduct completion 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, 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:
(-sets are the free coproduct completion of -orbits)
Let be a discrete group. Write
for its category of group actions on sets,
for its orbit category, the full subcategory on the transitive actions, hence the sets of cosets , for subgroups .
Since every G-set decomposes as a disjoint union of transitive actions, namely of orbits of elements of , this inclusion exhibits 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 is already extensive to start with then its free coproduct completion may equivalently be described as the category of -bundles over sets, the latter regarded as objects of via the unique coproduct-preserving functor , hence as the comma category :
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 of is of the form shown in (2) hence determined by a family ,
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 )
which by extensitivity are equivalently -indexed families .
This is again manifestly the explicit description of the free coproduct completion from above.
Conversely this gives a sense that if a category is not extensive, so that the notion of bundles with total spaces and fibers in does not make sense, its free coproduct completion may be understood as the closest stand-in for that category of -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 August 27, 2024 at 20:29:40. See the history of this page for a list of all contributions to it.