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₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.ConcreteCategory D] [J.HasSheafCompose (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.

Equations

• CategoryTheory.sheafForget J = (CategoryTheory.sheafCompose J (CategoryTheory.forget D)).comp (CategoryTheory.sheafEquivSheafOfTypes J).functor

@[simp]

theorem CategoryTheory.Sheaf.composeEquiv_apply_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [CategoryTheory.HasWeakSheafify J D] [J.HasSheafCompose F] (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.whiskerRight Cᵒᵖ adj).homEquiv X.val Y.val) (CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J (((CategoryTheory.whiskeringRight Cᵒᵖ E D).obj G).obj X.val)) η.val)

@[simp]

theorem CategoryTheory.Sheaf.composeEquiv_symm_apply_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [CategoryTheory.HasWeakSheafify J D] [J.HasSheafCompose F] (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.sheafifyLift J (((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).homEquiv ((CategoryTheory.sheafToPresheaf J E).obj X) Y.val).symm ((CategoryTheory.sheafToPresheaf J E).map γ)) ⋯

def CategoryTheory.Sheaf.composeEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [CategoryTheory.HasWeakSheafify J D] [J.HasSheafCompose F] (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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

def CategoryTheory.Sheaf.adjunction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [CategoryTheory.HasWeakSheafify J D] [J.HasSheafCompose F] (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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev CategoryTheory.Sheaf.composeAndSheafifyFromTypes {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.HasWeakSheafify J 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.

Equations

• CategoryTheory.Sheaf.composeAndSheafifyFromTypes J G = (CategoryTheory.sheafEquivSheafOfTypes J).inverse.comp (CategoryTheory.Sheaf.composeAndSheafify J G)

def CategoryTheory.Sheaf.adjunctionToTypes {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.ConcreteCategory D] [J.HasSheafCompose (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.

Equations

• CategoryTheory.Sheaf.adjunctionToTypes J adj = (CategoryTheory.sheafEquivSheafOfTypes J).symm.toAdjunction.comp (CategoryTheory.Sheaf.adjunction J adj)

@[simp]

theorem CategoryTheory.Sheaf.adjunctionToTypes_unit_app_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.ConcreteCategory D] [J.HasSheafCompose (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.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 u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.ConcreteCategory D] [J.HasSheafCompose (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.sheafifyLift J (CategoryTheory.CategoryStruct.comp (X.1.associator (CategoryTheory.forget D) G).hom ((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).counit.app X.1)) ⋯

instance CategoryTheory.Sheaf.instIsRightAdjointSheafOfTypesSheafForgetOfForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.ConcreteCategory D] [J.HasSheafCompose (CategoryTheory.forget D)] [(CategoryTheory.forget D).IsRightAdjoint] : (CategoryTheory.sheafForget J).IsRightAdjoint

Equations

• ⋯ = ⋯