mathlib3 documentation


THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.