ncatlab.org

free coproduct completion in nLab

Contents

Contents

Idea

Given a category 𝒞\mathcal{C}, its free coproduct completion (or free sum completion) is the category PSh ⊔(𝒞)PSh_{\sqcup}(\mathcal{C}) (often denoted Fam(𝒞)Fam(\mathcal{C}), for families in 𝒞\mathcal{C}, 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 𝒞\mathcal{C}.

Definitions

Here are a few concrete realizations of free coproduct completions.

Via indexed sets of objects

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 ⊔(𝒞)PSh_{\sqcup}(\mathcal{C}) of a category 𝒞\mathcal{C} is:

  • Its objects are dependent pairs consisting of

    1. an index set I∈I \in Set

    2. an II-indexed set (X i∈𝒞) i∈I\big( X_i \in \mathcal{C} \big)_{i \in I} of objects of 𝒞\mathcal{C}.

  • Its morphisms (X i) i∈I→(ϕ i) i∈I(Y j) j∈J\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:I→Jf \,\colon\, I \to J.

    • an II-indexed set of morphisms ϕ i:X i→Y f(i)\phi_i \,\colon\, X_i \xrightarrow{\;} Y_{f(i)} for i∈Ii \in I in 𝒞\mathcal{C}.

  • The composition-law and identity morphisms are the evident ones.

As a comma category

The free coproduct completion of a category 𝒞\mathcal{C} is equivalently the following comma category.

As a Grothendieck construction

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

PSh ⊔(𝒞)≃∫S∈Set∏s∈S𝒞 PSh_{\sqcup}(\mathcal{C}) \;\; \simeq \;\; \underset { S \,\in\, Set } { \textstyle{\int} } \; \underset{s \in S}{\textstyle{\prod}} \mathcal{C}

on the contravariant pseudofunctor on Set which sends a set SS to the SS-indexed product category of 𝒞\mathcal{C} with itself (equivalently: to the functor category into 𝒞\mathcal{C} out of the discrete category on SS):

Set op ⟶ Cat S ↦ Func(S,𝒞) ≃∏s∈S𝒞 ↓ f ↑ f * T ↦ Func(T,𝒞) ≃∏t∈T𝒞, \array{ Set^{op} &\longrightarrow& Cat \\ S &\mapsto& Func(S,\mathcal{C}) & \simeq \;\underset{s \in S}{\prod} \mathcal{C} \\ \Big\downarrow\mathrlap{{}^{f}} && \Big\uparrow\mathrlap{{}^{f^\ast}} \\ T &\mapsto& Func(T,\mathcal{C}) & \simeq \;\underset{t \in T}{\prod} \mathcal{C} \mathrlap{\,,} }

where the base change-functors f *f^\ast are given (on functor categories by precomposition with ff, hence) by:

(1)f:S⟶T⊢∏t∈T𝒞 →f ∏s∈S𝒞 (X t) t∈T ↦ (X f(s)) s∈S. f \,\colon\, S \longrightarrow T \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\; \vdash \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\; \array{ \underset{t \in T}{\prod} \mathcal{C} &\xrightarrow{\;\; f \;\;}& \underset{s \in S}{\prod} \mathcal{C} \\ \big( X_t \big)_{t \in T} &\mapsto& \big( X_{f(s)} \big)_{s \in S} \,. }

Namely, by definition of the Grothendieck construction

  1. its objects are dependent pairs of the form

    X S≡(S∈Set,(X s∈𝒞) s∈S) X_S \;\equiv\; \big( S \in Set ,\, (X_s \in \mathcal{C})_{s \in S} \big)

  2. its morphisms

    ϕ f:X S⟶Y T \phi_f \;\colon\; X_S \longrightarrow Y_T

    are dependent pairs consisting of a map

    f:S⟶T f \,\colon\, S \longrightarrow T

    and a morphism in ∏s∈S𝒞\underset{s \in S}{\prod} \mathcal{C} of the form

    ϕ:X S⟶f *Y T. \phi \,\colon\, X_S \longrightarrow f^\ast Y_T \,.

    where, by definition (1) of f *f^\ast and the nature of product categories, the latter is an SS-indexed set (ϕ s) s∈S(\phi_s)_{s \in S} of morphisms in 𝒞\mathcal{C} of the form

    ϕ s:X s⟶Y f(s). \phi_s \,\colon\, X_s \longrightarrow Y_{f(s)} \,.

But this is manifestly the same as the explicit description of PSh ⊔(𝒞)PSh_{\sqcup}(\mathcal{C}) above.

Via coproducts of presheaves

The free coproduct completion of 𝒞\mathcal{C} is equivalently the full subcategory

PSh ⊔(𝒞)↪PSh(𝒞) PSh_{\sqcup}(\mathcal{C}) \xhookrightarrow{\;} PSh(\mathcal{C})

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

y:𝒞↪PSh ⊔(𝒞)↪PSh(𝒞) y \;\colon\; \mathcal{C} \xhookrightarrow{\;} PSh_{\sqcup}(\mathcal{C}) \xhookrightarrow{\;} PSh(\mathcal{C})

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.

Properties

Fairly immediate from the explicit definition above is:

(Carboni & Vitale 1998, Lem. 42)
Proof

Since, by assumption, the objects of ℬ\mathcal{B} are already presented by indexed sets (X s) s∈S\big(X_s\big)_{s \in S} of objects in 𝒞\mathcal{C}, it is sufficient to see that under this presentation the morphisms

ϕ:(∐s∈SX s)⟶(∐t∈TY t) \phi \,\colon\, \big(\underset{s \in S}{\coprod} X_s\big) \longrightarrow \big(\underset{t \in T}{\coprod} Y_t\big)

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

  1. the general fact that hom-functors take coproducts in the first argument to products

  2. 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

Hom 𝒞(∐ sX s,∐ tY t) ≃∏ sHom 𝒞(X s,∐ tY t) ≃∏s∈S∐t s∈THom 𝒞(X s,Y t s) ≃∐f:S→T∏s∈SHom 𝒞(X s,Y f(s)). \begin{array}{ll} Hom_{\mathcal{C}}\big( \coprod_s X_s ,\, \coprod_t Y_t \big) \\ \;\simeq\; \prod_s Hom_{\mathcal{C}}\big( X_s ,\, \coprod_t Y_t \big) \\ \;\simeq\; \underset{s \in S}{\prod} \underset{t_s \in T}{\coprod} Hom_{\mathcal{C}}\big( X_s ,\, Y_{t_s} \big) \\ \;\simeq\; \underset{f \colon S \to T}{\coprod} \underset{s \in S}{\prod} Hom_{\mathcal{C}}\big( X_s ,\, Y_{f(s)} \big) \,. \end{array}

(Makkai & Paré (1989), Cor. 5.3.6) (e.g. Carboni, Lack & Walters 1993)
Proof

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 ⊔(𝒞)≃∫ S∈Set𝒞 SPSh_{\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):

X S,Y T∈∫ S∈Set𝒞⊢X S×Y T≃(((pr S) *X)× S×T((pr T) *Y)) S×T. X_S,\, Y_T \,\in\, \textstyle{\int}_{S \in Set} \mathcal{C} \;\;\;\;\;\;\;\;\; \vdash \;\;\;\;\;\;\;\;\; X_S \times Y_T \;\simeq\; \Big( \big( (pr_S)^\ast X \big) \times_{S \times T} \big( (pr_T)^\ast Y \big) \Big)_{S \times T} \,.

Of course this comes down to the expected component formula

(X S×Y T) s,t ≃(((pr S) *X)× S×T((pr T) *Y)) s,t by the above ≃{(s,t)} *(((pr S) *X)× S×T((pr T) *Y)) by definition ≃(({(s,t)} *(pr S) *X)× {(s,t)}({(s,t)} *(pr T) *Y)) pullback is right adjoint ≃({s} *X)× {(s,t)}({t} *Y) by commuting diagram below ≃X s×Y t by definition \begin{array}{ll} \big( X_S \times Y_T \big)_{s,t} \\ \;\simeq\; \Big( \big( (pr_S)^\ast X \big) \times_{S \times T} \big( (pr_T)^\ast Y \big) \Big)_{s,t} & \text{by the above} \\ \;\simeq\; \{(s,t)\}^\ast \Big( \big( (pr_S)^\ast X \big) \times_{S \times T} \big( (pr_T)^\ast Y \big) \Big) & \text{by definition} \\ \;\simeq\; \Big( \big( \{(s,t)\}^\ast (pr_S)^\ast X \big) \times_{\{(s,t)\}} \big( \{(s,t)\}^\ast (pr_T)^\ast Y \big) \Big) & \text{pullback is right adjoint} \\ \;\simeq\; \big( \{s\}^\ast X \big) \times_{\{(s,t)\}} \big( \{t\}^\ast Y \big) & \text{by commuting diagram below} \\ \;\simeq\; X_s \times Y_t & \text{by definition} \end{array}

{s} ≃ {(s,t)} ≃ {t} ↓ ↓ ↓ S ⟵pr S S×T ⟶pr T T \array{ \{s\} &\simeq& \{(s,t)\} &\simeq& \{t\} \\ \Big\downarrow && \Big\downarrow && \Big\downarrow \\ S &\underset{pr_S}{\longleftarrow}& S \times T &\underset{pr_T}{\longrightarrow}& T }

Similarly, the component formula for the free coproduct is

(Y T⨿Y′ T′) τ≃{Y τ | τ∈T Y′ τ | τ∈T′. \big( Y_T \amalg Y'_{T'} \big)_{\tau} \;\simeq\; \left\{ \begin{array}{lll} Y_\tau &\vert& \tau \in T \\ Y'_{\tau} &\vert& \tau \in T' \end{array} \right. \,.

Using all this, distributivity is verified as follows:

(X S×(Y T⊔Y T′)) s,τ ≃X s×(Y T⊔Y T′) τ ≃{X s×Y τ | τ∈T X s×Y′ τ | τ∈T′ ≃{(X S×Y T) s,τ | τ∈T (X S×Y′ T′) s,τ | τ∈T′ ≃((X S×Y T)⊔(X S×Y′ T′)) s,τ. \begin{array}{ll} \Big( X_S \times \big( Y_T \sqcup Y_{T'} \big) \Big)_{s, \tau} \\ \;\simeq\; X_s \times \big( Y_T \sqcup Y_{T'} \big)_\tau \\ \;\simeq\; \left\{ \begin{array}{lll} X_s \times Y_\tau &\vert& \tau \in T \\ X_s \times Y'_{\tau} &\vert& \tau \in T' \end{array} \right. \\ \;\simeq\; \left\{ \begin{array}{lll} (X_S \times Y_T)_{s, \tau} &\vert& \tau \in T \\ (X_S \times Y'_{T'})_{s, \tau} &\vert& \tau \in T' \end{array} \right. \\ \;\simeq\; \Big( \big( X_S \times Y_T \big) \sqcup \big( X_S \times Y'_{T'} \big) \Big)_{s,\tau} \,. \end{array}

Examples

Coproduct completion of connected objects

The following examples follow as special cases of Prop. :

Coproduct compeletion of extensive categories

References

Early discussion of the concept:

  • Jean Bénabou, §3.3 in: Fibered Categories and the Foundations of Naive Category Theory, The Journal of Symbolic Logic, Vol. 50 1 (1985) 10-37 [doi:10.2307/2273784]

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

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.