chore(category_theory/limits/functor_category): shuffle limits in functor cats (#4124)

Give `is_limit` versions for statements about limits in the functor category, and write the `has_limit` versions in terms of those.
This also generalises the universes a little.
As usual, suggestions for better docstrings or better names appreciated!

Author: b-mehta

src/category_theory/limits/cones.lean

@@ -84,7 +84,7 @@ structure cone (F : J ⥤ C) :=
 (X : C)
 (π : (const J).obj X ⟶ F)
 
-@[simp] lemma cone.w {F : J ⥤ C} (c : cone F) {j j' : J} (f : j ⟶ j') :
+@[simp, reassoc] lemma cone.w {F : J ⥤ C} (c : cone F) {j j' : J} (f : j ⟶ j') :
   c.π.app j ≫ F.map f = c.π.app j' :=
 by { rw ← (c.π.naturality f), apply id_comp }
 
@@ -99,7 +99,7 @@ structure cocone (F : J ⥤ C) :=
 (X : C)
 (ι : F ⟶ (const J).obj X)
 
-@[simp] lemma cocone.w {F : J ⥤ C} (c : cocone F) {j j' : J} (f : j ⟶ j') :
+@[simp, reassoc] lemma cocone.w {F : J ⥤ C} (c : cocone F) {j j' : J} (f : j ⟶ j') :
   F.map f ≫ c.ι.app j' = c.ι.app j :=
 by { rw (c.ι.naturality f), apply comp_id }
 

src/category_theory/limits/functor_category.lean

@@ -7,87 +7,124 @@ import category_theory.limits.preserves.basic
 
 open category_theory category_theory.category
 
-noncomputable theory
-
 namespace category_theory.limits
 
-universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
+universes v v₂ u -- declare the `v`'s first; see `category_theory.category` for an explanation
 
 variables {C : Type u} [category.{v} C]
 
-variables {J K : Type v} [small_category J] [small_category K]
-
-@[simp] lemma cone.functor_w {F : J ⥤ (K ⥤ C)} (c : cone F) {j j' : J} (f : j ⟶ j') (k : K) :
-  (c.π.app j).app k ≫ (F.map f).app k = (c.π.app j').app k :=
-by convert ←nat_trans.congr_app (c.π.naturality f).symm k; apply id_comp
+variables {J K : Type v} [small_category J] [category.{v₂} K]
 
-@[simp] lemma cocone.functor_w {F : J ⥤ (K ⥤ C)} (c : cocone F) {j j' : J} (f : j ⟶ j') (k : K) :
-  (F.map f).app k ≫ (c.ι.app j').app k = (c.ι.app j).app k :=
-by convert ←nat_trans.congr_app (c.ι.naturality f) k; apply comp_id
-
-@[simps] def functor_category_limit_cone [has_limits_of_shape J C] (F : J ⥤ K ⥤ C) :
+/--
+The evaluation functors jointly reflect limits: that is, to show a cone is a limit of `F`
+it suffices to show that each evaluation cone is a limit. In other words, to prove a cone is
+limiting you can show it's pointwise limiting.
+-/
+def evaluation_jointly_reflects_limits {F : J ⥤ K ⥤ C} (c : cone F)
+  (t : Π (k : K), is_limit (((evaluation K C).obj k).map_cone c)) : is_limit c :=
+{ lift := λ s,
+  { app := λ k, (t k).lift ⟨s.X.obj k, whisker_right s.π ((evaluation K C).obj k)⟩,
+    naturality' := λ X Y f, (t Y).hom_ext $ λ j,
+    begin
+      rw [assoc, (t Y).fac _ j],
+      simpa using ((t X).fac_assoc ⟨s.X.obj X, whisker_right s.π ((evaluation K C).obj X)⟩ j _).symm,
+    end },
+  fac' := λ s j, nat_trans.ext _ _ $ funext $ λ k, (t k).fac _ j,
+  uniq' := λ s m w, nat_trans.ext _ _ $ funext $ λ x, (t x).hom_ext $ λ j,
+      (congr_app (w j) x).trans
+        ((t x).fac ⟨s.X.obj _, whisker_right s.π ((evaluation K C).obj _)⟩ j).symm }
+
+/--
+Given a functor `F` and a collection of limit cones for each diagram `X ↦ F X k`, we can stitch
+them together to give a cone for the diagram `F`.
+`combined_is_limit` shows that the new cone is limiting, and `eval_combined` shows it is
+(essentially) made up of the original cones.
+-/
+@[simps] def combine_cones (F : J ⥤ K ⥤ C) (c : Π (k : K), limit_cone (F.flip.obj k)) :
   cone F :=
-{ X := F.flip ⋙ lim,
+{ X :=
+  { obj := λ k, (c k).cone.X,
+    map := λ k₁ k₂ f, (c k₂).is_limit.lift ⟨_, (c k₁).cone.π ≫ F.flip.map f⟩,
+    map_id' := λ k, (c k).is_limit.hom_ext (λ j, by { dsimp, simp }),
+    map_comp' := λ k₁ k₂ k₃ f₁ f₂, (c k₃).is_limit.hom_ext (λ j, by simp) },
   π :=
-  { app := λ j,
-    { app := λ k, limit.π (F.flip.obj k) j },
-      naturality' := λ j j' f,
-        by ext k; convert (limit.w (F.flip.obj k) _).symm using 1; apply id_comp } }
+  { app := λ j, { app := λ k, (c k).cone.π.app j },
+    naturality' := λ j₁ j₂ g, nat_trans.ext _ _ $ funext $ λ k, (c k).cone.π.naturality g } }
+
+/-- The stitched together cones each project down to the original given cones (up to iso). -/
+def evaluate_combined_cones (F : J ⥤ K ⥤ C) (c : Π (k : K), limit_cone (F.flip.obj k)) (k : K) :
+  ((evaluation K C).obj k).map_cone (combine_cones F c) ≅ (c k).cone :=
+cones.ext (iso.refl _) (by tidy)
 
-@[simps] def functor_category_colimit_cocone [has_colimits_of_shape J C] (F : J ⥤ K ⥤ C) :
+/-- Stitching together limiting cones gives a limiting cone. -/
+def combined_is_limit (F : J ⥤ K ⥤ C) (c : Π (k : K), limit_cone (F.flip.obj k)) :
+  is_limit (combine_cones F c) :=
+evaluation_jointly_reflects_limits _
+  (λ k, (c k).is_limit.of_iso_limit (evaluate_combined_cones F c k).symm)
+
+/--
+The evaluation functors jointly reflect colimits: that is, to show a cocone is a colimit of `F`
+it suffices to show that each evaluation cocone is a colimit. In other words, to prove a cocone is
+colimiting you can show it's pointwise colimiting.
+-/
+def evaluation_jointly_reflects_colimits {F : J ⥤ K ⥤ C} (c : cocone F)
+  (t : Π (k : K), is_colimit (((evaluation K C).obj k).map_cocone c)) : is_colimit c :=
+{ desc := λ s,
+  { app := λ k, (t k).desc ⟨s.X.obj k, whisker_right s.ι ((evaluation K C).obj k)⟩,
+    naturality' := λ X Y f, (t X).hom_ext $ λ j,
+    begin
+      rw [(t X).fac_assoc _ j],
+      erw ← (c.ι.app j).naturality_assoc f,
+      erw (t Y).fac ⟨s.X.obj _, whisker_right s.ι _⟩ j,
+      dsimp,
+      simp,
+    end },
+  fac' := λ s j, nat_trans.ext _ _ $ funext $ λ k, (t k).fac _ j,
+  uniq' := λ s m w, nat_trans.ext _ _ $ funext $ λ x, (t x).hom_ext $ λ j,
+      (congr_app (w j) x).trans
+        ((t x).fac ⟨s.X.obj _, whisker_right s.ι ((evaluation K C).obj _)⟩ j).symm }
+
+/--
+Given a functor `F` and a collection of colimit cocones for each diagram `X ↦ F X k`, we can stitch
+them together to give a cocone for the diagram `F`.
+`combined_is_colimit` shows that the new cocone is colimiting, and `eval_combined` shows it is
+(essentially) made up of the original cocones.
+-/
+@[simps] def combine_cocones (F : J ⥤ K ⥤ C) (c : Π (k : K), colimit_cocone (F.flip.obj k)) :
   cocone F :=
-{ X := F.flip ⋙ colim,
+{ X :=
+  { obj := λ k, (c k).cocone.X,
+    map := λ k₁ k₂ f, (c k₁).is_colimit.desc ⟨_, F.flip.map f ≫ (c k₂).cocone.ι⟩,
+    map_id' := λ k, (c k).is_colimit.hom_ext (λ j, by { dsimp, simp }),
+    map_comp' := λ k₁ k₂ k₃ f₁ f₂, (c k₁).is_colimit.hom_ext (λ j, by simp) },
   ι :=
-  { app := λ j,
-    { app := λ k, colimit.ι (F.flip.obj k) j },
-      naturality' := λ j j' f,
-        by ext k; convert (colimit.w (F.flip.obj k) _) using 1; apply comp_id } }
-
-@[simp] def evaluate_functor_category_limit_cone
-  [has_limits_of_shape J C] (F : J ⥤ K ⥤ C) (k : K) :
-  ((evaluation K C).obj k).map_cone (functor_category_limit_cone F) ≅
-    limit.cone (F.flip.obj k) :=
-cones.ext (iso.refl _) (by tidy)
+  { app := λ j, { app := λ k, (c k).cocone.ι.app j },
+    naturality' := λ j₁ j₂ g, nat_trans.ext _ _ $ funext $ λ k, (c k).cocone.ι.naturality g } }
 
-@[simp] def evaluate_functor_category_colimit_cocone
-  [has_colimits_of_shape J C] (F : J ⥤ K ⥤ C) (k : K) :
-  ((evaluation K C).obj k).map_cocone (functor_category_colimit_cocone F) ≅
-    colimit.cocone (F.flip.obj k) :=
+/-- The stitched together cocones each project down to the original given cocones (up to iso). -/
+def evaluate_combined_cocones (F : J ⥤ K ⥤ C) (c : Π (k : K), colimit_cocone (F.flip.obj k)) (k : K) :
+  ((evaluation K C).obj k).map_cocone (combine_cocones F c) ≅ (c k).cocone :=
 cocones.ext (iso.refl _) (by tidy)
 
-def functor_category_is_limit_cone [has_limits_of_shape J C] (F : J ⥤ K ⥤ C) :
-  is_limit (functor_category_limit_cone F) :=
-{ lift := λ s,
-  { app := λ k, limit.lift (F.flip.obj k) (((evaluation K C).obj k).map_cone s) },
-  uniq' := λ s m w,
-  begin
-    ext1, ext1 k,
-    exact is_limit.uniq _
-      (((evaluation K C).obj k).map_cone s) (m.app k) (λ j, nat_trans.congr_app (w j) k)
-  end }
-
-def functor_category_is_colimit_cocone [has_colimits_of_shape J C] (F : J ⥤ K ⥤ C) :
-  is_colimit (functor_category_colimit_cocone F) :=
-{ desc := λ s,
-  { app := λ k, colimit.desc (F.flip.obj k) (((evaluation K C).obj k).map_cocone s) },
-  uniq' := λ s m w,
-  begin
-    ext1, ext1 k,
-    exact is_colimit.uniq _
-      (((evaluation K C).obj k).map_cocone s) (m.app k) (λ j, nat_trans.congr_app (w j) k)
-  end }
+/-- Stitching together colimiting cocones gives a colimiting cocone. -/
+def combined_is_colimit (F : J ⥤ K ⥤ C) (c : Π (k : K), colimit_cocone (F.flip.obj k)) :
+  is_colimit (combine_cocones F c) :=
+evaluation_jointly_reflects_colimits _
+  (λ k, (c k).is_colimit.of_iso_colimit (evaluate_combined_cocones F c k).symm)
+
+noncomputable theory
 
 instance functor_category_has_limits_of_shape
   [has_limits_of_shape J C] : has_limits_of_shape J (K ⥤ C) :=
 { has_limit := λ F, has_limit.mk
-  { cone := functor_category_limit_cone F,
-    is_limit := functor_category_is_limit_cone F } }
+  { cone := combine_cones F (λ k, get_limit_cone _),
+    is_limit := combined_is_limit _ _ } }
 
 instance functor_category_has_colimits_of_shape
   [has_colimits_of_shape J C] : has_colimits_of_shape J (K ⥤ C) :=
 { has_colimit := λ F, has_colimit.mk
-  { cocone := functor_category_colimit_cocone F,
-    is_colimit := functor_category_is_colimit_cocone F } }
+  { cocone := combine_cocones _ (λ k, get_colimit_cocone _),
+    is_colimit := combined_is_colimit _ _ } }
 
 instance functor_category_has_limits [has_limits C] : has_limits (K ⥤ C) :=
 { has_limits_of_shape := λ J 𝒥, by resetI; apply_instance }
@@ -98,16 +135,16 @@ instance functor_category_has_colimits [has_colimits C] : has_colimits (K ⥤ C)
 instance evaluation_preserves_limits_of_shape [has_limits_of_shape J C] (k : K) :
   preserves_limits_of_shape J ((evaluation K C).obj k) :=
 { preserves_limit :=
-  λ F, preserves_limit_of_preserves_limit_cone (functor_category_is_limit_cone _) $
+  λ F, preserves_limit_of_preserves_limit_cone (combined_is_limit _ _) $
     is_limit.of_iso_limit (limit.is_limit _)
-      (evaluate_functor_category_limit_cone F k).symm }
+      (evaluate_combined_cones F _ k).symm }
 
 instance evaluation_preserves_colimits_of_shape [has_colimits_of_shape J C] (k : K) :
   preserves_colimits_of_shape J ((evaluation K C).obj k) :=
 { preserves_colimit :=
-  λ F, preserves_colimit_of_preserves_colimit_cocone (functor_category_is_colimit_cocone _) $
+  λ F, preserves_colimit_of_preserves_colimit_cocone (combined_is_colimit _ _) $
     is_colimit.of_iso_colimit (colimit.is_colimit _)
-      (evaluate_functor_category_colimit_cocone F k).symm }
+      (evaluate_combined_cocones F _ k).symm }
 
 instance evaluation_preserves_limits [has_limits C] (k : K) :
   preserves_limits ((evaluation K C).obj k) :=