mathlib3 documentation

category_theory.sites.adjunction

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.

@[reducible]

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.

Equations