feat(category_theory/limits): the isomorphism expressing preservation of chosen limits

src/category_theory/limits/limits.lean

@@ -70,6 +70,11 @@ def unique_up_to_iso {s t : cone F} (P : is_limit s) (Q : is_limit t) : s ≅ t
   hom_inv_id' := P.uniq_cone_morphism,
   inv_hom_id' := Q.uniq_cone_morphism }
 
+/-- Limits of `F` are unique up to isomorphism. -/
+-- We may later want to prove the coherence of these isomorphisms.
+def cone_point_unique_up_to_iso {s t : cone F} (P : is_limit s) (Q : is_limit t) : s.X ≅ t.X :=
+(cones.forget F).map_iso (unique_up_to_iso P Q)
+
 /-- Transport evidence that a cone is a limit cone across an isomorphism of cones. -/
 def of_iso_limit {r t : cone F} (P : is_limit r) (i : r ≅ t) : is_limit t :=
 is_limit.mk_cone_morphism
@@ -274,6 +279,11 @@ def unique_up_to_iso {s t : cocone F} (P : is_colimit s) (Q : is_colimit t) : s
   hom_inv_id' := P.uniq_cocone_morphism,
   inv_hom_id' := Q.uniq_cocone_morphism }
 
+/-- Colimits of `F` are unique up to isomorphism. -/
+-- We may later want to prove the coherence of these isomorphisms.
+def cone_point_unique_up_to_iso {s t : cocone F} (P : is_colimit s) (Q : is_colimit t) : s.X ≅ t.X :=
+(cocones.forget F).map_iso (unique_up_to_iso P Q)
+
 /-- Transport evidence that a cocone is a colimit cocone across an isomorphism of cocones. -/
 def of_iso_colimit {r t : cocone F} (P : is_colimit r) (i : r ≅ t) : is_colimit t :=
 is_colimit.mk_cocone_morphism

src/category_theory/limits/preserves.lean

@@ -49,6 +49,15 @@ class preserves_limit (K : J ⥤ C) (F : C ⥤ D) : Type (max u₁ u₂ v) :=
 class preserves_colimit (K : J ⥤ C) (F : C ⥤ D) : Type (max u₁ u₂ v) :=
 (preserves : Π {c : cocone K}, is_colimit c → is_colimit (F.map_cocone c))
 
+/-- A functor which preserves limits preserves chosen limits up to isomorphism. -/
+def preserves_limit_iso (K : J ⥤ C) [has_limit.{v} K] (F : C ⥤ D) [has_limit.{v} (K ⋙ F)] [preserves_limit K F] :
+  F.obj (limit K) ≅ limit (K ⋙ F) :=
+is_limit.cone_point_unique_up_to_iso (preserves_limit.preserves F (limit.is_limit K)) (limit.is_limit (K ⋙ F))
+/-- A functor which preserves colimits preserves chosen colimits up to isomorphism. -/
+def preserves_colimit_iso (K : J ⥤ C) [has_colimit.{v} K] (F : C ⥤ D) [has_colimit.{v} (K ⋙ F)] [preserves_colimit K F] :
+  F.obj (colimit K) ≅ colimit (K ⋙ F) :=
+is_colimit.cone_point_unique_up_to_iso (preserves_colimit.preserves F (colimit.is_colimit K)) (colimit.is_colimit (K ⋙ F))
+
 class preserves_limits_of_shape (J : Type v) [small_category J] (F : C ⥤ D) : Type (max u₁ u₂ v) :=
 (preserves_limit : Π {K : J ⥤ C}, preserves_limit K F)
 class preserves_colimits_of_shape (J : Type v) [small_category J] (F : C ⥤ D) : Type (max u₁ u₂ v) :=