mathlib4 feat(CategoryTheory/Sites): functors which preserves sheafification

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.

If we also assume J.HasSheafCompose F (which says that the postcomposition with F induces a functor sheafCompose J F : Sheaf J A ⥤ Sheaf J B), then we obtain that the canonical map is an isomorphism sheafify J (P ⋙ F) ≅ sheafify J P ⋙ F.

We obtain PreservesSheafification J (forget D) when D is a concrete category satisfying suitable conditions.