feat(category_theory/limits): equivalence creates colimits (#4923)

Dualises and tidy proofs already there

src/category_theory/adjunction/limits.lean

@@ -77,6 +77,25 @@ omit adj
 instance is_equivalence_preserves_colimits (E : C ⥤ D) [is_equivalence E] : preserves_colimits E :=
 left_adjoint_preserves_colimits E.adjunction
 
+@[priority 100] -- see Note [lower instance priority]
+instance is_equivalence_reflects_colimits (E : D ⥤ C) [is_equivalence E] : reflects_colimits E :=
+{ reflects_colimits_of_shape := λ J 𝒥, by exactI
+  { reflects_colimit := λ K,
+    { reflects := λ c t,
+      begin
+        have l := (is_colimit_of_preserves E.inv t).map_cocone_equiv E.fun_inv_id,
+        refine (((is_colimit.precompose_inv_equiv K.right_unitor _).symm) l).of_iso_colimit _,
+        tidy,
+      end } } }
+
+@[priority 100] -- see Note [lower instance priority]
+instance is_equivalence_creates_colimits (H : D ⥤ C) [is_equivalence H] : creates_colimits H :=
+{ creates_colimits_of_shape := λ J 𝒥, by exactI
+  { creates_colimit := λ F,
+    { lifts := λ c t,
+      { lifted_cocone := H.map_cocone_inv c,
+        valid_lift := H.map_cocone_map_cocone_inv c } } } }
+
 -- verify the preserve_colimits instance works as expected:
 example (E : C ⥤ D) [is_equivalence E]
   (c : cocone K) (h : is_colimit c) : is_colimit (E.map_cocone c) :=
@@ -159,12 +178,9 @@ instance is_equivalence_reflects_limits (E : D ⥤ C) [is_equivalence E] : refle
   { reflects_limit := λ K,
     { reflects := λ c t,
       begin
-        have l: is_limit (E.inv.map_cone (E.map_cone c)) := preserves_limit.preserves t,
-        convert is_limit.map_cone_equiv E.fun_inv_id l,
-        { rw functor.comp_id },
-        { cases c,
-          cases c_π,
-          congr; rw functor.comp_id }
+        have := (is_limit_of_preserves E.inv t).map_cone_equiv E.fun_inv_id,
+        refine (((is_limit.postcompose_hom_equiv K.left_unitor _).symm) this).of_iso_limit _,
+        tidy,
       end } } }
 
 @[priority 100] -- see Note [lower instance priority]

src/category_theory/limits/limits.lean

@@ -389,22 +389,10 @@ If `F` and `G` are naturally isomorphic, then `F.map_cone c` being a limit impli
 -/
 def map_cone_equiv {D : Type u'} [category.{v} D] {K : J ⥤ C} {F G : C ⥤ D} (h : F ≅ G) {c : cone K}
   (t : is_limit (F.map_cone c)) : is_limit (G.map_cone c) :=
-{ lift := λ s, t.map s (iso_whisker_left K h).inv ≫ h.hom.app c.X,
-  fac' := λ s j,
-  begin
-    erw [assoc, ← h.hom.naturality (c.π.app j), t.map_π_assoc s (iso_whisker_left K h).inv j],
-    dsimp,
-    simp,
-  end,
-  uniq' := λ s m J,
-  begin
-    rw ← cancel_mono (h.inv.app c.X),
-    apply t.hom_ext,
-    intro j,
-    rw [assoc, assoc, assoc, h.hom_inv_id_app_assoc],
-    erw [← h.inv.naturality (c.π.app j), reassoc_of (J j)],
-    apply (t.map_π s (iso_whisker_left K h).inv j).symm,
-  end }
+begin
+  apply postcompose_inv_equiv (iso_whisker_left K h : _) (G.map_cone c) _,
+  apply t.of_iso_limit (postcompose_whisker_left_map_cone h.symm c).symm,
+end
 
 /--
 A cone is a limit cone exactly if
@@ -809,6 +797,17 @@ def of_faithful {t : cocone F} {D : Type u'} [category.{v} D] (G : C ⥤ D) [fai
     apply G.map_comp
   end }
 
+/--
+If `F` and `G` are naturally isomorphic, then `F.map_cone c` being a colimit implies
+`G.map_cone c` is also a colimit.
+-/
+def map_cocone_equiv {D : Type u'} [category.{v} D] {K : J ⥤ C} {F G : C ⥤ D} (h : F ≅ G)
+  {c : cocone K} (t : is_colimit (F.map_cocone c)) : is_colimit (G.map_cocone c) :=
+begin
+  apply is_colimit.of_iso_colimit _ (precompose_whisker_left_map_cocone h c),
+  apply (precompose_inv_equiv (iso_whisker_left K h : _) _).symm t,
+end
+
 /--
 A cocone is a colimit cocone exactly if
 there is a unique cocone morphism from any other cocone.