nLab dependent sum

Contents

Context

Category theory

Limits and colimits

Contents

Idea

The dependent sum is a universal construction in category theory. It generalizes the Cartesian product to the situation where one factor may depend on the other. It is the left adjoint to the base change functor between slice categories.

The dual notion is that of dependent product.

Definition

Let π’ž\mathcal{C} be a category and f:Aβ†’If \colon A \to I a morphism in π’ž\mathcal{C} such that pullbacks along ff exist in π’ž\mathcal{C}. These then constitute a base change functor

f *:π’ž /Iβ†’π’ž /A f^* \colon \mathcal{C}_{/I} \to \mathcal{C}_{/A}

between the corresponding slice categories.

Definition

The dependent sum or dependent coproduct along the morphism ff is the left adjoint βˆ‘ f:π’ž /Aβ†’π’ž /I\sum_f \colon \mathcal{C}_{/A} \to \mathcal{C}_{/I} of the base change functor

(βˆ‘ f⊣f *):π’ž /A←f *β†’βˆ‘ fπ’ž /I. (\sum_f \dashv f^* ) \colon \mathcal{C}_{/A} \stackrel{\overset{\sum_f}{\to}}{\underset{f^*}{\leftarrow}} \mathcal{C}_{/I} \qquad.

This is directly seen to be equivalent to the following.

Definition

The dependent sum along f:A→If \colon A \to I is the functor

βˆ‘ f≔f∘(βˆ’):π’ž /Aβ†’π’ž /I \sum_f \coloneqq f\circ (-) \colon \mathcal{C}_{/A} \to \mathcal{C}_{/I}

given by composition with ff.

Properties

Relation to the product

Assume that the category π’ž\mathcal{C} has a terminal object *βˆˆπ’ž* \in \mathcal{C}. Let Xβˆˆπ’žX \in \mathcal{C} be any object and assume that the terminal morphism f:Xβ†’*f \colon X \to * admits all pullbacks along it.

