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 u_1} [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.GrothendieckTopology.HasSheafCompose J (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.Functor.comp (CategoryTheory.sheafCompose J (CategoryTheory.forget D)) (CategoryTheory.sheafEquivSheafOfTypes J).functor

@[inline, reducible]

abbrev CategoryTheory.Sheaf.composeAndSheafify {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_3, u_1} D] {E : Type u_2} [CategoryTheory.Category.{u_4, u_2} E] [CategoryTheory.HasWeakSheafify J 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.

Equations

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

@[simp]

theorem CategoryTheory.Sheaf.composeEquiv_symm_apply_val {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_3, u_1} D] {E : Type u_2} [CategoryTheory.Category.{u_4, u_2} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.GrothendieckTopology.HasSheafCompose J F] (adj : G ⊣ F) (X : CategoryTheory.Sheaf J E) (Y : CategoryTheory.Sheaf J D) (γ : X ⟶ (CategoryTheory.sheafCompose J F).toPrefunctor.obj Y) : ((CategoryTheory.Sheaf.composeEquiv J adj X Y).symm γ).val = CategoryTheory.sheafifyLift J (((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).homEquiv ((CategoryTheory.sheafToPresheaf J E).toPrefunctor.obj X) Y.val).symm ((CategoryTheory.sheafToPresheaf J E).toPrefunctor.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 u_1} [CategoryTheory.Category.{u_3, u_1} D] {E : Type u_2} [CategoryTheory.Category.{u_4, u_2} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.GrothendieckTopology.HasSheafCompose J F] (adj : G ⊣ F) (X : CategoryTheory.Sheaf J E) (Y : CategoryTheory.Sheaf J D) (η : (CategoryTheory.Sheaf.composeAndSheafify J G).toPrefunctor.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).toPrefunctor.obj G).toPrefunctor.obj X.val)) η.val)

def CategoryTheory.Sheaf.composeEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_3, u_1} D] {E : Type u_2} [CategoryTheory.Category.{u_4, u_2} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.GrothendieckTopology.HasSheafCompose J F] (adj : G ⊣ F) (X : CategoryTheory.Sheaf J E) (Y : CategoryTheory.Sheaf J D) : ((CategoryTheory.Sheaf.composeAndSheafify J G).toPrefunctor.obj X ⟶ Y) ≃ (X ⟶ (CategoryTheory.sheafCompose J F).toPrefunctor.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_unit_app_val {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_3, u_1} D] {E : Type u_2} [CategoryTheory.Category.{u_4, u_2} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.GrothendieckTopology.HasSheafCompose J 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).toPrefunctor.obj (CategoryTheory.Functor.comp X.val G)).val) (CategoryTheory.toSheafify J (CategoryTheory.Functor.comp X.val G))

@[simp]

theorem CategoryTheory.Sheaf.adjunction_counit_app_val {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_3, u_1} D] {E : Type u_2} [CategoryTheory.Category.{u_4, u_2} E] {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.GrothendieckTopology.HasSheafCompose J 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 (CategoryTheory.Functor.comp Y.val F) Y.val).symm (CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.comp Y.val F))) (_ : CategoryTheory.Presheaf.IsSheaf J Y.val)

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

• CategoryTheory.Sheaf.adjunction J adj = CategoryTheory.Adjunction.mkOfHomEquiv (CategoryTheory.Adjunction.CoreHomEquiv.mk (CategoryTheory.Sheaf.composeEquiv J adj))

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

Equations

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

@[inline, reducible]

abbrev CategoryTheory.Sheaf.composeAndSheafifyFromTypes {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_3, u_1} 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.Functor.comp (CategoryTheory.sheafEquivSheafOfTypes J).inverse (CategoryTheory.Sheaf.composeAndSheafify J G)

def CategoryTheory.Sheaf.adjunctionToTypes {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1} [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.GrothendieckTopology.HasSheafCompose J (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.Adjunction.comp (CategoryTheory.sheafEquivSheafOfTypes J).symm.toAdjunction (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_1} [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.GrothendieckTopology.HasSheafCompose J (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).toPrefunctor.obj Y)) (CategoryTheory.whiskerRight (CategoryTheory.toSheafify J (((CategoryTheory.whiskeringRight Cᵒᵖ (Type (max v u)) D).toPrefunctor.obj G).toPrefunctor.obj ((CategoryTheory.sheafOfTypesToPresheaf J).toPrefunctor.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_1} [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.GrothendieckTopology.HasSheafCompose J (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 (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 u_1} [CategoryTheory.Category.{u_3, u_1} D] [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.GrothendieckTopology.HasSheafCompose J (CategoryTheory.forget D)] [CategoryTheory.IsRightAdjoint (CategoryTheory.forget D)] : CategoryTheory.IsRightAdjoint (CategoryTheory.sheafForget J)

Equations

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