Could not include topos theory - contents
Internal category theory
The notions of presheaf, site and sheaf can be formulated internal to any topos. The ordinary such notions are recovered by internalization into Set.
More precisely, the direct internalization of these notions is into the very large 2-topos of the given ambient topos , since an internal presheaf is to be an -valued internal functor, but does not quite sit inside itself. It does, however, sit inside , incarnated as the 2-sheaf corresponding to its codomain fibration.
Therefore, regarding as the 2-category of internal categories in , an internal site in is an object of and an internal presheaf is a morphism .
While it is straightforward to define an internal site, hence the domain of an internal (pre)sheaf, the definition of the codomain is slightly more subtle, for that needs to be an copy of the ambient universe internalized into itself. One way to naturally say this is by passing to the external 2-sheaves 2-topos. This version of the definition we state in
But the resulting notion can of course be expressed entirely in terms of data in the ambient topos. This we spell out in
In terms of external 2-sheaves
Let be a topos and let be an internal category in :
Write for the 2-sheaf on
that is represented by . More explicitly, this is the pseudofunctor which to an object assigns
An internal presheaf on (internal to ) is a morphism
of 2-sheaves on . (Also called an “indexed functor” between indexed categories“.)
Suppose moreover that is equipped with the structure of an internal site. Then above is an internal sheaf on if it satisfies the evident descent condition.
A morphism of internal presheaves is simply a 2-morphism in (also called an “indexed natural transformation”). This yields a category
of internal presheaves. Accordingly we have the full subcategory
of internal sheaves.
We unwind what the above amounts to more explicitly.
Let be an internal site in , i.e. an internal category equipped with an internal coverage . Let be the topos of internal diagrams on .
An internal presheaf on is an internal diagram .
An internal sheaf on (with respect to ) is an internal presheaf on satisfying one of the following equivalent conditions:
- satisfies the usual sheaf condition interpreted in the internal language of .
- is a -sheaf for the Lawvere-Tierney topology on induced by . (The equivalence is because the usual proof for Set is constructive and can thus be internalized in an arbitrary topos.)
Let and be as above.
The category of internal presheaves is a topos.
This appears as (Johnstone, cor. B.2.3.17).
Let be an internal functor. Write for the corresponding morphism in . Precomposition with this morphism induces a functor of internal presheaf catgeories
This is the inverse image of a geometric morphism of toposes
This appears as (Johnstone, cor. B.2.3.22).
Internal presheaves in a Grothendieck topos are discussed in Section V.7 of
and in section B2.3 of
In these references internal presheaves are introduced in components as in the explicit definition above. The equivalence to the abstract formulation above, in terms of morphisms between 2-sheaves, follows for instance with (Johnstone, lemma B.2.3.13).