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} [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) : 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 ((whiskeringRight Cᵒᵖ A B).obj F)

theorem CategoryTheory.GrothendieckTopology.W_of_preservesSheafification {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) [J.PreservesSheafification F] {P₁ P₂ : Functor Cᵒᵖ A} (f : P₁ ⟶ P₂) (hf : J.W f) : J.W (whiskerRight f F)

theorem CategoryTheory.GrothendieckTopology.W_isInvertedBy_whiskeringRight_presheafToSheaf {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) [J.PreservesSheafification F] [HasWeakSheafify J B] : J.W.IsInvertedBy (((whiskeringRight Cᵒᵖ A B).obj F).comp (presheafToSheaf J B))

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

• 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} [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] [HasWeakSheafify J A] : ((whiskeringRight Cᵒᵖ A B).obj F).comp (presheafToSheaf J B) ⟶ (presheafToSheaf J A).comp (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} [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] [HasWeakSheafify J A] (X : Functor Cᵒᵖ A) : (toPresheafToSheafCompComposeAndSheafify J F).app X = (presheafToSheaf J B).map (whiskerRight (toSheafify J X) F)

instance CategoryTheory.instIsIsoFunctorOppositeSheafToPresheafToSheafCompComposeAndSheafify {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] [HasWeakSheafify J A] [J.PreservesSheafification F] : IsIso (toPresheafToSheafCompComposeAndSheafify J F)

noncomputable def CategoryTheory.presheafToSheafCompComposeAndSheafifyIso {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] [HasWeakSheafify J A] [J.PreservesSheafification F] : (presheafToSheaf J A).comp (Sheaf.composeAndSheafify J F) ≅ ((whiskeringRight Cᵒᵖ A B).obj F).comp (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} [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] [HasWeakSheafify J A] [J.PreservesSheafification F] (X : Functor Cᵒᵖ A) : (presheafToSheafCompComposeAndSheafifyIso J F).inv.app X = (presheafToSheaf J B).map (whiskerRight (toSheafify J X) F)

noncomputable instance CategoryTheory.instLiftingFunctorOppositeSheafPresheafToSheafWCompObjWhiskeringRightComposeAndSheafify {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] [HasWeakSheafify J A] [J.PreservesSheafification F] : Localization.Lifting (presheafToSheaf J A) J.W (((whiskeringRight Cᵒᵖ A B).obj F).comp (presheafToSheaf J B)) (Sheaf.composeAndSheafify J F)

Equations

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

theorem CategoryTheory.GrothendieckTopology.preservesSheafification_iff_of_adjunctions {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [Category.{u_4, u_1} A] [Category.{u_3, 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.PreservesSheafification F ↔ ∀ (P : Functor Cᵒᵖ A), IsIso (G₂.map (whiskerRight (adj₁.unit.app P) F))

def CategoryTheory.sheafComposeNatTrans {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] : ((whiskeringRight Cᵒᵖ A B).obj F).comp G₂ ⟶ G₁.comp (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} [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

theorem CategoryTheory.GrothendieckTopology.preservesSheafification_iff_of_adjunctions_of_hasSheafCompose {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 ↔ IsIso (sheafComposeNatTrans J F adj₁ adj₂)

instance CategoryTheory.instIsIsoFunctorOppositeSheafSheafComposeNatTrans {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] : IsIso (sheafComposeNatTrans J F adj₁ adj₂)

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] : ((whiskeringRight Cᵒᵖ A B).obj F).comp G₂ ≅ G₁.comp (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} [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 A] [HasWeakSheafify J B] [J.HasSheafCompose F] [J.PreservesSheafification F] (P : Functor Cᵒᵖ A) : sheafify J (P.comp F) ≅ (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} [Category.{v, u} C] (J : GrothendieckTopology C) {A : Type u_1} {B : Type u_2} [Category.{u_4, u_1} A] [Category.{u_3, u_2} B] (F : Functor A B) [HasWeakSheafify J A] [HasWeakSheafify J B] [J.HasSheafCompose F] [J.PreservesSheafification F] (P : Functor Cᵒᵖ A) : CategoryStruct.comp (toSheafify J (P.comp F)) (sheafifyComposeIso J F P).hom = whiskerRight (toSheafify J P) F

@[simp]

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

@[simp]

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

@[simp]

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

theorem CategoryTheory.GrothendieckTopology.sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type u_3} {E : Type u_4} [Category.{max v u, u_3} D] [Category.{max v u, u_4} E] (F : Functor D E) [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) D] [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) E] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] {FD : D → D → Type u_5} {CD : D → Type (max v u)} {FE : E → E → Type u_6} {CE : E → Type (max v u)} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [(X Y : E) → FunLike (FE X Y) (CE X) (CE Y)] [instCCD : ConcreteCategory D FD] [instCCE : ConcreteCategory E FE] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget E)] [Limits.PreservesLimits (forget D)] [Limits.PreservesLimits (forget E)] [(forget D).ReflectsIsomorphisms] [(forget E).ReflectsIsomorphisms] (P : Functor Cᵒᵖ D) : (sheafToPresheaf J E).map ((sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)).app P) = (J.sheafifyCompIso F P).inv