Notice that a pullback of some Aβ†’*A \to * along Xβ†’*X \to * is simply the product XΓ—AX \times A, equipped with its projection morphism XΓ—Aβ†’XX \times A \to X. We may regard XΓ—Aβ†’XX \times A \to X as the image of the base change functor f *:π’ž /*β†’π’ž /Xf^* \colon \mathcal{C}_{/*} \to \mathcal{C}_{/X}, but this is not quite just the product in π’ž\mathcal{C}, which instead corresponds to the terminal morphisms XΓ—Aβ†’*X \times A \to *. But we have:

Proposition

The product XΓ—Aβˆˆπ’žX \times A \in \mathcal{C} is, if it exists, equivalently the dependent sum of the base change of Aβ†’*A \to * along Xβ†’*X \to *:

βˆ‘ XX *A≃XΓ—Aβˆˆπ’ž. \sum_{X} X^* A \simeq X \times A \in \mathcal{C} \quad .

Here we write β€œXX” also for the morphism Xβ†’*X \to *.

Relation to type theory

Under the relation between category theory and type theory the dependent sum is the categorical semantics of dependent sum types .

Notice that under the identification of propositions as types, dependent sum types (or rather their bracket types) correspond to existential quantification βˆƒx:X,Px\exists x\colon X, P x.

The following table shows how the natural deduction rules for dependent sum types correspond to their categorical semantics given by the dependent sum universal construction.

The inference rules for dependent pair types (aka β€œdependent sum types” or β€œΞ£\Sigma-types”):

Relation to some limits

Proposition

For π’ž\mathcal{C} a category with finite limits and Xβˆˆπ’žX \in \mathcal{C} an object, then dependent sum

βˆ‘X:π’ž /XβŸΆπ’ž \underset{X}{\sum}: \mathcal{C}_{/X} \longrightarrow \mathcal{C}

preserves and reflects fiber products.

Proof

By this proposition limits over a cospan diagram in the slice category are computed as limits over the cocone diagram under the cospan in the base category. By this proposition this inclusion is a final functor, hence preserves limits. Since the dependent sum of the diagram is the restriction along this final functor, the result follows.

Proposition

For π’ž\mathcal{C} a category with finite limits and Xβˆˆπ’žX\in \mathcal{C} any object, the naturality square of the unit of the (βˆ‘X⊣X *)(\underset{X}{\sum} \dashv X^\ast)-adjunction on any morphism (f:Aβ†’B)(f \colon A \to B) in π’ž /X\mathcal{C}_{/X}

A ⟢ X *βˆ‘XA ↓ f ↓ X *βˆ‘Xf B ⟢ X *βˆ‘XB \array{ A &\longrightarrow& X^\ast \underset{X}{\sum} A \\ \downarrow^{\mathrlap{f}} && \downarrow^{\mathrlap{X^\ast \underset{X}{\sum} f}} \\ B &\longrightarrow& X^\ast \underset{X}{\sum} B }

is a pullback.

Proof

By prop. it suffices to see that the diagram is a pullback in π’ž\mathcal{C} under βˆ‘X\underset{X}{\sum}, where, by Frobenius reciprocity, it becomes

βˆ‘XA ⟢(A,id) XΓ—βˆ‘XA ↓ βˆ‘Xf ↓ (id,βˆ‘Xf) βˆ‘XB ⟢(B,id) XΓ—βˆ‘XB. \array{ \underset{X}{\sum} A &\stackrel{(A,id)}{\longrightarrow}& X \times \underset{X}{\sum} A \\ \downarrow^{\mathrlap{\underset{X}{\sum}f}} && \downarrow^{\mathrlap{(id, \underset{X}{\sum} f)}} \\ \underset{X}{\sum} B &\stackrel{(B,id)}{\longrightarrow}& X \times \underset{X}{\sum} B } \qquad .
Proposition

For π’ž\mathcal{C} a category with finite limits and Xβˆˆπ’žX\in \mathcal{C} any object, the naturality square of the counit of the (βˆ‘X⊣X *)(\underset{X}{\sum} \dashv X^\ast)-adjunction on any morphism (f:Aβ†’B)(f \colon A \to B) in π’ž\mathcal{C}

βˆ‘XX *A ⟢ A ↓ βˆ‘XX *f ↓ f βˆ‘XX *B ⟢ B \array{ \underset{X}{\sum} X^\ast A &\longrightarrow& A \\ \downarrow^{\mathrlap{\underset{X}{\sum}X^\ast f}} && \downarrow^{\mathrlap{f}} \\ \underset{X}{\sum} X^\ast B &\longrightarrow& B }

is a pullback.

Proof

By Frobenius reciprocity the diagram is equivalent to

XΓ—A ⟢ A ↓ (id,f) ↓ f XΓ—B ⟢ B. \array{ X\times A & \longrightarrow& A \\ \downarrow^{\mathrlap{(id,f)}} && \downarrow^{\mathrlap{f}} \\ X \times B &\longrightarrow& B } \qquad.

In higher category theory

Let CC be an (∞,1)-category. We still want to define the dependent sum as the functor C /Xβ†’C /YC_{/X} \to C_{/Y} given by composing with the functor Xβ†’YX \to Y, but the details are more complex.

The codomain fibration tgt:C [1]β†’Ctgt : C^{[1]} \to C is a cocartesian fibration classified by a functor L:Cβ†’(∞,1)Cat:X↦C /XL : C \to (\infty,1)Cat : X \mapsto C_{/X}.

Then for any f:X→Yf : X \to Y, we can define Σ f=L(f)\Sigma_f = L(f) to be the dependent sum.

Since the morphisms [z→x]→[z→y][z \to x] \to [z \to y] induced by composition are cocartesian morphisms, we see that Σ f\Sigma_f is indeed given by composition with ff.

By proposition 6.1.1.1 and the following remarks of Lurie, if CC has pullbacks, then this is also a cartesian fibration, and is classified by a map R:C opβ†’(∞,1)CatR : C^{op} \to (\infty,1)Cat. Then f *=R(f):C /Yβ†’C /Xf^* = R(f) : C_{/Y} \to C_{/X} is the functor computing pullbacks along ff, and we have the adjunction Ξ£ f⊣f *\Sigma_f \dashv f^*.

References

Standard textbook accounts include section A1.5.3 of

and section IV of

Other references:

Last revised on May 19, 2021 at 03:52:57. See the history of this page for a list of all contributions to it.