Preservation of colimits and reflective adjunctions

Let adj : F ⊣ G be an adjunction with G : D ⥤ C full and faithful. We show that if colimits of shape J exist in C, then a functor H : D ⥤ E preserves colimits of shape J iff F ⋙ H does.

In particular, a functor from a category of sheaves preserves colimits iff it does so after precomposition with the sheafification functor.

theorem CategoryTheory.Adjunction.preservesColimitsOfShape_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {E : Type u₃} [Category.{v₃, u₃} E] (H : Functor D E) (J : Type u) [Category.{v, u} J] [Limits.HasColimitsOfShape J C] [G.Full] [G.Faithful] : Limits.PreservesColimitsOfShape J H ↔ Limits.PreservesColimitsOfShape J (F.comp H)

theorem CategoryTheory.Adjunction.preservesColimitsOfSize_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) {E : Type u₃} [Category.{v₃, u₃} E] (H : Functor D E) [Limits.HasColimitsOfSize.{v, u, v₁, u₁} C] [G.Full] [G.Faithful] : Limits.PreservesColimitsOfSize.{v, u, v₂, v₃, u₂, u₃} H ↔ Limits.PreservesColimitsOfSize.{v, u, v₁, v₃, u₁, u₃} (F.comp H)