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

A slight generalisation of a construction from before. Maybe this is the dual version you were talking about @jcommelin - if so my mistake! I think the advantage of doing it this way is that you definitionally get the old version but also the new version too.

Author: b-mehta

src/category_theory/equivalence.lean

@@ -271,16 +271,16 @@ by { dsimp [inv_fun_id_assoc], tidy }
 by { dsimp [inv_fun_id_assoc], tidy }
 
 /-- If `C` is equivalent to `D`, then `C ⥤ E` is equivalent to `D ⥤ E`. -/
-@[simps {rhs_md:=semireducible}]
+@[simps functor inverse unit_iso counit_iso {rhs_md:=semireducible}]
 def congr_left (e : C ≌ D) : (C ⥤ E) ≌ (D ⥤ E) :=
 equivalence.mk
   ((whiskering_left _ _ _).obj e.inverse)
   ((whiskering_left _ _ _).obj e.functor)
   (nat_iso.of_components (λ F, (e.fun_inv_id_assoc F).symm) (by tidy))
   (nat_iso.of_components (λ F, e.inv_fun_id_assoc F) (by tidy))
-  
+
 /-- If `C` is equivalent to `D`, then `E ⥤ C` is equivalent to `E ⥤ D`. -/
-@[simps {rhs_md:=semireducible}]
+@[simps functor inverse unit_iso counit_iso {rhs_md:=semireducible}]
 def congr_right (e : C ≌ D) : (E ⥤ C) ≌ (E ⥤ D) :=
 equivalence.mk
   ((whiskering_right _ _ _).obj e.functor)

src/category_theory/limits/presheaf.lean

@@ -309,13 +309,23 @@ def unique_extension_along_yoneda (L : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ) (hL : yo
 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`.
+If `L` preserves colimits and `ℰ` has them, then it is a left adjoint. This is a special case of
+`is_left_adjoint_of_preserves_colimits` used to prove that.
 -/
-def is_left_adjoint_of_preserves_colimits (L : (Cᵒᵖ ⥤ Type u₁) ⥤ ℰ) [preserves_colimits L] :
+def is_left_adjoint_of_preserves_colimits_aux (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 }
+            ((unique_extension_along_yoneda _ L (iso.refl _)).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 :=
+let e : (_ ⥤ Type u₁) ≌ (_ ⥤ Type u₁) := (op_op_equivalence C).congr_left,
+    t := is_left_adjoint_of_preserves_colimits_aux (e.functor ⋙ L : _)
+in by exactI adjunction.left_adjoint_of_nat_iso (e.inv_fun_id_assoc _)
 
 end category_theory