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