feat(category_theory/limits): dualise a limits result (#2940)

Add the dual of `is_limit.of_cone_equiv`.

Co-authored-by: Scott Morrison <scott@tqft.net>

Author: b-mehta

src/category_theory/adjunction/basic.lean

@@ -41,6 +41,15 @@ is_right_adjoint.left R
 def right_adjoint (L : C ⥤ D) [is_left_adjoint L] : D ⥤ C :=
 is_left_adjoint.right L
 
+/-- The adjunction associated to a functor known to be a left adjoint. -/
+def adjunction.of_left_adjoint (left : C ⥤ D) [is_left_adjoint left] :
+  adjunction left (right_adjoint left) :=
+is_left_adjoint.adj
+/-- The adjunction associated to a functor known to be a right adjoint. -/
+def adjunction.of_right_adjoint (right : C ⥤ D) [is_right_adjoint right] :
+  adjunction (left_adjoint right) right :=
+is_right_adjoint.adj
+
 namespace adjunction
 
 restate_axiom hom_equiv_unit'

src/category_theory/limits/cones.lean

@@ -257,12 +257,12 @@ by { fapply nat_iso.of_components, { intro s, fapply ext, refl, obviously }, obv
 def precompose_id : precompose (𝟙 F) ≅ 𝟭 (cocone F) :=
 by { fapply nat_iso.of_components, { intro s, fapply ext, refl, obviously }, obviously }
 
+@[simps]
 def precompose_equivalence {G : J ⥤ C} (α : G ≅ F) : cocone F ≌ cocone G :=
-begin
-  refine equivalence.mk (precompose α.hom) (precompose α.inv) _ _,
-  { symmetry, refine (precompose_comp _ _).symm.trans _, rw [iso.inv_hom_id], exact precompose_id },
-  { refine (precompose_comp _ _).symm.trans _, rw [iso.hom_inv_id], exact precompose_id }
-end
+{ functor := precompose α.hom,
+  inverse := precompose α.inv,
+  unit_iso := nat_iso.of_components (λ s, cocones.ext (iso.refl _) (by tidy)) (by tidy),
+  counit_iso := nat_iso.of_components (λ s, cocones.ext (iso.refl _) (by tidy)) (by tidy) }
 
 section
 variable (F)

src/category_theory/limits/limits.lean

@@ -174,16 +174,15 @@ def iso_unique_cone_morphism {t : cone F} :
   { lift := λ s, (h s).default.hom,
     uniq' := λ s f w, congr_arg cone_morphism.hom ((h s).uniq ⟨f, w⟩) } }
 
--- TODO: this should actually hold for an adjunction between cone F and cone G, not just for
--- equivalences
 /--
 Given two functors which have equivalent categories of cones, we can transport a limiting cone across
 the equivalence.
 -/
-def of_cone_equiv {D : Type u'} [category.{v} D] {G : K ⥤ D} (h : cone F ≌ cone G) {c : cone G} (t : is_limit c) :
-  is_limit (h.inverse.obj c) :=
+def of_cone_equiv {D : Type u'} [category.{v} D] {G : K ⥤ D}
+  (h : cone G ⥤ cone F) [is_right_adjoint h] {c : cone G} (t : is_limit c) :
+  is_limit (h.obj c) :=
 mk_cone_morphism
-  (λ s, h.to_adjunction.hom_equiv s c (t.lift_cone_morphism _))
+  (λ s, (adjunction.of_right_adjoint h).hom_equiv s c (t.lift_cone_morphism _))
   (λ s m, (adjunction.eq_hom_equiv_apply _ _ _).2 t.uniq_cone_morphism )
 
 namespace of_nat_iso
@@ -396,6 +395,17 @@ def iso_unique_cocone_morphism {t : cocone F} :
   { desc := λ s, (h s).default.hom,
     uniq' := λ s f w, congr_arg cocone_morphism.hom ((h s).uniq ⟨f, w⟩) } }
 
+/--
+Given two functors which have equivalent categories of cocones, we can transport a limiting cocone
+across the equivalence.
+-/
+def of_cocone_equiv {D : Type u'} [category.{v} D] {G : K ⥤ D}
+  (h : cocone G ⥤ cocone F) [is_left_adjoint h] {c : cocone G} (t : is_colimit c) :
+  is_colimit (h.obj c) :=
+mk_cocone_morphism
+  (λ s, ((adjunction.of_left_adjoint h).hom_equiv c s).symm (t.desc_cocone_morphism _))
+  (λ s m, (adjunction.hom_equiv_apply_eq _ _ _).1 t.uniq_cocone_morphism)
+
 namespace of_nat_iso
 variables {X : C} (h : coyoneda.obj (op X) ≅ F.cocones)
 

src/category_theory/limits/over.lean

@@ -167,7 +167,8 @@ def has_over_limit_discrete_of_wide_pullback_limit {B : C} {J : Type v} (F : dis
   [has_limit (wide_pullback_diagram_of_diagram_over B F)] :
   has_limit F :=
 { cone := _,
-  is_limit := is_limit.of_cone_equiv (cones_equiv B F).symm (limit.is_limit (wide_pullback_diagram_of_diagram_over B F)) }
+  is_limit := is_limit.of_cone_equiv
+    (cones_equiv B F).functor (limit.is_limit (wide_pullback_diagram_of_diagram_over B F)) }
 
 /-- Given a wide pullback in `C`, construct a product in `C/B`. -/
 def over_product_of_wide_pullback {J : Type v} [has_limits_of_shape.{v} (wide_pullback_shape J) C] {B : C} :

src/category_theory/limits/preserves.lean

@@ -129,9 +129,10 @@ def preserves_limit_of_iso {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K
   preserves_limit K₂ F :=
 { preserves := λ c t,
   begin
-    have t' := is_limit.of_cone_equiv (cones.postcompose_equivalence h) t,
+    have t' := is_limit.of_cone_equiv (cones.postcompose_equivalence h).inverse t,
     let hF := iso_whisker_right h F,
-    have := is_limit.of_cone_equiv (cones.postcompose_equivalence hF).symm (preserves_limit.preserves t'),
+    have := is_limit.of_cone_equiv (cones.postcompose_equivalence hF).functor
+              (preserves_limit.preserves t'),
     apply is_limit.of_iso_limit this,
     refine cones.ext (iso.refl _) (λ j, _),
     dsimp,
@@ -145,6 +146,22 @@ def preserves_colimit_of_preserves_colimit_cocone {F : C ⥤ D} {t : cocone K}
   (h : is_colimit t) (hF : is_colimit (F.map_cocone t)) : preserves_colimit K F :=
 ⟨λ t' h', is_colimit.of_iso_colimit hF (functor.map_iso _ (is_colimit.unique_up_to_iso h h'))⟩
 
+/-- Transfer preservation of colimits along a natural isomorphism in the shape. -/
+def preserves_colimit_of_iso {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [preserves_colimit K₁ F] :
+  preserves_colimit K₂ F :=
+{ preserves := λ c t,
+  begin
+    have t' := is_colimit.of_cocone_equiv (cocones.precompose_equivalence h).functor t,
+    let hF := iso_whisker_right h F,
+    have := is_colimit.of_cocone_equiv (cocones.precompose_equivalence hF).inverse
+              (preserves_colimit.preserves t'),
+    apply is_colimit.of_iso_colimit this,
+    refine cocones.ext (iso.refl _) (λ j, _),
+    dsimp,
+    rw [← F.map_comp],
+    simp,
+  end }
+
 /-
 A functor F : C → D reflects limits if whenever the image of a cone
 under F is a limit cone in D, the cone was already a limit cone in C.