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 . (In Set, would be the index set of the family, and the fiber of the bundle over an element of would be the set indexed by . Conversely, given a family of sets, can be constructed as its disjoint union.)
In these terms, the cartesian product of the family of sets is the set of (global) sections of the bundle. This set comes equipped with an evaluation map such that
equals the usual product projection from to , so and are both morphisms in the over category . The universal property of is that, given any set and morphism in , there's a unique map that makes everything commute.
In other words, and define an adjunction from to in which taking the product with 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 is secretly , where is the one-point set (the final object), and move everything from to an arbitrary over category .
Let be a category, and a morphism in , such that pullbacks along this morphism exist. These then constitute the base change functor between the corresponding slice categories
The dependent product along is, if it exists, the right adjoint functor to the base change along
So a category with all dependent products is necessarily a category with all pullbacks.
Let be a cartesian closed category with all limits and note that . Let be any object and identify it with the terminal morphism . Then the dependent product functor
sends bundles to their object of sections.
We check the characterizing natural isomorphism for the adjunction: For every we have the following sequence of natural isos:
This statement and its proof remain valid in homotopy theory. More in detail, if is a simplicial model category, , and are cofibrant, and are fibrant and is a fibration, then as above is the homotopy-correct derived section space.
As a special case of prop. one obtains exponential objects/internal homs.
Let have a terminal object . Let and in be objects and let and be the terminal morphisms.
The dependent product along of the arrow obtained by base change of along is the exponential object :
This is essentially a categorified version of the familiar fact that the exponentiation of two natural numbers can be identified with the product of copies of .
Consider the chain of equivalences from to in Set: Firstly, the exponential object is characterized in as right adjoint to . Secondly, the elements of are in turn in bijection with those functions from , that leave the second component fixed. The condition just stated is the definition of arrows in the overcategory , between the right projections out of resp. . If we identify objects with their terminal morphisms in , those two right projections are the pullbacks and , respectively. Thirdly, thus, the subset of we are interested in corresponds to in . Finally, the right adjoint to is a functor from to , such that . Hence must correspond to .
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 “-types”):
Dependent products (and sums) exist in any topos:
For a topos and any morphism in , both the left adjoint as well as the right adjoint to exist.
Moreover, 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 an (∞,1)-topos and an group object in (an ∞-group), then the slice (∞,1)-topos over its delooping may be identified with the (∞,1)-category of -∞-actions (see there for more):
Under this identification, then dependent product along a morphism of the form (corresponding to an ∞-group homomorphism ) corresponds to forming coinduced representations.
As the special case of the above for the trivial group we obtain the following:
Let be any (∞,1)-topos and let be a group object in (an ∞-group). Then the dependent product along the canonical point inclusion
into the delooping of takes the following form:
There is a pair of adjoint ∞-functors of the form
where
denotes the operation of taking the homotopy fiber of a map to over the canonical basepoint;
denotes the internal hom in ;
denotes the homotopy quotient by the conjugation ∞-action for equipped with its canonical ∞-action by left multiplication and the argument regarded as equipped with its trivial --action
(for then this is the cyclic loop space construction).
Hence for
a coefficient object, such as for some differential generalized cohomology theory
then there is a natural equivalence
given by
The statement that follows immediately by the definitions. What we need to show is that the dependent product along is given as claimed.
To that end, first observe that the conjugation action on is the internal hom in the (∞,1)-category of -∞-actions . Under the equivalence of (∞,1)-categories
(from NSS 12) then with its canonical ∞-action is and with the trivial action is .
Hence
So far this is the very definition of what is to mean in the first place.
But now since the slice (∞,1)-topos is itself cartesian closed, via
it is immediate that there is the following sequence of natural equivalences
Here denotes the terminal morphism and denotes the base change along it.
See also at double dimensional reduction for more on this.
More generally:
Let be an (∞,1)-topos and an ∞-group.
Let moreover be an object equipped with a -∞-action , equivalently (by the discussion there) a homotopy fiber sequence of the form
Then
pullback along is the operation that assigns to a morphism the -fiber ∞-bundle which is associated via to the -principal ∞-bundle classified by :
the right base change along is given on objects of the form by
The first statement is NSS 12, prop. 4.6.
The second statement follows as in the proof of prop. : Let
be any object, then there is the following sequence of natural equivalences
where again
(symmetric powers)
Let
be the symmetric group on elements, and
the -element set (h-set) equipped with the canonical -action. Then prop. says that right base change of any along
is equivalently the th symmetric power of
dependent sum, dependent product
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.