Write . The category of elements of a categorical presheaf has objects with ; a morphism is satisfying . It is a small category because is small and each is a set. Consider the diagram sending to and to the natural transformation given by postcomposition with .
There is a canonical cocone with
Functoriality makes it a natural transformation, and the equation makes these transformations a cocone.
To prove its universal property, let be any categorical presheaf with a compatible cocone . Define
For and , compatibility with the arrow gives
Thus is natural. Naturality of each shows . Conversely any transformation with these equations must have the displayed values , so it is unique. We have proved the canonical colimit presentation of a presheaf:
A Cartesian closed category has finite categorical products and, for every , an exponential object with an evaluation morphism such that composition with evaluation gives natural bijections
Finite categorical products in the presheaf category are pointwise; in particular its terminal object is the constant singleton categorical presheaf. For categorical presheaves define
For , restriction sends to . Composition and identity laws follow from those of the Yoneda embedding, so this is a categorical presheaf.
Define evaluation at by . For , naturality of gives , which is the evaluation of the restricted pair. Hence evaluation is a natural transformation.
Given , its currying sends to the transformation whose component at is
Naturality in follows from that of , and naturality in follows by composing with the relevant arrow. Evaluating at recovers . Conversely, if , naturality of along says that evaluating at gives . Thus currying the evaluation of recovers . These constructions are inverse and natural, proving the universal property. This is the exponential in a presheaf category, and proves the presheaf category is Cartesian closed.
The Yoneda embedding preserves categorical products: for any , maps correspond naturally to pairs of maps and . Hence . Using the exponential in a presheaf category, the Yoneda lemma and the exponential universal property in gives
Every bijection is natural in , since it is given by precomposition or the natural exponential adjunction. Thus these component bijections are a natural isomorphism of categorical presheaves:

Articles by others on the same topic (0)

There are currently no matching articles.