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 withFunctoriality 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 . DefineFor and , compatibility with the arrow givesThus 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 bijectionsFinite categorical products in the presheaf category are pointwise; in particular its terminal object is the constant singleton categorical presheaf. For categorical presheaves defineFor , 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 isNaturality 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 givesEvery 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
There are currently no matching articles.