mathlib documentation


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.

An auxiliary definition to be used in defining category_theory.Sheaf.adjunction below.


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.