feat(category_theory/limits/preserves): transfer reflecting limits th…

…rough nat iso (#4934)

src/category_theory/limits/preserves/basic.lean

@@ -346,6 +346,21 @@ def preserves_limit_of_reflects_of_preserves [preserves_limit K (F ⋙ G)]
   exact preserves_limit.preserves h
  end⟩
 
+/-- Transfer reflection of a limit along a natural isomorphism in the functor. -/
+def reflects_limit_of_nat_iso (K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [reflects_limit K F] :
+  reflects_limit K G :=
+{ reflects := λ c t, reflects_limit.reflects (is_limit.map_cone_equiv h.symm t) }
+
+/-- Transfer reflection of limits of shape along a natural isomorphism in the functor. -/
+def reflects_limits_of_shape_of_nat_iso {F G : C ⥤ D} (h : F ≅ G) [reflects_limits_of_shape J F] :
+  reflects_limits_of_shape J G :=
+{ reflects_limit := λ K, reflects_limit_of_nat_iso K h }
+
+/-- Transfer reflection of limits along a natural isomorphism in the functor. -/
+def reflects_limits_of_nat_iso {F G : C ⥤ D} (h : F ≅ G) [reflects_limits F] :
+  reflects_limits G :=
+{ reflects_limits_of_shape := λ J 𝒥₁, by exactI reflects_limits_of_shape_of_nat_iso h }
+
 /-- If `F ⋙ G` preserves colimits for `K`, and `G` reflects colimits for `K ⋙ F`,
 then `F` preserves colimits for `K`. -/
 def preserves_colimit_of_reflects_of_preserves [preserves_colimit K (F ⋙ G)]
@@ -357,6 +372,20 @@ def preserves_colimit_of_reflects_of_preserves [preserves_colimit K (F ⋙ G)]
   exact preserves_colimit.preserves h
  end⟩
 
+/-- Transfer reflection of a colimit along a natural isomorphism in the functor. -/
+def reflects_colimit_of_nat_iso (K : J ⥤ C) {F G : C ⥤ D} (h : F ≅ G) [reflects_colimit K F] :
+  reflects_colimit K G :=
+{ reflects := λ c t, reflects_colimit.reflects (is_colimit.map_cocone_equiv h.symm t) }
+
+/-- Transfer reflection of colimits of shape along a natural isomorphism in the functor. -/
+def reflects_colimits_of_shape_of_nat_iso {F G : C ⥤ D} (h : F ≅ G)
+  [reflects_colimits_of_shape J F] : reflects_colimits_of_shape J G :=
+{ reflects_colimit := λ K, reflects_colimit_of_nat_iso K h }
+
+/-- Transfer reflection of colimits along a natural isomorphism in the functor. -/
+def reflects_colimits_of_nat_iso {F G : C ⥤ D} (h : F ≅ G) [reflects_colimits F] :
+  reflects_colimits G :=
+{ reflects_colimits_of_shape := λ J 𝒥₁, by exactI reflects_colimits_of_shape_of_nat_iso h }
 
 end