nLab
dependent product

Idea

The concept of cartesian product makes sense for any family of sets, while the category-theoretic product makes sense for any family of objects. In each case, however, the family is indexed by a set; how can we get a purely category-theoretic product indexed by an object?

First we need to describe a family of objects indexed by an object; it's common to interpret this as a bundle, that is an arbitrary morphism $g:B\to A$. (In Set, $A$ would be the index set of the family, and the fiber of the bundle over an element $x$ of $A$ would be the set indexed by $x$. Conversely, given a family of sets, $B$ can be constructed as its disjoint union.)

In these terms, the cartesian product of the family of sets is the set $S$ of (global) sections of the bundle. This set comes equipped with an evaluation map $\mathrm{ev}:S\times A\to B$ such that

$$S\times A\stackrel{\mathrm{ev}}{\to }B\stackrel{g}{\to }A$$S \times A \stackrel{ev}\to B \stackrel{g}\to A

equals the usual product projection; in other words, $\mathrm{ev}$ is a morphism in the over category $\mathrm{Set}/A$. The universal property of $S$ is that, given any set $T$ and morphism $T\times A\to B$ in $\mathrm{Set}/A$, there's a unique map $T\to S$ that makes everything commute.

In other words, $S$ and $\mathrm{ev}$ define an adjunction from $\mathrm{Set}$ to $\mathrm{Set}/A$ in which taking the product with $A$ is the left adjoint and applying this universal property is the right adjoint. This is the basis for the definition below, but we add one further level of generality: we move everything from $\mathrm{Set}$ to an arbitrary over category $\mathrm{Set}/I$.

We also consider dependent sums, which are actually simpler.

Definitions

For $C$ a category, the dependent product of the morphism $g:B\to A$ indexed by the morphism $f:A\to I$ is an object ${\prod }_{f}g$ in the over category $C/I$, where the operation ${\prod }_f:C/A\to C/I$ is the right adjoint to the base change functor $f^{*}:C/I\to C/A$. For this to make sense, $f^{*}$ must exist; that is, all pullbacks along $f$ must exist. So a category with all dependent products is necessarily a category with all pullbacks.

In type theory, the operation of dependent product is typically taken as a primitive; see dependent product type. When employing the Curry–Howard correspondence, one sometimes (such as in Coq) writes ${\Pi }_{x\in X}{P}_x$ as written $\forall x:X,Px$, because dependent products correspond to universal quantification.

The left adjoint to the base-change functor, the dependent coproduct or dependent sum ${\sum }_f:C/A\to C/I$, is much simpler. It is simply given by composition with $f$, so it always exists when it makes sense (that is when $f$ has all pullbacks). In the Curry–Howard correspondence, this corresponds to the particular quantification $\exists x:X,Px$. See dependent sum type.

Note that the binary cartesian product is a special case of the direct sum: when $g:B\to A$ is a constant family, i.e. a projection $C\times A\to A$ from a binary product, then its dependent sum is just the ordinary cartesian product $C\times A$. In this context, the dependent product can be identified with the exponential object $C^A$. In other words, dependent sums generalize ordinary products, while dependent products generalize ordinary exponentials. (For this reason, one occasionally finds the dependent sum called the “dependent product”.) This is essentially a categorified version of the familiar fact that the product $n\cdot m$ of two natural numbers can be identified with the sum $\stackrel{n}{\overbrace{m+\dots +m}}$ of $n$ copies of $m$.

Properties

Relation to spaces of sections

Proposition

Let $𝒞$ be a cartesian closed category with all limits. Let $X\in C$ be any object.

Then the dependent product functor

$$𝒞/X\stackrel{\stackrel{-\times X}{\leftarrow }}{\underset{\prod _{x\in X}}{\to }}𝒞$$\mathcal{C}/X \stackrel{\overset{- \times X}{\leftarrow}}{\underset{\prod_{x \in X}}{\to}} \mathcal{C}

sends bundles $P\to X$ to their object of sections

$$\prod _{x\in X}{P}_x\simeq {\Gamma }_X(P):=[X,P]{\times }_{[X,X]}\{\mathrm{id}\}.$$\prod_{x \in X} P_x \simeq \Gamma_X(P) := [X,P] \times_{[X,X]} \{id\} \,.

Proof

One computes for every $A\in 𝒞$

$$\begin{array}{rl}𝒞(A\times X,P\to X)& =𝒞(A\times X,P){\times }_{𝒞(A\times X,X)}\{p_2\}\\ & =𝒞(A,[X,P]){\times }_{𝒞(A,[X,X])}\{{\tilde{p}}_2\}\\ & =𝒞(A,[X,P]{\times }_{[X,X]}\{\mathrm{Id}\})\\ & =𝒞(A,{\Gamma }_X(P))\end{array}.$$\begin{aligned} \mathcal{C}(A \times X, P \to X) &= \mathcal{C}(A \times X, P ) \times_{\mathcal{C}(A \times X, X)} \{p_2\} \\ & = \mathcal{C}(A, [X,P]) \times_{\mathcal{C}(A,[X,X])} \{\tilde p_2\} \\ &= \mathcal{C}(A, [X,P] \times_{[X,X]} \{Id\}) \\ &= \mathcal{C}(A, \Gamma_X(P)) \end{aligned} \,.

Remark

This statement and its proof remain valid in homotopy theory. More in detail, if $𝒞$ is a simplicial model category, $X$, $A$ and $X\times A$ are cofibrant, $P$ and $X$ are fibrant and $P\to X$ is a fibration, then ${\Gamma }_X(A)$ as above is the homotopy-correct derived section space.

Relation to quantification in logic

In terms of the internal logic of categories, when one considers propositions as types, one has that

• dependent sum corresponds to existential quantification;

• dependent product corresponds to universal quantification.

See there for more details.

Examples

Dependent products (and sums) exist in any topos:

Proposition

For $C$ a topos and $f:A\to I$ any morphism in $C$, both the left adjoint ${\sum }_f:C/A\to C/I$ as well as the right adjoint ${\prod }_f:C/A\to C/I$ to $f^{*}:C/I\to C/A$ exist.

Moreover, $f^{*}$ preserves the subobject classifier and internal homs.

This is (MacLaneMoerdijk, theorem 2 in section IV, 7).

The dependent product plays a role in the definition of universe in a topos.

Related concepts

base change

• dependent sum, dependent product

• dependent sum type, dependent product type

References

Standard textbook accounts include section A1.5.3 of

• Peter Johnstone, Sketches of an Elephant

and section IV of

• Saunders MacLane, Ieke Moerdijk, Sheaves in Geometry and Logic