Redirected from "ccc structure on presheaves".
Contents
Context
Monoidal categories
monoidal categories
With braiding
With duals for objects
With duals for morphisms
With traces
Closed structure
Special sorts of products
Semisimplicity
Morphisms
Internal monoids
Examples
Theorems
In higher category theory
Category theory
Contents
Idea
As every topos, a category of presheaves is cartesian closed monoidal.
Definition
Proposition
(cartesian closure of categories of presheaves)
Let be a small category and write for its category of presheaves.
This is
-
a cartesian monoidal category, whose Cartesian product is given objectwise in by the Cartesian product in Set:
for , their Cartesian product exists and is given by
-
a cartesian closed category, whose internal hom is given for by
Here denotes the Yoneda embedding and is the hom-functor on the category of presheaves.
(e.g. MacLane-Moerdijk, section I.6, pages 46-47).
Proof
The first statement is a special case of the general fact that limits of presheaves are computed objectwise.
For the second statement, first assume that does exist. Then by the hom-adjunction isomorphism we have for any other presheaf a natural isomorphism of the form
(1)
This holds in particular for a representable functor (i.e. in the essential image of the Yoneda embedding) and so the Yoneda lemma implies that if it exists, then must have the claimed form:
Hence it remains to show that this formula does make (1) hold generally.
For this we use the equivalent definition of adjoint functors in terms of the adjunction counit providing a system of universal arrows.
Define a would-be adjunction counit, which here is called an evaluation morphism, by
Then it remains to show that for every morphism of presheaves of the form there is a unique morphism such that
(2)
The commutativity of this diagram means in components at that, that for all and we have
Hence this fixes the component when its first argument is the identity morphism . But let be any morphism and chase through the naturality diagram for :
This shows that is fixed to be given by
at least on those pairs such that is in the image of .
But, finally, is also natural in
which implies that (3) must hold generally. Hence naturality implies that (2) indeed has a unique solution.
Definition in terms of homs of direct images
Often another, equivalent, expression is used to express the internal hom of presheaves:
Let be a pre-site with underlying category . Recall from the discussion at site that just means that we have a category on which we consider presheaves , but that it suggests that
-
to each object and in particular to each there is naturally associated the pre-site with underlying category the comma category ;
-
that the canonical forgetful functor , which can be thought of as a morphism of pre-sites induces the direct image functor which we write .
Then in these terms the above internal hom for presheaves
is expressed for all by
Relation of the two definitions
To see the equivalence of the two definitions, notice
- that by the Yoneda lemma we have that is simply the over category ;
- by the general properties of functors and comma categories there is an equivalence ;
- which identifies the functor with the functor ;
- and that .
Presheaves over a monoidal category
It is worth noting that in the case where is itself a monoidal category , is equipped with another (bi)closed monoidal structure given by the Day convolution product and its componentwise right adjoints. Let and be two presheaves over . Their tensor product can be defined by the following coend formula:
Then we can define two right adjoints
by the following end formulas:
In the case where the monoidal structure on is cartesian, the induced closed monoidal structure on coincides with the cartesian closed structure described in the previous sections.
References
The first definition is discussed for instance in section I.6 of
The second definition is discussed for instance in section 17.1 of