In this file, we prove that sheafification is compatible with functors which preserve the correct limits and colimits.

noncomputable def CategoryTheory.GrothendieckTopology.sheafifyCompIso {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} 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 (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] [(X : C) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.Functor.comp (CategoryTheory.GrothendieckTopology.sheafify J P) F ≅ CategoryTheory.GrothendieckTopology.sheafify J (CategoryTheory.Functor.comp P F)

The isomorphism between the sheafification of P composed with F and the sheafification of P ⋙ F.

Use the lemmas whisker_right_to_sheafify_sheafify_comp_iso_hom, to_sheafify_comp_sheafify_comp_iso_inv and sheafify_comp_iso_inv_eq_sheafify_lift to reduce the components of this isomorphisms to a state that can be handled using the universal property of sheafification.

noncomputable def CategoryTheory.GrothendieckTopology.sheafificationWhiskerLeftIso {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} 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 (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] (P : CategoryTheory.Functor Cᵒᵖ D) [(F : CategoryTheory.Functor D E) → (X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] [(F : CategoryTheory.Functor D E) → (X : C) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] : (CategoryTheory.whiskeringLeft Cᵒᵖ D E).obj (CategoryTheory.GrothendieckTopology.sheafify J P) ≅ CategoryTheory.Functor.comp ((CategoryTheory.whiskeringLeft Cᵒᵖ D E).obj P) (CategoryTheory.GrothendieckTopology.sheafification J E)

The isomorphism between the sheafification of P composed with F and the sheafification of P ⋙ F, functorially in F.

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafificationWhiskerLeftIso_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} 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 (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] (P : CategoryTheory.Functor Cᵒᵖ D) (F : CategoryTheory.Functor D E) [(F : CategoryTheory.Functor D E) → (X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] [(F : CategoryTheory.Functor D E) → (X : C) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] : (CategoryTheory.GrothendieckTopology.sheafificationWhiskerLeftIso J P).hom.app F = (CategoryTheory.GrothendieckTopology.sheafifyCompIso J F P).hom

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafificationWhiskerLeftIso_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} 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 (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] (P : CategoryTheory.Functor Cᵒᵖ D) (F : CategoryTheory.Functor D E) [(F : CategoryTheory.Functor D E) → (X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] [(F : CategoryTheory.Functor D E) → (X : C) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] : (CategoryTheory.GrothendieckTopology.sheafificationWhiskerLeftIso J P).inv.app F = (CategoryTheory.GrothendieckTopology.sheafifyCompIso J F P).inv

noncomputable def CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} 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 (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] [(X : C) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] : CategoryTheory.Functor.comp (CategoryTheory.GrothendieckTopology.sheafification J D) ((CategoryTheory.whiskeringRight Cᵒᵖ D E).obj F) ≅ CategoryTheory.Functor.comp ((CategoryTheory.whiskeringRight Cᵒᵖ D E).obj F) (CategoryTheory.GrothendieckTopology.sheafification J E)

The isomorphism between the sheafification of P composed with F and the sheafification of P ⋙ F, functorially in P.

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} 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 (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] [(X : C) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] (P : CategoryTheory.Functor Cᵒᵖ D) : (CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso J F).hom.app P = (CategoryTheory.GrothendieckTopology.sheafifyCompIso J F P).hom

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} 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 (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] [(X : C) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] (P : CategoryTheory.Functor Cᵒᵖ D) : (CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso J F).inv.app P = (CategoryTheory.GrothendieckTopology.sheafifyCompIso J F P).inv

theorem CategoryTheory.GrothendieckTopology.whiskerRight_toSheafify_sheafifyCompIso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} 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 (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] [(X : C) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] (P : CategoryTheory.Functor Cᵒᵖ D) {Z : CategoryTheory.Functor Cᵒᵖ E} (h : CategoryTheory.GrothendieckTopology.sheafify J (CategoryTheory.Functor.comp P F) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.GrothendieckTopology.toSheafify J P) F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.sheafifyCompIso J F P).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.toSheafify J (CategoryTheory.Functor.comp P F)) h

@[simp]

theorem CategoryTheory.GrothendieckTopology.whiskerRight_toSheafify_sheafifyCompIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} 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 (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] [(X : C) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.GrothendieckTopology.toSheafify J P) F) (CategoryTheory.GrothendieckTopology.sheafifyCompIso J F P).hom = CategoryTheory.GrothendieckTopology.toSheafify J (CategoryTheory.Functor.comp P F)

theorem CategoryTheory.GrothendieckTopology.toSheafify_comp_sheafifyCompIso_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} 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 (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] [(X : C) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] (P : CategoryTheory.Functor Cᵒᵖ D) {Z : CategoryTheory.Functor Cᵒᵖ E} (h : CategoryTheory.Functor.comp (CategoryTheory.GrothendieckTopology.sheafify J P) F ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.toSheafify J (CategoryTheory.Functor.comp P F)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.sheafifyCompIso J F P).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.GrothendieckTopology.toSheafify J P) F) h

@[simp]

theorem CategoryTheory.GrothendieckTopology.toSheafify_comp_sheafifyCompIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} 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 (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] [(X : C) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.toSheafify J (CategoryTheory.Functor.comp P F)) (CategoryTheory.GrothendieckTopology.sheafifyCompIso J F P).inv = CategoryTheory.whiskerRight (CategoryTheory.GrothendieckTopology.toSheafify J P) F

@[simp]

theorem CategoryTheory.GrothendieckTopology.sheafifyCompIso_inv_eq_sheafifyLift {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w₁} [CategoryTheory.Category.{max v u, w₁} D] {E : Type w₂} [CategoryTheory.Category.{max v u, w₂} 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 (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ E] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ F] [(X : C) → (W : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index W P)) F] (P : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.ConcreteCategory D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] : (CategoryTheory.GrothendieckTopology.sheafifyCompIso J F P).inv = CategoryTheory.GrothendieckTopology.sheafifyLift J (CategoryTheory.whiskerRight (CategoryTheory.GrothendieckTopology.toSheafify J P) F) (_ : CategoryTheory.Presheaf.IsSheaf J (CategoryTheory.Functor.comp (CategoryTheory.GrothendieckTopology.sheafify J P) F))