Documentation

Mathlib.CategoryTheory.Sites.Adjunction

In this file, we show that an adjunction G ⊣ F induces an adjunction between categories of sheaves. We also show that G preserves sheafification.

source
@[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.

Equations
Instances For
    source
    noncomputable 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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Sheaf.adjunction_unit_app_hom {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).hom = CategoryStruct.comp ((Adjunction.whiskerRight Cᵒᵖ adj).unit.app X.obj) (Functor.whiskerRight (toSheafify J (X.obj.comp G)) F)
      source
      @[deprecated CategoryTheory.Sheaf.adjunction_unit_app_hom (since := "2026-03-05")]
      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).hom = CategoryStruct.comp ((Adjunction.whiskerRight Cᵒᵖ adj).unit.app X.obj) (Functor.whiskerRight (toSheafify J (X.obj.comp G)) F)

      Alias of CategoryTheory.Sheaf.adjunction_unit_app_hom.

      source
      @[simp]
      theorem CategoryTheory.Sheaf.adjunction_counit_app_hom {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).hom = sheafifyLift J ((Adjunction.whiskerRight Cᵒᵖ adj).counit.app Y.obj) ⋯
      source
      @[deprecated CategoryTheory.Sheaf.adjunction_counit_app_hom (since := "2026-03-05")]
      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).hom = sheafifyLift J ((Adjunction.whiskerRight Cᵒᵖ adj).counit.app Y.obj) ⋯

      Alias of CategoryTheory.Sheaf.adjunction_counit_app_hom.

      source
      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
      source
      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
      source
      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
      source
      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