feat(category_theory/monad): monadic functor really creates limits (#4931)

Show that a monadic functor `creates_limits`, and a partial result for colimits.

Author: b-mehta

src/category_theory/monad/limits.lean

@@ -259,16 +259,36 @@ instance comp_comparison_has_limit
 monad.has_limit_of_comp_forget_has_limit (F ⋙ monad.comparison R)
 
 /-- Any monadic functor creates limits. -/
-lemma monadic_creates_limits (F : J ⥤ D) (R : D ⥤ C) [monadic_right_adjoint R] [has_limit (F ⋙ R)] :
-  has_limit F :=
-adjunction.has_limit_of_comp_equivalence _ (monad.comparison R)
+def monadic_creates_limits (R : D ⥤ C) [monadic_right_adjoint R] :
+  creates_limits R :=
+creates_limits_of_nat_iso (monad.comparison_forget R)
+
+/-- A monadic functor creates any colimits of shapes it preserves. -/
+def monadic_creates_colimits_of_shape_of_preserves_colimits_of_shape (R : D ⥤ C)
+  [monadic_right_adjoint R] [preserves_colimits_of_shape J R] : creates_colimits_of_shape J R :=
+begin
+  have : preserves_colimits_of_shape J (left_adjoint R ⋙ R),
+  { apply category_theory.limits.comp_preserves_colimits_of_shape _ _,
+    { haveI := adjunction.left_adjoint_preserves_colimits (adjunction.of_right_adjoint R),
+      apply_instance },
+    apply_instance },
+  resetI,
+  apply creates_colimits_of_shape_of_nat_iso (monad.comparison_forget R),
+  apply_instance,
+end
+
+/-- A monadic functor creates colimits if it preserves colimits. -/
+def monadic_creates_colimits_of_preserves_colimits (R : D ⥤ C) [monadic_right_adjoint R]
+  [preserves_colimits R] : creates_colimits R :=
+{ creates_colimits_of_shape := λ J 𝒥₁,
+    by exactI monadic_creates_colimits_of_shape_of_preserves_colimits_of_shape _ }
 
 section
 
-/-- If C has limits then any reflective subcategory has limits -/
+/-- If C has limits then any reflective subcategory has limits. -/
 lemma has_limits_of_reflective (R : D ⥤ C) [has_limits C] [reflective R] : has_limits D :=
-{ has_limits_of_shape := λ J 𝒥, by exactI
-  { has_limit := λ F, monadic_creates_limits F R } }
+{ has_limits_of_shape := λ J 𝒥, by have := monadic_creates_limits R; exactI
+  { has_limit := λ F, has_limit_of_created F R } }
 
 end
 end category_theory