feat(category_theory/limits): limit of point iso (#3188)

Prove a cone is a limit given that the canonical morphism from it to a limiting cone is an iso.

Author: b-mehta

src/algebra/category/Group/limits.lean

@@ -5,6 +5,7 @@ Authors: Scott Morrison
 -/
 import algebra.category.Group.basic
 import category_theory.limits.types
+import category_theory.limits.preserves
 import algebra.pi_instances
 
 /-!

src/category_theory/limits/creates.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
-import category_theory.reflect_isomorphisms
+import category_theory.limits.preserves
 
 open category_theory category_theory.limits
 

src/category_theory/limits/limits.lean

@@ -5,6 +5,7 @@ Authors: Reid Barton, Mario Carneiro, Scott Morrison, Floris van Doorn
 -/
 import category_theory.limits.cones
 import category_theory.adjunction.basic
+import category_theory.reflect_isomorphisms
 
 open category_theory category_theory.category category_theory.functor opposite
 
@@ -78,6 +79,19 @@ is_limit.mk_cone_morphism
   (λ s, P.lift_cone_morphism s ≫ i.hom)
   (λ s m, by rw ←i.comp_inv_eq; apply P.uniq_cone_morphism)
 
+/--
+If the canonical morphism from a cone point to a limiting cone point is an iso, then the
+first cone was limiting also.
+-/
+def of_point_iso {r t : cone F} (P : is_limit r) [i : is_iso (P.lift t)] : is_limit t :=
+of_iso_limit P
+begin
+  haveI : is_iso (P.lift_cone_morphism t).hom := i,
+  haveI : is_iso (P.lift_cone_morphism t) := cone_iso_of_hom_iso _,
+  symmetry,
+  apply as_iso (P.lift_cone_morphism t),
+end
+
 variables {t : cone F}
 
 lemma hom_lift (h : is_limit t) {W : C} (m : W ⟶ t.X) :
@@ -376,6 +390,18 @@ is_colimit.mk_cocone_morphism
   (λ s, i.inv ≫ P.desc_cocone_morphism s)
   (λ s m, by rw i.eq_inv_comp; apply P.uniq_cocone_morphism)
 
+/--
+If the canonical morphism to a cocone point from a colimiting cocone point is an iso, then the
+first cocone was colimiting also.
+-/
+def of_point_iso {r t : cocone F} (P : is_colimit r) [i : is_iso (P.desc t)] : is_colimit t :=
+of_iso_colimit P
+begin
+  haveI : is_iso (P.desc_cocone_morphism t).hom := i,
+  haveI : is_iso (P.desc_cocone_morphism t) := cocone_iso_of_hom_iso _,
+  apply as_iso (P.desc_cocone_morphism t),
+end
+
 variables {t : cocone F}
 
 lemma hom_desc (h : is_colimit t) {W : C} (m : t.X ⟶ W) :

src/category_theory/reflect_isomorphisms.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
-import category_theory.limits.preserves
+import category_theory.limits.cones
 
 open category_theory category_theory.limits
 

src/topology/category/Top/limits.lean

@@ -5,6 +5,7 @@ Authors: Patrick Massot, Scott Morrison, Mario Carneiro
 -/
 import topology.category.Top.basic
 import category_theory.limits.types
+import category_theory.limits.preserves
 
 open topological_space
 open category_theory