Documentation

Mathlib.CategoryTheory.Sites.PreservesSheafification

Functors which preserve sheafification #

In this file, given a Grothendieck topology J on C and F : A ⥤ B, we define a type class J.PreservesSheafification F. We say that F preserves the sheafification if whenever a morphism of presheaves P₁ ⟶ P₂ induces an isomorphism on the associated sheaves, then the induced map P₁ ⋙ F ⟶ P₂ ⋙ F also induces an isomorphism on the associated sheaves. (Note: it suffices to check this property for the map from any presheaf P to its associated sheaf, see GrothendieckTopology.preservesSheafification_iff_of_adjunctions).

In general, we define Sheaf.composeAndSheafify J F : Sheaf J A ⥤ Sheaf J B as the functor which sends a sheaf G to the sheafification of the composition G.val ⋙ F. If J.PreservesSheafification F, we show that this functor can also be thought of as the localization of the functor _ ⋙ F on presheaves: we construct an isomorphism presheafToSheafCompComposeAndSheafifyIso between presheafToSheaf J A ⋙ Sheaf.composeAndSheafify J F and (whiskeringRight Cᵒᵖ A B).obj F ⋙ presheafToSheaf J B.

Moreover, if we assume J.HasSheafCompose F, we obtain an isomorphism sheafifyComposeIso J F P : sheafify J (P ⋙ F) ≅ sheafify J P ⋙ F.

We show that under suitable assumptions, the forgetful functor from a concrete category preserves sheafification; this holds more generally for functors between such concrete categories which commute both with suitable limits and colimits.

TODO #

A functor F : A ⥤ B preserves the sheafification for the Grothendieck topology J on a category C if whenever a morphism of presheaves f : P₁ ⟶ P₂ in Cᵒᵖ ⥤ A is such that becomes an iso after sheafification, then it is also the case of whiskerRight f F : P₁ ⋙ F ⟶ P₂ ⋙ F.

Instances
    @[reducible, inline]
    noncomputable abbrev CategoryTheory.Sheaf.composeAndSheafify {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [Category.{u_3, u_1} A] [Category.{u_4, u_2} B] (F : Functor A B) [HasWeakSheafify J B] :
    Functor (Sheaf J A) (Sheaf J B)

    This is the functor sending a sheaf X : Sheaf J A to the sheafification of X.val ⋙ F.

    Equations
    Instances For

      The canonical natural transformation from (whiskeringRight Cᵒᵖ A B).obj F ⋙ presheafToSheaf J B to presheafToSheaf J A ⋙ Sheaf.composeAndSheafify J F.

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

        The canonical isomorphism between presheafToSheaf J A ⋙ Sheaf.composeAndSheafify J F and (whiskeringRight Cᵒᵖ A B).obj F ⋙ presheafToSheaf J B when F : A ⥤ B preserves sheafification.

        Equations
        Instances For

          The canonical natural transformation (whiskeringRight Cᵒᵖ A B).obj F ⋙ G₂ ⟶ G₁ ⋙ sheafCompose J F when F : A ⥤ B is such that J.HasSheafCompose F, and that G₁ and G₂ are left adjoints to the forget functors sheafToPresheaf.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem CategoryTheory.sheafComposeNatTrans_fac {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [Category.{u_3, u_1} A] [Category.{u_4, u_2} B] (F : Functor A B) {G₁ : Functor (Functor Cᵒᵖ A) (Sheaf J A)} (adj₁ : G₁ sheafToPresheaf J A) {G₂ : Functor (Functor Cᵒᵖ B) (Sheaf J B)} (adj₂ : G₂ sheafToPresheaf J B) [J.HasSheafCompose F] (P : Functor Cᵒᵖ A) :
            CategoryStruct.comp (adj₂.unit.app (P.comp F)) ((sheafToPresheaf J B).map ((sheafComposeNatTrans J F adj₁ adj₂).app P)) = whiskerRight (adj₁.unit.app P) F
            theorem CategoryTheory.sheafComposeNatTrans_app_uniq {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [Category.{u_3, u_1} A] [Category.{u_4, u_2} B] (F : Functor A B) {G₁ : Functor (Functor Cᵒᵖ A) (Sheaf J A)} (adj₁ : G₁ sheafToPresheaf J A) {G₂ : Functor (Functor Cᵒᵖ B) (Sheaf J B)} (adj₂ : G₂ sheafToPresheaf J B) [J.HasSheafCompose F] (P : Functor Cᵒᵖ A) (α : G₂.obj (P.comp F) (sheafCompose J F).obj (G₁.obj P)) (hα : CategoryStruct.comp (adj₂.unit.app (P.comp F)) ((sheafToPresheaf J B).map α) = whiskerRight (adj₁.unit.app P) F) :
            α = (sheafComposeNatTrans J F adj₁ adj₂).app P
            noncomputable def CategoryTheory.sheafComposeNatIso {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [Category.{u_3, u_1} A] [Category.{u_4, u_2} B] (F : Functor A B) {G₁ : Functor (Functor Cᵒᵖ A) (Sheaf J A)} (adj₁ : G₁ sheafToPresheaf J A) {G₂ : Functor (Functor Cᵒᵖ B) (Sheaf J B)} (adj₂ : G₂ sheafToPresheaf J B) [J.HasSheafCompose F] [J.PreservesSheafification F] :

            The canonical natural isomorphism (whiskeringRight Cᵒᵖ A B).obj F ⋙ G₂ ≅ G₁ ⋙ sheafCompose J F when F : A ⥤ B preserves sheafification, and that G₁ and G₂ are left adjoints to the forget functors sheafToPresheaf.

            Equations
            Instances For

              The canonical isomorphism sheafify J (P ⋙ F) ≅ sheafify J P ⋙ F when F preserves the sheafification.

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