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 $ev: S \times A \to B$ such that
equals the usual product projection from $S \times A$ to $A$; So $ev$ is a morphism in the over category $Set/A$. The universal property of $S$ is that, given any set $T$ and morphism $T \times A \to B$ in $Set/A$, there's a unique map $T \to S$ that makes everything commute.
In other words, $S$ and $ev$ define an adjunction from $Set$ to $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 $Set$ to an arbitrary over category $\mathcal{C}/I$.
Let $\mathcal{C}$ be a category, and $g\colon B \to A$ a morphism in $\mathcal{C}$, such that pullbacks along this morphism exist. These then constitute the base change functor between the corresponding slice categories
The dependent product along $g$ is, if it exists, the right adjoint functor $\prod_g \colon : \mathcal{C}_{/B} \to \mathcal{C}_{/A}$ to the base change along $g$
So a category with all dependent products is necessarily a category with all pullbacks.
Let $\mathcal{C}$ be a cartesian closed category with all limits and note that $\mathcal{C}_{/\ast}\cong\mathcal{C}$. Let $X \in C$ be any object and identify it with the terminal morphism $X\to *$. Then the dependent product functor
sends bundles $P \to X$ to their object of sections.
We check the characterizing natural isomorphism for the adjunction: For every $A \in \mathcal{C}$ we have the following sequence of natural isos:
This statement and its proof remain valid in homotopy theory. More in detail, if $\mathcal{C}$ 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.
As a special case of prop. 1 one obtains exponential objects/internal homs.
Let $\mathcal{C}$ have a terminal object $* \in \mathcal{C}$. Let $A$ and $X$ in $\mathcal{C}$ be objects and let $A \colon A \to *$ and $X \colon X \to *$ be the terminal morphisms.
The dependent product along $X$ of the arrow obtained by base change of $A$ along $X$ is the exponential object $[X,A]$:
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 $\overset{n}{\overbrace{m+\dots +m}}$ of $n$ copies of $m$.
Consider the chain of equivalences from $[X,A]$ to $\prod_{X} X^* A$ in Set: Firstly, the exponential object $[X,A]$ is characterized in $[Y,[X,A]]$ as right adjoint to $[Y\times X,A]$. Secondly, the elements $\theta$ of $[Y\times X,A]$ are in turn in bijection with those functions $(y,x)\mapsto (\theta(y,x),x)$ from $[Y\times X,A\times X]$, that leave the second component fixed. The condition just stated is the definition of arrows in the overcategory ${Set}/X$, between the right projections out of $Y\times X$ resp. $A\times X$. If we identify objects $Z\in{Set}$ with their terminal morphisms $Z:Z\to *$ in ${Set}/*$, those two right projections are the pullbacks $X^* Y$ and $X^* A$, respectively. Thirdly, thus, the subset of $[Y\times X,A\times X]$ we are interested in corresponds to $[X^* Y,X^* A]$ in ${Set}/X$. Finally, the right adjoint to $X^*$ is a functor $\prod_{X}$ from ${Set}/X$ to ${Set}/*$, such that $[X^* Y,X^* A]\simeq [Y, \prod_{X} X^* A]$. Hence $\prod_{X} X^* A$ must correspond to $[X,A]$.
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 | $\displaystyle\frac{\vdash\: X \colon Type \;\;\;\;\; x \colon X \;\vdash\; A(x)\colon Type}{\vdash \; \left(\prod_{x \colon X} A\left(x\right)\right) \colon Type}$ | $\left( \array{ A^{\phantom{p_1}} \\ \downarrow^{p_1} \\ X_{\phantom{p_1}}} \in \mathcal{C}\right) \Rightarrow \left( \prod_{x\colon X} A\left(x\right) \in \mathcal{C}\right)$ |
term introduction | $\displaystyle\frac{x \colon X \;\vdash\; a\left(x\right) \colon A\left(x\right)}{\vdash (x \mapsto a\left(x\right)) \colon \prod_{x' \colon X} A\left(x'\right) }$ | |
term elimination | $\displaystyle\frac{\vdash\; f \colon \left(\prod_{x \colon X} A\left(x\right)\right)\;\;\;\; \vdash \; x \colon X}{x \colon X\;\vdash\; f(x) \colon A(x)}$ | |
computation rule | $(y \mapsto a(y))(x) = a(x)$ |
Dependent products (and sums) exist in any topos:
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.
For $\mathbf{H}$ an (∞,1)-topos and $G$ an group object in $\mathbf{H}$ (an ∞-group), then the slice (∞,1)-topos over its delooping may be identified with the (∞,1)-category of $G$-∞-actions (see there for more):
Under this identification, then dependent product along a morphism of the form $\mathbf{B}H \to \mathbf{B}G$ (corresponding to an ∞-group homomorphism $H \to G$) corresponds to forming coinduced representations.
As the special case of the above for $H = 1$ the trivial group we obtain the following:
Let $\mathbf{H}$ be any (∞,1)-topos and let $G$ be a group object in $\mathbf{H}$ (an ∞-group). Then the dependent product along the canonical point inclusion
into the delooping of $G$ takes the following form:
There is a pair of adjoint ∞-functors of the form
where
$hofib$ denotes the operation of taking the homotopy fiber of a map to $\mathbf{B}G$ over the canonical basepoint;
$[G,-]$ denotes the internal hom in $\mathbf{H}$;
$[G,-]/G$ denotes the homotopy quotient by the conjugation ∞-action for $G$ equipped with its canonical ∞-action by left multiplication and the argument regarded as equipped with its trivial $G$-$\infty$-action
(for $G = S^1$ then this is the cyclic loop space construction).
Hence for
$\hat X \to X$ a $G$-principal ∞-bundle
$A$ a coefficient object, such as for some differential generalized cohomology theory
then there is a natural equivalence
given by
The statement that $i^\ast \simeq hofib$ follows immediately by the definitions. What we need to show is that the dependent product along $i$ is given as claimed.
To that end, first observe that the conjugation action on $[G,X]$ is the internal hom in the (∞,1)-category of $G$-∞-actions $Act_G(\mathbf{H})$. Under the equivalence of (∞,1)-categories
(from NSS 12) then $G$ with its canonical ∞-action is $(\ast \to \mathbf{B}G)$ and $X$ with the trivial action is $(X \times \mathbf{B}G \to \mathbf{B}G)$.
Hence
So far this is the very definition of what $[G,X]/G \in \mathbf{H}_{/\mathbf{B}G}$ is to mean in the first place.
But now since the slice (∞,1)-topos $\mathbf{H}_{/\mathbf{B}G}$ is itself cartesian closed, via
it is immediate that there is the following sequence of natural equivalences
Here $p \colon \mathbf{B}G \to \ast$ denotes the terminal morphism and $p_! \dashv p^\ast$ denotes the base change along it.
See also at double dimensional reduction for more on this.
More generally:
Let $\mathbf{H}$ be an (∞,1)-topos and $G \in Grp(\mathbf{H})$ an ∞-group.
Let moreover $V \in \mathbf{H}$ be an object equipped with a $G$-∞-action $\rho$, equivalently (by the discussion there) a homotopy fiber sequence of the form
Then
pullback along $p_\rho$ is the operation that assigns to a morphism $c \colon X \to \mathbf{B}G$ the $V$-fiber ∞-bundle which is associated via $\rho$ to the $G$-principal ∞-bundle $P_c$ classified by $c$:
the right base change along $p_\rho$ is given on objects of the form $X \times (V/G)$ by
The first statement is NSS 12, prop. 4.6.
The second statement follows as in the proof of prop. \ref{CyclicLoopSpace}: Let
be any object, then there is the following sequence of natural equivalences
where again
(symmetric powers)
Let
be the symmetric group on $n$ elements, and
the $n$-element set (h-set) equipped with the canonical $\Sigma(n)$-action. Then prop. 3 says that right base change of any $p_\rho^\ast p^\ast X$ along
is equivalently the $n$th symmetric power of $X$
dependent sum, dependent product
Standard textbook accounts include section A1.5.3 of
and section IV of