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]

abbrev CategoryTheory.sheafForget {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] {FD : D → D → Type u_2} {CD : D → Type u_3} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] [J.HasSheafCompose (forget D)] : Functor (Sheaf J D) (Sheaf J (Type u_3))

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

def CategoryTheory.Sheaf.adjunction {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{v_1, u_1} E] {F : Functor D E} {G : Functor E D} [HasWeakSheafify J D] [J.HasSheafCompose F] (adj : G ⊣ F) : composeAndSheafify J G ⊣ sheafCompose J F

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.

@[simp]

theorem CategoryTheory.Sheaf.adjunction_unit_app_val {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{v_1, u_1} E] {F : Functor D E} {G : Functor E D} [HasWeakSheafify J D] [J.HasSheafCompose F] (adj : G ⊣ F) (X : Sheaf J E) : ((adjunction J adj).unit.app X).val = CategoryStruct.comp ((Adjunction.whiskerRight Cᵒᵖ adj).unit.app X.val) (Functor.whiskerRight (toSheafify J (X.val.comp G)) F)

@[simp]

theorem CategoryTheory.Sheaf.adjunction_counit_app_val {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{v_1, u_1} E] {F : Functor D E} {G : Functor E D} [HasWeakSheafify J D] [J.HasSheafCompose F] (adj : G ⊣ F) (Y : Sheaf J D) : ((adjunction J adj).counit.app Y).val = sheafifyLift J ((Adjunction.whiskerRight Cᵒᵖ adj).counit.app Y.val) ⋯

instance CategoryTheory.Sheaf.instIsRightAdjointSheafComposeOfHasWeakSheafify {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{v_1, u_1} E] {F : Functor D E} [HasWeakSheafify J D] [F.IsRightAdjoint] : (sheafCompose J F).IsRightAdjoint

instance CategoryTheory.Sheaf.instIsLeftAdjointComposeAndSheafify {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{v_1, u_1} E] {G : Functor E D} [HasWeakSheafify J D] [G.IsLeftAdjoint] : (composeAndSheafify J G).IsLeftAdjoint

theorem CategoryTheory.Sheaf.preservesSheafification_of_adjunction {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{v_1, u_1} E] {F : Functor D E} {G : Functor E D} (adj : G ⊣ F) : J.PreservesSheafification G

instance CategoryTheory.Sheaf.instPreservesSheafificationOfIsLeftAdjoint {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{v_1, u_1} E] {G : Functor E D} [G.IsLeftAdjoint] : J.PreservesSheafification G