In this file, we show that an adjunction
F ⊣ G induces an adjunction between
categories of sheaves, under certain hypotheses on
The forgetful functor from
Sheaf J D to sheaves of types, for a concrete category
whose forgetful functor preserves the correct limits.
This is the functor sending a sheaf
X : Sheaf J E to the sheafification
X ⋙ G.
An auxiliary definition to be used in defining
adj : G ⊣ F with
F : D ⥤ E and
G : E ⥤ D induces an adjunction
Sheaf J D and
Sheaf J E, in contexts where one can sheafify
F preserves the correct limits.
This is the functor sending a sheaf of types
X to the sheafification of
X ⋙ G.
A variant of the adjunction between sheaf categories, in the case where the right adjoint is the forgetful functor to sheaves of types.