From 11368e1b50d2c8ebb40c43637feca1c7a53c94ea Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Sat, 7 Nov 2020 18:00:08 +0000 Subject: [PATCH] feat(category_theory/limits/preserves): transfer reflecting limits through nat iso (#4934) --- .../limits/preserves/basic.lean | 29 +++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/src/category_theory/limits/preserves/basic.lean b/src/category_theory/limits/preserves/basic.lean index 105a93a24023f..9350243deb85d 100644 --- a/src/category_theory/limits/preserves/basic.lean +++ b/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