Documentation

Mathlib.CategoryTheory.Sites.Adjunction

In this file, we show that an adjunction G ⊣ F induces an adjunction between categories of sheaves. We also show that G preserves sheafification.

@[reducible, inline]

The forgetful functor from Sheaf J D to sheaves of types, for a concrete category D whose forgetful functor preserves the correct limits.

Equations
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 postcomposing with F preserves the property of being a sheaf.

    Equations
    • One or more equations did not get rendered due to their size.
    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.

      Equations
      Instances For