internal sheaf



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 Sh^ 2(𝒮,can)\hat Sh_2(\mathcal{S},can) of the given ambient topos 𝒮\mathcal{S}, since an internal presheaf is to be an 𝒮\mathcal{S}-valued internal functor, but 𝒮\mathcal{S} does not quite sit inside itself. It does, however, sit inside Sh^ 2(𝒮,can)\hat Sh_2(\mathcal{S},can), incarnated as the 2-sheaf 𝒮¯\bar \mathcal{S} corresponding to its codomain fibration.

Therefore, regarding Sh^ 2(𝒮,can)\hat Sh_2(\mathcal{S}, can) as the 2-category of internal categories in 𝒮\mathcal{S}, an internal site in 𝒮\mathcal{S} is an object ¯\bar \mathbb{C} of Sh^ 2(𝒮,can)\hat Sh_2(\mathcal{S}, can) and an internal presheaf is a morphism F:¯ op𝒮¯F : \bar \mathbb{C}^{op} \to \bar \mathcal{S}.


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 𝒮\mathcal{S} be a topos and let \mathbb{C} be an internal category in 𝒮\mathcal{S}:

=(C 1tsC 0)𝒮. \mathbb{C} = \left( C_1 \stackrel{\overset{s}{\to}}{\underset{t}{\to}} C_0 \right) \in \mathcal{S} \,.

Write ¯\bar \mathbb{C} for the 2-sheaf on 𝒮\mathcal{S}

¯:𝒮 opCat \bar \mathbb{C} : \mathcal{S}^{op} \to Cat

that is represented by \mathbb{C}. More explicitly, this is the pseudofunctor which to an object X𝒮X \in \mathcal{S} assigns

¯:X(𝒮(X,C 1)𝒮(X,t)𝒮(X,s)𝒮(X,C 0)). \bar \mathbb{C} : X \mapsto \left( \mathcal{S}(X,C_1) \stackrel{\overset{\mathcal{S}(X,s)}{\to}}{\underset{\mathcal{S}(X,t)}{\to}} \mathcal{S}(X,C_0) \right) \,.


𝒮¯:𝒮 opCat \bar \mathcal{S} : \mathcal{S}^{op} \to Cat

for the 2-sheaf that classifies the codomain fibration of 𝒮\mathcal{S}, the pseudofunctor which sends an object to the corresponding slice topos and morphisms to base change

𝒮¯:X𝒮 /X \bar \mathcal{S} : X \mapsto \mathcal{S}_{/X}

(also called the “self-indexing of 𝒮\mathcal{S}”).


This is the incarnation of 𝒮\mathcal{S} itself, regard internal to its 2-sheaf 2-topos Sh^ 2(𝒯,can)\hat Sh_{2}(\mathcal{T}, can).


An internal presheaf on \mathbb{C} (internal to 𝒯\mathcal{T}) is a morphism

F:¯ op𝒮¯ F : \bar \mathbb{C}^{op} \to \bar \mathcal{S}

of 2-sheaves on 𝒮\mathcal{S}. (Also called an “indexed functor” between indexed categories“.)

Suppose moreover that \mathbb{C} is equipped with the structure of an internal site. Then FF above is an internal sheaf on \mathbb{C} if it satisfies the evident descent condition.

A morphism of internal presheaves is simply a 2-morphism in Sh^ 2(𝒮,can)\hat Sh_2(\mathcal{S}, can) (also called an “indexed natural transformation”). This yields a category

PSh() PSh(\mathbb{C})

of internal presheaves. Accordingly we have the full subcategory

Sh(,𝒮)PSh(,𝒮) Sh(\mathbb{C}, \mathcal{S}) \hookrightarrow PSh(\mathbb{C}, \mathcal{S})

of internal sheaves.

Explicit definition

We unwind what the above amounts to more explicitly.

Let (,J)(\mathbb{C},J) be an internal site in 𝒮\mathcal{S}, i.e. an internal category \mathbb{C} equipped with an internal coverage JJ. Let 𝒮 op\mathcal{S}^{\mathbb{C}^{op}} be the topos of internal diagrams on op\mathbb{C}^{op}.

  1. An internal presheaf on \mathbb{C} is an internal diagram F𝒮 opF \in \mathcal{S}^{\mathbb{C}^{op}}.

  2. An internal sheaf on \mathbb{C} (with respect to JJ) is an internal presheaf on \mathbb{C} satisfying one of the following equivalent conditions:

    1. FF satisfies the usual sheaf condition interpreted in the internal language of 𝒮\mathcal{S}.
    2. FF is a jj-sheaf for the Lawvere-Tierney topology on 𝒮 op\mathcal{S}^{\mathbb{C}^{op}} induced by JJ. (The equivalence is because the usual proof for 𝒮=\mathcal{S} = Set is constructive and can thus be internalized in an arbitrary topos.)


Let 𝒮\mathcal{S} and \mathbb{C} be as above.


The category of internal presheaves PSh(,𝒮)PSh(\mathbb{C}, \mathcal{S}) is a topos.

This appears as (Johnstone, cor. B.2.3.17).


Let f:𝔻f : \mathbb{C} \to \mathbb{D} be an internal functor. Write f¯:¯𝔻¯\bar f : \bar \mathbb{C} \to \bar \mathbb{D} for the corresponding morphism in Sh^ 2(𝒮,can)\hat Sh_2(\mathcal{S}, can). Precomposition with this morphism induces a functor of internal presheaf catgeories

f *:PSh(𝔻,𝒮)PSh(,𝒮). f^* : PSh(\mathbb{D}, \mathcal{S}) \to PSh(\mathbb{C}, \mathcal{S}) \,.

This is the inverse image of a geometric morphism of toposes

f:PSh(,𝒮)PSh(𝔻,𝒮). f : PSh(\mathbb{C}, \mathcal{S}) \to PSh(\mathbb{D}, \mathcal{S}) \,.

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).

category: sheaf theory

Revised on March 6, 2013 19:50:35 by Zoran Škoda (