instance CategoryTheory.GrothendieckTopology.instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type u_3} {E : Type u_4} [Category.{max v u, u_3} D] [Category.{max v u, u_4} E] (F : Functor D E) [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) D] [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) E] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] {FD : D → D → Type u_5} {CD : D → Type (max v u)} {FE : E → E → Type u_6} {CE : E → Type (max v u)} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [(X Y : E) → FunLike (FE X Y) (CE X) (CE Y)] [instCCD : ConcreteCategory D FD] [instCCE : ConcreteCategory E FE] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget E)] [Limits.PreservesLimits (forget D)] [Limits.PreservesLimits (forget E)] [(forget D).ReflectsIsomorphisms] [(forget E).ReflectsIsomorphisms] (P : Functor Cᵒᵖ D) : IsIso ((sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)).app P)

instance CategoryTheory.GrothendieckTopology.instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type u_3} {E : Type u_4} [Category.{max v u, u_3} D] [Category.{max v u, u_4} E] (F : Functor D E) [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) D] [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) E] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] {FD : D → D → Type u_5} {CD : D → Type (max v u)} {FE : E → E → Type u_6} {CE : E → Type (max v u)} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [(X Y : E) → FunLike (FE X Y) (CE X) (CE Y)] [instCCD : ConcreteCategory D FD] [instCCE : ConcreteCategory E FE] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget E)] [Limits.PreservesLimits (forget D)] [Limits.PreservesLimits (forget E)] [(forget D).ReflectsIsomorphisms] [(forget E).ReflectsIsomorphisms] : IsIso (sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E))

instance CategoryTheory.GrothendieckTopology.instPreservesSheafification {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type u_3} {E : Type u_4} [Category.{max v u, u_3} D] [Category.{max v u, u_4} E] (F : Functor D E) [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) D] [∀ (J : Limits.MulticospanShape), Limits.HasLimitsOfShape (Limits.WalkingMulticospan J) E] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] [∀ (X : C) (W : J.Cover X) (P : Functor Cᵒᵖ D), Limits.PreservesLimit (W.index P).multicospan F] {FD : D → D → Type u_5} {CD : D → Type (max v u)} {FE : E → E → Type u_6} {CE : E → Type (max v u)} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [(X Y : E) → FunLike (FE X Y) (CE X) (CE Y)] [instCCD : ConcreteCategory D FD] [instCCE : ConcreteCategory E FE] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget E)] [Limits.PreservesLimits (forget D)] [Limits.PreservesLimits (forget E)] [(forget D).ReflectsIsomorphisms] [(forget E).ReflectsIsomorphisms] : J.PreservesSheafification F