nLab
dependent product

Idea

The dependent product is a universal construction in category theory. It generalizes the internal hom, and hence indexed products, to the situation where the codomain may depend on the domain, hence it forms sections of a bundle.

The dual concept is that of dependent sum.

The concept of cartesian product of sets 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$.

Definitions

Let $𝒞$ be a category, and $g:B\to A$ a morphism in $𝒞$, such that pullbacks along this morphism exist. These then constitute the base change functor between the corresponding slice categories

$$g^{*}:{𝒞}_{/A}\to {𝒞}_{/B}.$$g^* \colon \mathcal{C}_{/A} \to \mathcal{C}_{/B} \,.

Definition

The dependent product along $g$ is, if it exists, the right adjoint functor ${\prod }_g::{𝒞}_{/B}\to {𝒞}_{/A}$ to the base change along $g$

$$(g^{*}⊢\prod _g):{𝒞}_{/B}\stackrel{\stackrel{g^{*}}{\leftarrow }}{\underset{\prod _g}{\to }}{𝒞}_{/A}.$$(g^* \vdash \prod_g) \colon \mathcal{C}_{/B} \stackrel{\overset{g^* }{\leftarrow}}{\underset{\prod_g}{\to}} \mathcal{C}_{/A} \,.

So a category with all dependent products is necessarily a category with all pullbacks.

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 exponential objects / internal homs

As a special case of the above one obtaines exponential objects/internal homs.

Let $𝒞$ have a terminal object $*\in 𝒞$. Let $X\in 𝒞$ be any object and let $X:X\to *$ be the terminal morphism.

Proposition

The dependent product along $X$ of the base change along $X$ is the exponential object/internal hom $[X,A]$

$$\prod _X{X}^{*}A\simeq [X,A]\in 𝒞.$$\prod_{X} X^* A \simeq [X,A] \in \mathcal{C} \,.

Remark

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

Relation to type theory and quantification in logic

The dependent product is the categorical semantics of what in type theory is the formation of dependent product types. Under propositions as types this corresponds to universal quantification.

	type theory	category theory
	syntax	semantics
	natural deduction	universal construction
	dependent product type	dependent product
type formation	$\frac{⊢X:\mathrm{Type}x:X⊢A(x):\mathrm{Type}}{⊢\left({\prod }_{x:X}A\left(x\right)\right):\mathrm{Type}}$
term introduction	$\frac{x:X⊢a\left(x\right):A\left(x\right)}{⊢(x\mapsto a\left(x\right)):{\prod }_{x\prime :X}A(x\prime )}$
term elimination	$\frac{⊢f:\left({\prod }_{x:X}A\left(x\right)\right)⊢x:X}{x:X⊢f(x):A(x)}$
computation rule	$(y\mapsto a(y))(x)=a(x)$

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

• product, coproduct

• Kan extension

• 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