nLab dependent product

Dependent products


Category theory

Limits and colimits

Dependent products


The dependent product is a universal construction in category theory. It generalizes the internal hom to the situation where the codomain may depend on the domain, and internalizes indexed products. 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 π:EA\pi: E \to A. (In Set, AA would be the index set of the family, and the fiber of the bundle over an element xx of AA would be the set indexed by xx. Conversely, given a family of sets, EE can be constructed as its disjoint union.)

In these terms, the cartesian product of the family of sets is the set SS of (global) sections of the bundle. This set comes equipped with an evaluation map ev:S×AEev: S \times A \to E such that

S×AevEπA S \times A \stackrel{ev}\to E \stackrel{\pi}\to A

equals the usual product projection from S×AS \times A to AA, so evev and π\pi are both morphisms in the over category Set/ASet/A. The universal property of SS is that, given any set TT and morphism T×AET \times A \to E in Set/ASet/A, there's a unique map TST \to S that makes everything commute.

In other words, SS and evev define an adjunction from SetSet to Set/ASet/A in which taking the product with AA 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 realise that SetSet is secretly Set/*Set/*, where ** is the one-point set (the final object), and move everything from SetSet to an arbitrary over category 𝒞/I\mathcal{C}/I.


Let 𝒞\mathcal{C} be a category, and g:BAg\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

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

The dependent product along gg is, if it exists, the right adjoint functor g:𝒞 /B𝒞 /A\prod_g \colon \mathcal{C}_{/B} \to \mathcal{C}_{/A} to the base change along gg

(g * g):𝒞 /B gg *𝒞 /A. (g^* \dashv \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.


Relation to spaces of sections


Let 𝒞\mathcal{C} be a cartesian closed category with all limits and note that 𝒞 /*𝒞\mathcal{C}_{/\ast}\cong\mathcal{C}. Let XCX \in C be any object and identify it with the terminal morphism X*X\to *. Then the dependent product functor

𝒞 /X xX×X𝒞 \mathcal{C}_{/X} \underoverset {\underset{\prod_{x \in X}}{\longrightarrow}} {\overset{- \times X}{\longleftarrow}} {\bot} \mathcal{C}

sends bundles PXP \to X to their object of sections.

xXP xΓ X(P):=[X,P]× [X,X]{id}. \prod_{x \in X} P_x \simeq \Gamma_X(P) := [X,P] \times_{[X,X]} \{id\} \,.

We check the characterizing natural isomorphism for the adjunction: For every A𝒞A \in \mathcal{C} we have the following sequence of natural isos:

𝒞 /X(A×X,PX) =𝒞(A×X,P)× 𝒞(A×X,X){p 2} =𝒞(A,[X,P])× 𝒞(A,[X,X]){p˜ 2} =𝒞(A,[X,P]× [X,X]{Id}) =𝒞(A,Γ X(P)). \begin{aligned} \mathcal{C}_{/X}(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} \,.

This statement and its proof remain valid in homotopy theory. More in detail, if 𝒞\mathcal{C} is a simplicial model category, XX, AA and X×AX \times A are cofibrant, PP and XX are fibrant and PXP \to X is a fibration, then Γ X(A)\Gamma_X(A) as above is the homotopy-correct derived section space.

Relation to exponential objects / internal homs

As a special case of prop. one obtains exponential objects/internal homs.

Let 𝒞\mathcal{C} have a terminal object *𝒞* \in \mathcal{C}. Let AA and XX in 𝒞\mathcal{C} be objects and let A:A*A \colon A \to * and X:X*X \colon X \to * be the terminal morphisms.


The dependent product along XX of the arrow obtained by base change of AA along XX is the exponential object [X,A][X,A]:

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

This is essentially a categorified version of the familiar fact that the exponentiation m nm^n of two natural numbers can be identified with the product mmn\overset{n}{\overbrace{m\cdot\dots \cdot m}} of nn copies of mm.


Consider the chain of equivalences from [X,A][X,A] to XX *A\prod_{X} X^* A in Set: Firstly, the exponential object [X,A][X,A] is characterized in [Y,[X,A]][Y,[X,A]] as right adjoint to [Y×X,A][Y\times X,A]. Secondly, the elements θ\theta of [Y×X,A][Y\times X,A] are in turn in bijection with those functions (y,x)(θ(y,x),x)(y,x)\mapsto (\theta(y,x),x) from [Y×X,A×X][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{Set}/X, between the right projections out of Y×XY\times X resp. A×XA\times X. If we identify objects ZSetZ\in{Set} with their terminal morphisms Z:Z*Z:Z\to * in Set/*{Set}/*, those two right projections are the pullbacks X *YX^* Y and X *AX^* A, respectively. Thirdly, thus, the subset of [Y×X,A×X][Y\times X,A\times X] we are interested in corresponds to [X *Y,X *A][X^* Y,X^* A] in Set/X{Set}/X. Finally, the right adjoint to X *X^* is a functor X\prod_{X} from Set/X{Set}/X to Set/*{Set}/*, such that [X *Y,X *A][Y, XX *A][X^* Y,X^* A]\simeq [Y, \prod_{X} X^* A]. Hence XX *A\prod_{X} X^* A must correspond to [X,A][X,A].

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.

The inference rules for dependent function types (aka “dependent product types” or “Π\Pi-types”):


In toposes

Dependent products (and sums) exist in any topos:


For CC a topos and f:AIf : A \to I any morphism in CC, both the left adjoint f:C/AC/I\sum_f : C/A \to C/I as well as the right adjoint f:C/AC/I\prod_f: C/A \to C/I to f *:C/IC/Af^*: C/I \to C/A exist.

Moreover, f *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.

Along BHBG\mathbf{B}H \to \mathbf{B}G

For H\mathbf{H} an (∞,1)-topos and GG an group object in H\mathbf{H} (an ∞-group), then the slice (∞,1)-topos over its delooping may be identified with the (∞,1)-category of GG-∞-actions (see there for more):

Act G(H)H /BG. Act_G(\mathbf{H}) \simeq \mathbf{H}_{/\mathbf{B}G} \,.

Under this identification, then dependent product along a morphism of the form BHBG\mathbf{B}H \to \mathbf{B}G (corresponding to an ∞-group homomorphism HGH \to G) corresponds to forming coinduced representations.

Along *BG\ast \to \mathbf{B}G

As the special case of the above for H=1H = 1 the trivial group we obtain the following:


Let H\mathbf{H} be any (∞,1)-topos and let GG be a group object in H\mathbf{H} (an ∞-group). Then the dependent product along the canonical point inclusion

i:*BG i \;\colon\; \ast \to \mathbf{B}G

into the delooping of GG takes the following form:

There is a pair of adjoint ∞-functors of the form

Hi[G,]/Gi *hofibH /BG, \mathbf{H} \underoverset { \underset{\underset{i}{\prod} \simeq [G,-]/G}{\longrightarrow}} { \overset{i^\ast \simeq hofib}{\longleftarrow}} {\bot} \mathbf{H}_{/\mathbf{B}G} \,,


  • hofibhofib denotes the operation of taking the homotopy fiber of a map to BG\mathbf{B}G over the canonical basepoint;

  • [G,][G,-] denotes the internal hom in H\mathbf{H};

  • [G,]/G[G,-]/G denotes the homotopy quotient by the conjugation ∞-action for GG equipped with its canonical ∞-action by left multiplication and the argument regarded as equipped with its trivial GG-\infty-action

    (for G=S 1G = S^1 then this is the cyclic loop space construction).

Hence for

then there is a natural equivalence

H(X^,A)originalfluxesoxidationreductionH(X,[G,A]/G)doublydimensionally reducedfluxes \underset{ \text{original} \atop \text{fluxes} }{ \underbrace{ \mathbf{H}(\hat X\;,\; A) } } \;\; \underoverset {\underset{oxidation}{\longleftarrow}} {\overset{reduction}{\longrightarrow}} {\simeq} \;\; \underset{ \text{doubly} \atop { \text{dimensionally reduced} \atop \text{fluxes} } }{ \underbrace{ \mathbf{H}(X \;,\; [G,A]/G) } }

given by

(X^A)(X [G,A]/G BG) \left( \hat X \longrightarrow A \right) \;\;\; \leftrightarrow \;\;\; \left( \array{ X && \longrightarrow && [G,A]/G \\ & \searrow && \swarrow \\ && \mathbf{B}G } \right)

The statement that i *hofibi^\ast \simeq hofib follows immediately by the definitions. What we need to show is that the dependent product along ii is given as claimed.

To that end, first observe that the conjugation action on [G,X][G,X] is the internal hom in the (∞,1)-category of GG-∞-actions Act G(H)Act_G(\mathbf{H}). Under the equivalence of (∞,1)-categories

Act G(H)H /BG Act_G(\mathbf{H}) \simeq \mathbf{H}_{/\mathbf{B}G}

(from NSS 12) then GG with its canonical ∞-action is (*BG)(\ast \to \mathbf{B}G) and XX with the trivial action is (X×BGBG)(X \times \mathbf{B}G \to \mathbf{B}G).


[G,X]/G[*,X×BG] BGH /BG. [G,X]/G \simeq [\ast, X \times \mathbf{B}G]_{\mathbf{B}G} \;\;\;\;\; \in \mathbf{H}_{/\mathbf{B}G} \,.

So far this is the very definition of what [G,X]/GH /BG[G,X]/G \in \mathbf{H}_{/\mathbf{B}G} is to mean in the first place.

But now since the slice (∞,1)-topos H /BG\mathbf{H}_{/\mathbf{B}G} is itself cartesian closed, via

E× BG()[E,] BG E \times_{\mathbf{B}G}(-) \;\;\; \dashv \;\;\; [E,-]_{\mathbf{B}G}

it is immediate that there is the following sequence of natural equivalences

H /BG(Y,[G,X]/G) H /BG(Y,[*,X×BG] BG) H /BG(Y× BG*,X×BGp *X) H(p !(Y× BG*)hofib(Y),X) H(hofib(Y),X) \begin{aligned} \mathbf{H}_{/\mathbf{B}G}(Y, [G,X]/G) & \simeq \mathbf{H}_{/\mathbf{B}G}(Y, [\ast, X \times \mathbf{B}G]_{\mathbf{B}G}) \\ & \simeq \mathbf{H}_{/\mathbf{B}G}( Y \times_{\mathbf{B}G} \ast, \underset{p^\ast X}{\underbrace{X \times \mathbf{B}G }} ) \\ & \simeq \mathbf{H}( \underset{hofib(Y)}{\underbrace{p_!(Y \times_{\mathbf{B}G} \ast)}}, X ) \\ & \simeq \mathbf{H}(hofib(Y),X) \end{aligned}

Here p:BG*p \colon \mathbf{B}G \to \ast denotes the terminal morphism and p !p *p_! \dashv p^\ast denotes the base change along it.

See also at double dimensional reduction for more on this.

Along V/GBGV/G \to \mathbf{B}G

More generally:


Let H\mathbf{H} be an (∞,1)-topos and GGrp(H)G \in Grp(\mathbf{H}) an ∞-group.

Let moreover VHV \in \mathbf{H} be an object equipped with a GG-∞-action ρ\rho, equivalently (by the discussion there) a homotopy fiber sequence of the form

V V/G p ρ BG \array{ V \\ \downarrow \\ V/G & \overset{p_\rho}{\longrightarrow}& \mathbf{B}G }


  1. pullback along p ρp_\rho is the operation that assigns to a morphism c:XBGc \colon X \to \mathbf{B}G the VV-fiber ∞-bundle which is associated via ρ\rho to the GG-principal ∞-bundle P cP_c classified by cc:

    (p ρ) *:cP c× GV (p_\rho)^\ast \;\colon\; c \mapsto P_c \times_G V
  2. the right base change along p ρp_\rho is given on objects of the form X×(V/G)X \times (V/G) by

    (p ρ) *:X×(V/G)[V,X]/G (p_\rho)_\ast \;\colon\; X \times (V/G) \;\mapsto\; [V,X]/G

The first statement is NSS 12, prop. 4.6.

The second statement follows as in the proof of prop. : Let

(Y c BG)H /BG \left( \array{ Y \\ \downarrow^{\mathrlap{c}} \\ \mathbf{B}G } \right) \;\in\; \mathbf{H}_{/\mathbf{B}G}

be any object, then there is the following sequence of natural equivalences

H /BG(Y,[V,X]/G) H /BG(Y,[V/G,X×BG] BG) H /BG(Y× BG(V/G),X×BGp *X) H /BG((p ρ) !(P c× G(V/G)),p *X) H /(V/G)(P c× GV,(p ρ) *p *X) H /(V/G)(P c× GV,X×(V/G)) \begin{aligned} \mathbf{H}_{/\mathbf{B}G}(Y, [V,X]/G) & \simeq \mathbf{H}_{/\mathbf{B}G}(Y, [V/G, X \times \mathbf{B}G]_{\mathbf{B}G}) \\ & \simeq \mathbf{H}_{/\mathbf{B}G}( Y \times_{\mathbf{B}G} (V/G), \underset{p^\ast X}{\underbrace{X \times \mathbf{B}G }} ) \\ & \simeq \mathbf{H}_{/\mathbf{B}G} ( (p_\rho)_!( P_c \times_G (V/G) ), p^\ast X ) \\ & \simeq \mathbf{H}_{/(V/G)} ( P_c \times_G V, (p_\rho)^\ast p^\ast X ) \\ & \simeq \mathbf{H}_{/(V/G)}(P_c \times_G V, X \times (V/G)) \end{aligned}

where again

p:BG*. p \colon \mathbf{B}G \to \ast \,.

(symmetric powers)


G=Σ(n)Grp(Set)Grp(Grpd)LConstH G = \Sigma(n) \in Grp(Set) \hookrightarrow Grp(\infty Grpd) \overset{LConst}{\longrightarrow} \mathbf{H}

be the symmetric group on nn elements, and

V={1,,n}SetGrpdLConstH V = \{1, \cdots, n\} \in Set \hookrightarrow \infty Grpd \overset{LConst}{\longrightarrow} \mathbf{H}

the nn-element set (h-set) equipped with the canonical Σ(n)\Sigma(n)-action. Then prop. says that right base change of any p ρ *p *Xp_\rho^\ast p^\ast X along

{1,,n}/Σ(n)BΣ(n) \{1, \cdots, n\}/\Sigma(n) \longrightarrow \mathbf{B}\Sigma(n)

is equivalently the nnth symmetric power of XX

[{1,,n},X]/Σ(n)(X n)/Σ(n). [\{1,\cdots, n\},X]/\Sigma(n) \simeq (X^n)/\Sigma(n) \,.


Standard textbook accounts include section A1.5.3 of

and section IV of

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