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

• construct an isomorphism Sheaf.composeAndSheafify J F ≅ sheafCompose J F

class CategoryTheory.GrothendieckTopology.PreservesSheafification {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor A B) : Prop

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.

• le : J.W ≤ J.W.inverseImage ((CategoryTheory.whiskeringRight Cᵒᵖ A B).obj F)

theorem CategoryTheory.GrothendieckTopology.W_of_preservesSheafification {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor A B) [J.PreservesSheafification F] {P₁ P₂ : CategoryTheory.Functor Cᵒᵖ A} (f : P₁ ⟶ P₂) (hf : J.W f) : J.W (CategoryTheory.whiskerRight f F)

theorem CategoryTheory.GrothendieckTopology.W_isInvertedBy_whiskeringRight_presheafToSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor A B) [J.PreservesSheafification F] [CategoryTheory.HasWeakSheafify J B] : J.W.IsInvertedBy (((CategoryTheory.whiskeringRight Cᵒᵖ A B).obj F).comp (CategoryTheory.presheafToSheaf J B))

@[reducible, inline]

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

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

Equations

• CategoryTheory.Sheaf.composeAndSheafify J F = (CategoryTheory.sheafToPresheaf J A).comp (((CategoryTheory.whiskeringRight Cᵒᵖ A B).obj F).comp (CategoryTheory.presheafToSheaf J B))

noncomputable def CategoryTheory.toPresheafToSheafCompComposeAndSheafify {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J B] [CategoryTheory.HasWeakSheafify J A] : ((CategoryTheory.whiskeringRight Cᵒᵖ A B).obj F).comp (CategoryTheory.presheafToSheaf J B) ⟶ (CategoryTheory.presheafToSheaf J A).comp (CategoryTheory.Sheaf.composeAndSheafify J F)

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.

@[simp]

theorem CategoryTheory.toPresheafToSheafCompComposeAndSheafify_app {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J B] [CategoryTheory.HasWeakSheafify J A] (X : CategoryTheory.Functor Cᵒᵖ A) : (CategoryTheory.toPresheafToSheafCompComposeAndSheafify J F).app X = (CategoryTheory.presheafToSheaf J B).map (CategoryTheory.whiskerRight (CategoryTheory.toSheafify J X) F)

instance CategoryTheory.instIsIsoFunctorOppositeSheafToPresheafToSheafCompComposeAndSheafify {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J B] [CategoryTheory.HasWeakSheafify J A] [J.PreservesSheafification F] : CategoryTheory.IsIso (CategoryTheory.toPresheafToSheafCompComposeAndSheafify J F)

noncomputable def CategoryTheory.presheafToSheafCompComposeAndSheafifyIso {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J B] [CategoryTheory.HasWeakSheafify J A] [J.PreservesSheafification F] : (CategoryTheory.presheafToSheaf J A).comp (CategoryTheory.Sheaf.composeAndSheafify J F) ≅ ((CategoryTheory.whiskeringRight Cᵒᵖ A B).obj F).comp (CategoryTheory.presheafToSheaf J B)

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

• CategoryTheory.presheafToSheafCompComposeAndSheafifyIso J F = (CategoryTheory.asIso (CategoryTheory.toPresheafToSheafCompComposeAndSheafify J F)).symm

@[simp]

theorem CategoryTheory.presheafToSheafCompComposeAndSheafifyIso_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J B] [CategoryTheory.HasWeakSheafify J A] [J.PreservesSheafification F] (X : CategoryTheory.Functor Cᵒᵖ A) : (CategoryTheory.presheafToSheafCompComposeAndSheafifyIso J F).inv.app X = (CategoryTheory.presheafToSheaf J B).map (CategoryTheory.whiskerRight (CategoryTheory.toSheafify J X) F)

noncomputable instance CategoryTheory.instLiftingFunctorOppositeSheafPresheafToSheafWCompObjWhiskeringRightComposeAndSheafify {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J B] [CategoryTheory.HasWeakSheafify J A] [J.PreservesSheafification F] : CategoryTheory.Localization.Lifting (CategoryTheory.presheafToSheaf J A) J.W (((CategoryTheory.whiskeringRight Cᵒᵖ A B).obj F).comp (CategoryTheory.presheafToSheaf J B)) (CategoryTheory.Sheaf.composeAndSheafify J F)

