feat(category_theory/limits/presheaf): left adjoint if preserves colimits (#4896)

Author: b-mehta

src/category_theory/limits/presheaf.lean

@@ -308,4 +308,14 @@ def unique_extension_along_yoneda (L : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ) (hL : yo
   L ≅ extend_along_yoneda A :=
 nat_iso_of_nat_iso_on_representables _ _ (hL ≪≫ (is_extension_along_yoneda _).symm)
 
+/--
+If `L` preserves colimits and `ℰ` has them, then it is a left adjoint. Note this is a (partial)
+converse to `left_adjoint_preserves_colimits`.
+-/
+def is_left_adjoint_of_preserves_colimits (L : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ) [preserves_colimits L] :
+  is_left_adjoint L :=
+{ right := restricted_yoneda (yoneda ⋙ L),
+  adj := (yoneda_adjunction _).of_nat_iso_left
+              (unique_extension_along_yoneda _ L (iso.refl _)).symm }
+
 end category_theory