Limits and colimits
limits and colimits
limit and colimit
limits and colimits by example
commutativity of limits and colimits
connected limit, wide pullback
preserved limit, reflected limit, created limit
product, fiber product, base change, coproduct, pullback, pushout, cobase change, equalizer, coequalizer, join, meet, terminal object, initial object, direct product, direct sum
end and coend
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 . (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; in other words, is a morphism 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 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.
Relation to spaces of sections
Let be a cartesian closed category with all limits. Let be any object.
Then the dependent product functor
sends bundles to their object of sections.
One computes for every
Relation to exponential objects / internal homs
As a special case of the above one obtains exponential objects/internal homs.
Let have a terminal object . Let be any object and let be the terminal morphism.
The dependent product along of the base change along is the exponential object/internal hom
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.
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.
Standard textbook accounts include section A1.5.3 of
and section IV of