Equations

• CategoryTheory.instLiftingFunctorOppositeSheafPresheafToSheafWCompObjWhiskeringRightComposeAndSheafify J F = { iso' := CategoryTheory.presheafToSheafCompComposeAndSheafifyIso J F }

theorem CategoryTheory.GrothendieckTopology.preservesSheafification_iff_of_adjunctions {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_4, u_1} A] [CategoryTheory.Category.{u_3, u_2} B] (F : CategoryTheory.Functor A B) {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A) {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)} (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) : J.PreservesSheafification F ↔ ∀ (P : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.IsIso (G₂.map (CategoryTheory.whiskerRight (adj₁.unit.app P) F))

def CategoryTheory.sheafComposeNatTrans {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor A B) {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A) {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)} (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [J.HasSheafCompose F] : ((CategoryTheory.whiskeringRight Cᵒᵖ A B).obj F).comp G₂ ⟶ G₁.comp (CategoryTheory.sheafCompose J F)

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.

theorem CategoryTheory.sheafComposeNatTrans_fac {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor A B) {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A) {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)} (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [J.HasSheafCompose F] (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.CategoryStruct.comp (adj₂.unit.app (P.comp F)) ((CategoryTheory.sheafToPresheaf J B).map ((CategoryTheory.sheafComposeNatTrans J F adj₁ adj₂).app P)) = CategoryTheory.whiskerRight (adj₁.unit.app P) F

theorem CategoryTheory.sheafComposeNatTrans_app_uniq {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor A B) {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A) {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)} (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [J.HasSheafCompose F] (P : CategoryTheory.Functor Cᵒᵖ A) (α : G₂.obj (P.comp F) ⟶ (CategoryTheory.sheafCompose J F).obj (G₁.obj P)) (hα : CategoryTheory.CategoryStruct.comp (adj₂.unit.app (P.comp F)) ((CategoryTheory.sheafToPresheaf J B).map α) = CategoryTheory.whiskerRight (adj₁.unit.app P) F) : α = (CategoryTheory.sheafComposeNatTrans J F adj₁ adj₂).app P

theorem CategoryTheory.GrothendieckTopology.preservesSheafification_iff_of_adjunctions_of_hasSheafCompose {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor A B) {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A) {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)} (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [J.HasSheafCompose F] : J.PreservesSheafification F ↔ CategoryTheory.IsIso (CategoryTheory.sheafComposeNatTrans J F adj₁ adj₂)

instance CategoryTheory.instIsIsoFunctorOppositeSheafSheafComposeNatTrans {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor A B) {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A) {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)} (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [J.HasSheafCompose F] [J.PreservesSheafification F] : CategoryTheory.IsIso (CategoryTheory.sheafComposeNatTrans J F adj₁ adj₂)

noncomputable def CategoryTheory.sheafComposeNatIso {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor A B) {G₁ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)} (adj₁ : G₁ ⊣ CategoryTheory.sheafToPresheaf J A) {G₂ : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ B) (CategoryTheory.Sheaf J B)} (adj₂ : G₂ ⊣ CategoryTheory.sheafToPresheaf J B) [J.HasSheafCompose F] [J.PreservesSheafification F] : ((CategoryTheory.whiskeringRight Cᵒᵖ A B).obj F).comp G₂ ≅ G₁.comp (CategoryTheory.sheafCompose J 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

• CategoryTheory.sheafComposeNatIso J F adj₁ adj₂ = CategoryTheory.asIso (CategoryTheory.sheafComposeNatTrans J F adj₁ adj₂)

noncomputable def CategoryTheory.sheafifyComposeIso {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_3, u_1} A] [CategoryTheory.Category.{u_4, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [J.HasSheafCompose F] [J.PreservesSheafification F] (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.sheafify J (P.comp F) ≅ (CategoryTheory.sheafify J P).comp F

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.

@[simp]

theorem CategoryTheory.sheafComposeIso_hom_fac {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_4, u_1} A] [CategoryTheory.Category.{u_3, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [J.HasSheafCompose F] [J.PreservesSheafification F] (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J (P.comp F)) (CategoryTheory.sheafifyComposeIso J F P).hom = CategoryTheory.whiskerRight (CategoryTheory.toSheafify J P) F

@[simp]

theorem CategoryTheory.sheafComposeIso_hom_fac_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_4, u_1} A] [CategoryTheory.Category.{u_3, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [J.HasSheafCompose F] [J.PreservesSheafification F] (P : CategoryTheory.Functor Cᵒᵖ A) {Z : CategoryTheory.Functor Cᵒᵖ B} (h : (CategoryTheory.sheafify J P).comp F ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J (P.comp F)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyComposeIso J F P).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.toSheafify J P) F) h

@[simp]

theorem CategoryTheory.sheafComposeIso_inv_fac {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_4, u_1} A] [CategoryTheory.Category.{u_3, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [J.HasSheafCompose F] [J.PreservesSheafification F] (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.toSheafify J P) F) (CategoryTheory.sheafifyComposeIso J F P).inv = CategoryTheory.toSheafify J (P.comp F)

@[simp]

theorem CategoryTheory.sheafComposeIso_inv_fac_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_4, u_1} A] [CategoryTheory.Category.{u_3, u_2} B] (F : CategoryTheory.Functor A B) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify J B] [J.HasSheafCompose F] [J.PreservesSheafification F] (P : CategoryTheory.Functor Cᵒᵖ A) {Z : CategoryTheory.Functor Cᵒᵖ B} (h : CategoryTheory.sheafify J (P.comp F) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.toSheafify J P) F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyComposeIso J F P).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J (P.comp F)) h

