In this file, we show that an adjunction F ⊣ G induces an adjunction between categories of sheaves, under certain hypotheses on F and G.

@[inline, reducible]

abbrev CategoryTheory.sheafForget {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] : CategoryTheory.Functor (CategoryTheory.Sheaf J D) (CategoryTheory.SheafOfTypes J)

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

@[inline, reducible]

abbrev CategoryTheory.Sheaf.composeAndSheafify {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} E] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (G : CategoryTheory.Functor E D) : CategoryTheory.Functor (CategoryTheory.Sheaf J E) (CategoryTheory.Sheaf J D)

This is the functor sending a sheaf X : Sheaf J E to the sheafification of X ⋙ G.

@[simp]

theorem CategoryTheory.Sheaf.composeEquiv_symm_apply_val {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [(X : C) → (S : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S P)) F] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (adj : G ⊣ F) (X : CategoryTheory.Sheaf J E) (Y : CategoryTheory.Sheaf J D) (γ : X ⟶ (CategoryTheory.sheafCompose J F).obj Y) : (↑(CategoryTheory.Sheaf.composeEquiv J adj X Y).symm γ).val = CategoryTheory.GrothendieckTopology.sheafifyLift J (↑(CategoryTheory.Adjunction.homEquiv (CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj) ((CategoryTheory.sheafToPresheaf J E).obj X) Y.val).symm ((CategoryTheory.sheafToPresheaf J E).map γ)) (_ : CategoryTheory.Presheaf.IsSheaf J Y.val)

@[simp]

theorem CategoryTheory.Sheaf.composeEquiv_apply_val {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [(X : C) → (S : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S P)) F] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (adj : G ⊣ F) (X : CategoryTheory.Sheaf J E) (Y : CategoryTheory.Sheaf J D) (η : (CategoryTheory.Sheaf.composeAndSheafify J G).obj X ⟶ Y) : (↑(CategoryTheory.Sheaf.composeEquiv J adj X Y) η).val = ↑(CategoryTheory.Adjunction.homEquiv (CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj) ((CategoryTheory.sheafToPresheaf J E).obj X) Y.val) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.toSheafify J (((CategoryTheory.whiskeringRight Cᵒᵖ E D).obj G).obj ((CategoryTheory.sheafToPresheaf J E).obj X))) η.val)

def CategoryTheory.Sheaf.composeEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [(X : C) → (S : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S P)) F] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (adj : G ⊣ F) (X : CategoryTheory.Sheaf J E) (Y : CategoryTheory.Sheaf J D) : ((CategoryTheory.Sheaf.composeAndSheafify J G).obj X ⟶ Y) ≃ (X ⟶ (CategoryTheory.sheafCompose J F).obj Y)

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

@[simp]

theorem CategoryTheory.Sheaf.adjunction_counit_app_val {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [(X : C) → (S : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S P)) F] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (adj : G ⊣ F) (Y : CategoryTheory.Sheaf J D) : ((CategoryTheory.Sheaf.adjunction J adj).counit.app Y).val = CategoryTheory.GrothendieckTopology.sheafifyLift J (↑(CategoryTheory.Adjunction.homEquiv (CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj) (CategoryTheory.Functor.comp Y.val F) Y.val).symm (CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.comp Y.val F))) (_ : CategoryTheory.Presheaf.IsSheaf J Y.val)

@[simp]

theorem CategoryTheory.Sheaf.adjunction_unit_app_val {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [(X : C) → (S : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S P)) F] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (adj : G ⊣ F) (X : CategoryTheory.Sheaf J E) : ((CategoryTheory.Sheaf.adjunction J adj).unit.app X).val = ↑(CategoryTheory.Adjunction.homEquiv (CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj) X.val (CategoryTheory.GrothendieckTopology.sheafify J (CategoryTheory.Functor.comp X.val G))) (CategoryTheory.GrothendieckTopology.toSheafify J (CategoryTheory.Functor.comp X.val G))

def CategoryTheory.Sheaf.adjunction {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [(X : C) → (S : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S P)) F] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (adj : G ⊣ F) : CategoryTheory.Sheaf.composeAndSheafify J G ⊣ CategoryTheory.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 F preserves the correct limits.

instance CategoryTheory.Sheaf.instIsRightAdjointSheafInstCategorySheafSheafInstCategorySheafSheafComposeCoverFunctorOppositeOpposite {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} E] {F : CategoryTheory.Functor D E} [(X : C) → (S : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S P)) F] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] [CategoryTheory.IsRightAdjoint F] : CategoryTheory.IsRightAdjoint (CategoryTheory.sheafCompose J F)

@[inline, reducible]

abbrev CategoryTheory.Sheaf.composeAndSheafifyFromTypes {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (G : CategoryTheory.Functor (Type (max v u)) D) : CategoryTheory.Functor (CategoryTheory.SheafOfTypes J) (CategoryTheory.Sheaf J D)

This is the functor sending a sheaf of types X to the sheafification of X ⋙ G.

def CategoryTheory.Sheaf.adjunctionToTypes {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] {G : CategoryTheory.Functor (Type (max v u)) D} (adj : G ⊣ CategoryTheory.forget D) : CategoryTheory.Sheaf.composeAndSheafifyFromTypes J G ⊣ CategoryTheory.sheafForget J

A variant of the adjunction between sheaf categories, in the case where the right adjoint is the forgetful functor to sheaves of types.

@[simp]

theorem CategoryTheory.Sheaf.adjunctionToTypes_unit_app_val {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] {G : CategoryTheory.Functor (Type (max v u)) D} (adj : G ⊣ CategoryTheory.forget D) (Y : CategoryTheory.SheafOfTypes J) : ((CategoryTheory.Sheaf.adjunctionToTypes J adj).unit.app Y).val = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).unit.app ((CategoryTheory.sheafOfTypesToPresheaf J).obj Y)) (CategoryTheory.whiskerRight (CategoryTheory.GrothendieckTopology.toSheafify J (((CategoryTheory.whiskeringRight Cᵒᵖ (Type (max v u)) D).obj G).obj ((CategoryTheory.sheafOfTypesToPresheaf J).obj Y))) (CategoryTheory.forget D))

@[simp]

theorem CategoryTheory.Sheaf.adjunctionToTypes_counit_app_val {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] {G : CategoryTheory.Functor (Type (max v u)) D} (adj : G ⊣ CategoryTheory.forget D) (X : CategoryTheory.Sheaf J D) : ((CategoryTheory.Sheaf.adjunctionToTypes J adj).counit.app X).val = CategoryTheory.GrothendieckTopology.sheafifyLift J (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.associator X.1 (CategoryTheory.forget D) G).hom ((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).counit.app X.1)) (_ : CategoryTheory.Presheaf.IsSheaf J X.val)

instance CategoryTheory.Sheaf.instIsRightAdjointSheafOfTypesInstCategorySheafOfTypesSheafInstCategorySheafSheafForget {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] [CategoryTheory.IsRightAdjoint (CategoryTheory.forget D)] : CategoryTheory.IsRightAdjoint (CategoryTheory.sheafForget J)