theorem CategoryTheory.GrothendieckTopology.sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_3} {E : Type u_4} [CategoryTheory.Category.{max v u, u_3} D] [CategoryTheory.Category.{max v u, u_4} E] (F : CategoryTheory.Functor D E) [∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] [CategoryTheory.ConcreteCategory D] [CategoryTheory.ConcreteCategory E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget E)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget E)] [(CategoryTheory.forget D).ReflectsIsomorphisms] [(CategoryTheory.forget E).ReflectsIsomorphisms] (P : CategoryTheory.Functor Cᵒᵖ D) : (CategoryTheory.sheafToPresheaf J E).map ((CategoryTheory.sheafComposeNatTrans J F (CategoryTheory.plusPlusAdjunction J D) (CategoryTheory.plusPlusAdjunction J E)).app P) = (J.sheafifyCompIso F P).inv

instance CategoryTheory.GrothendieckTopology.instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_3} {E : Type u_4} [CategoryTheory.Category.{max v u, u_3} D] [CategoryTheory.Category.{max v u, u_4} E] (F : CategoryTheory.Functor D E) [∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] [CategoryTheory.ConcreteCategory D] [CategoryTheory.ConcreteCategory E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget E)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget E)] [(CategoryTheory.forget D).ReflectsIsomorphisms] [(CategoryTheory.forget E).ReflectsIsomorphisms] (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.IsIso ((CategoryTheory.sheafComposeNatTrans J F (CategoryTheory.plusPlusAdjunction J D) (CategoryTheory.plusPlusAdjunction J E)).app P)

instance CategoryTheory.GrothendieckTopology.instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_3} {E : Type u_4} [CategoryTheory.Category.{max v u, u_3} D] [CategoryTheory.Category.{max v u, u_4} E] (F : CategoryTheory.Functor D E) [∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] [CategoryTheory.ConcreteCategory D] [CategoryTheory.ConcreteCategory E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget E)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget E)] [(CategoryTheory.forget D).ReflectsIsomorphisms] [(CategoryTheory.forget E).ReflectsIsomorphisms] : CategoryTheory.IsIso (CategoryTheory.sheafComposeNatTrans J F (CategoryTheory.plusPlusAdjunction J D) (CategoryTheory.plusPlusAdjunction J E))

instance CategoryTheory.GrothendieckTopology.instPreservesSheafification {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_3} {E : Type u_4} [CategoryTheory.Category.{max v u, u_3} D] [CategoryTheory.Category.{max v u, u_4} E] (F : CategoryTheory.Functor D E) [∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) D] [∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) E] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D), CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F] [CategoryTheory.ConcreteCategory D] [CategoryTheory.ConcreteCategory E] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget E)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget E)] [(CategoryTheory.forget D).ReflectsIsomorphisms] [(CategoryTheory.forget E).ReflectsIsomorphisms] : J.PreservesSheafification F