feat(category_theory): preservation of (co)limits, (co)limits in func…

…tor categories

category_theory/limits/functor_category.lean

@@ -0,0 +1,126 @@
+-- Copyright (c) 2018 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison
+
+import category_theory.products
+import category_theory.limits.preserves
+
+open category_theory category_theory.category
+
+namespace category_theory.limits
+
+universes u v
+
+variables {C : Type u} [𝒞 : category.{u v} C]
+include 𝒞
+
+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
+
+@[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
+
+@[simp] def functor_category_limit_cone [has_limits_of_shape J C] (F : J ⥤ K ⥤ C) :
+  cone F :=
+{ X := F.flip ⋙ lim,
+  π :=
+  { 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 } }
+
+@[simp] def functor_category_colimit_cocone [has_colimits_of_shape J C] (F : J ⥤ K ⥤ C) :
+  cocone F :=
+{ X := F.flip ⋙ colim,
+  ι :=
+  { 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)
+
+@[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) :=
+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),
+    naturality' := λ k k' f,
+      by ext; dsimp; simpa using (s.π.app j).naturality f },
+  uniq' := λ s m w,
+  begin
+    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.{u v} 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),
+    naturality' := λ k k' f,
+    begin
+      ext,
+      rw [←assoc, ←assoc],
+      dsimp [functor.flip],
+      simpa using (s.ι.app j).naturality f
+    end },
+  uniq' := λ s m w,
+  begin
+    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 }
+
+instance functor_category_has_limits_of_shape
+  [has_limits_of_shape J C] : has_limits_of_shape J (K ⥤ C) :=
+λ F,
+{ cone := functor_category_limit_cone F,
+  is_limit := functor_category_is_limit_cone F }
+
+instance functor_category_has_colimits_of_shape
+  [has_colimits_of_shape J C] : has_colimits_of_shape J (K ⥤ C) :=
+λ F,
+{ cocone := functor_category_colimit_cocone F,
+  is_colimit := functor_category_is_colimit_cocone F }
+
+instance functor_category_has_limits [has_limits C] : has_limits (K ⥤ C) :=
+λ J 𝒥, by resetI; apply_instance
+
+instance functor_category_has_colimits [has_colimits C] : has_colimits (K ⥤ C) :=
+λ J 𝒥, by resetI; apply_instance
+
+instance evaluation_preserves_limits_of_shape [has_limits_of_shape J C] (k : K) :
+  preserves_limits_of_shape J ((evaluation K C).obj k) :=
+λ F, preserves_limit_of_preserves_limit_cone (limit.is_limit _) $
+  is_limit.of_iso_limit (limit.is_limit _)
+    (evaluate_functor_category_limit_cone 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) :=
+λ F, preserves_colimit_of_preserves_colimit_cocone (colimit.is_colimit _) $
+  is_colimit.of_iso_colimit (colimit.is_colimit _)
+    (evaluate_functor_category_colimit_cocone F k).symm
+
+instance evaluation_preserves_limits [has_limits C] (k : K) :
+  preserves_limits ((evaluation K C).obj k) :=
+λ J 𝒥, by resetI; apply_instance
+
+instance evaluation_preserves_colimits [has_colimits C] (k : K) :
+  preserves_colimits ((evaluation K C).obj k) :=
+λ J 𝒥, by resetI; apply_instance
+
+end category_theory.limits

category_theory/limits/preserves.lean

@@ -0,0 +1,180 @@
+-- Copyright (c) 2018 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison, Reid Barton
+
+-- Preservation and reflection of (co)limits.
+
+import category_theory.whiskering
+import category_theory.limits.limits
+
+open category_theory
+
+namespace category_theory.limits
+
+universes u₁ u₂ u₃ v
+
+variables {C : Type u₁} [𝒞 : category.{u₁ v} C]
+variables {D : Type u₂} [𝒟 : category.{u₂ v} D]
+include 𝒞 𝒟
+
+variables {J : Type v} [small_category J] {K : J ⥤ C}
+
+/- Note on "preservation of (co)limits"
+
+There are various distinct notions of "preserving limits". The one we
+aim to capture here is: A functor F : C → D "preserves limits" if it
+sends every limit cone in C to a limit cone in D. Informally, F
+preserves all the limits which exist in C.
+
+Note that:
+
+* Of course, we do not want to require F to *strictly* take chosen
+  limit cones of C to chosen limit cones of D. Indeed, the above
+  definition makes no reference to a choice of limit cones so it makes
+  sense without any conditions on C or D.
+
+* Some diagrams in C may have no limit. In this case, there is no
+  condition on the behavior of F on such diagrams. There are other
+  notions (such as "flat functor") which impose conditions also on
+  diagrams in C with no limits, but these are not considered here.
+
+In order to be able to express the property of preserving limits of a
+certain form, we say that a functor F preserves the limit of a
+diagram K if F sends every limit cone on K to a limit cone. This is
+vacuously satisfied when K does not admit a limit, which is consistent
+with the above definition of "preserves limits".
+
+-/
+
+class preserves_limit (K : J ⥤ C) (F : C ⥤ D) :=
+(preserves : Π {c : cone K}, is_limit c → is_limit (F.map_cone c))
+class preserves_colimit (K : J ⥤ C) (F : C ⥤ D) :=
+(preserves : Π {c : cocone K}, is_colimit c → is_colimit (F.map_cocone c))
+
+@[class] def preserves_limits_of_shape (J : Type v) [small_category J] (F : C ⥤ D) :=
+Π {K : J ⥤ C}, preserves_limit K F
+@[class] def preserves_colimits_of_shape (J : Type v) [small_category J] (F : C ⥤ D) :=
+Π {K : J ⥤ C}, preserves_colimit K F
+
+@[class] def preserves_limits (F : C ⥤ D) :=
+Π {J : Type v} {𝒥 : small_category J}, by exactI preserves_limits_of_shape J F
+@[class] def preserves_colimits (F : C ⥤ D) :=
+Π {J : Type v} {𝒥 : small_category J}, by exactI preserves_colimits_of_shape J F
+
+instance preserves_limit_of_preserves_limits_of_shape (F : C ⥤ D)
+  [H : preserves_limits_of_shape J F] : preserves_limit K F :=
+H
+instance preserves_colimit_of_preserves_colimits_of_shape (F : C ⥤ D)
+  [H : preserves_colimits_of_shape J F] : preserves_colimit K F :=
+H
+
+instance preserves_limits_of_shape_of_preserves_limits (F : C ⥤ D)
+  [H : preserves_limits F] : preserves_limits_of_shape J F :=
+@H J _
+instance preserves_colimits_of_shape_of_preserves_colimits (F : C ⥤ D)
+  [H : preserves_colimits F] : preserves_colimits_of_shape J F :=
+@H J _
+
+instance id_preserves_limits : preserves_limits (functor.id C) :=
+λ J 𝒥 K, by exactI ⟨λ c h,
+  ⟨λ s, h.lift ⟨s.X, λ j, s.π.app j, λ j j' f, s.π.naturality f⟩,
+   by cases K; rcases c with ⟨_, _, _⟩; intros s j; cases s; exact h.fac _ j,
+   by cases K; rcases c with ⟨_, _, _⟩; intros s m w; rcases s with ⟨_, _, _⟩; exact h.uniq _ m w⟩⟩
+
+instance id_preserves_colimits : preserves_colimits (functor.id C) :=
+λ J 𝒥 K, by exactI ⟨λ c h,
+  ⟨λ s, h.desc ⟨s.X, λ j, s.ι.app j, λ j j' f, s.ι.naturality f⟩,
+   by cases K; rcases c with ⟨_, _, _⟩; intros s j; cases s; exact h.fac _ j,
+   by cases K; rcases c with ⟨_, _, _⟩; intros s m w; rcases s with ⟨_, _, _⟩; exact h.uniq _ m w⟩⟩
+
+section
+variables {E : Type u₃} [ℰ : category.{u₃ v} E]
+variables (F : C ⥤ D) (G : D ⥤ E)
+
+local attribute [elab_simple] preserves_limit.preserves preserves_colimit.preserves
+
+instance comp_preserves_limit [preserves_limit K F] [preserves_limit (K ⋙ F) G] :
+  preserves_limit K (F ⋙ G) :=
+⟨λ c h, preserves_limit.preserves G (preserves_limit.preserves F h)⟩
+
+instance comp_preserves_colimit [preserves_colimit K F] [preserves_colimit (K ⋙ F) G] :
+  preserves_colimit K (F ⋙ G) :=
+⟨λ c h, preserves_colimit.preserves G (preserves_colimit.preserves F h)⟩
+
+end
+
+/-- If F preserves one limit cone for the diagram K,
+  then it preserves any limit cone for K. -/
+def preserves_limit_of_preserves_limit_cone {F : C ⥤ D} {t : cone K}
+  (h : is_limit t) (hF : is_limit (F.map_cone t)) : preserves_limit K F :=
+⟨λ t' h', is_limit.of_iso_limit hF (functor.on_iso _ (is_limit.unique h h'))⟩
+
+/-- If F preserves one colimit cocone for the diagram K,
+  then it preserves any colimit cocone for K. -/
+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.on_iso _ (is_colimit.unique h h'))⟩
+
+/-
+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.
+Note that again we do not assume a priori that D actually has any
+limits.
+-/
+
+class reflects_limit (K : J ⥤ C) (F : C ⥤ D) :=
+(reflects : Π {c : cone K}, is_limit (F.map_cone c) → is_limit c)
+class reflects_colimit (K : J ⥤ C) (F : C ⥤ D) :=
+(reflects : Π {c : cocone K}, is_colimit (F.map_cocone c) → is_colimit c)
+
+@[class] def reflects_limits_of_shape (J : Type v) [small_category J] (F : C ⥤ D) :=
+Π {K : J ⥤ C}, reflects_limit K F
+@[class] def reflects_colimits_of_shape (J : Type v) [small_category J] (F : C ⥤ D) :=
+Π {K : J ⥤ C}, reflects_colimit K F
+
+@[class] def reflects_limits (F : C ⥤ D) :=
+Π {J : Type v} {𝒥 : small_category J}, by exactI reflects_limits_of_shape J F
+@[class] def reflects_colimits (F : C ⥤ D) :=
+Π {J : Type v} {𝒥 : small_category J}, by exactI reflects_colimits_of_shape J F
+
+instance reflects_limit_of_reflects_limits_of_shape (K : J ⥤ C) (F : C ⥤ D)
+  [H : reflects_limits_of_shape J F] : reflects_limit K F :=
+H
+instance reflects_colimit_of_reflects_colimits_of_shape (K : J ⥤ C) (F : C ⥤ D)
+  [H : reflects_colimits_of_shape J F] : reflects_colimit K F :=
+H
+
+instance reflects_limits_of_shape_of_reflects_limits (F : C ⥤ D)
+  [H : reflects_limits F] : reflects_limits_of_shape J F :=
+@H J _
+instance reflects_colimits_of_shape_of_reflects_colimits (F : C ⥤ D)
+  [H : reflects_colimits F] : reflects_colimits_of_shape J F :=
+@H J _
+
+instance id_reflects_limits : reflects_limits (functor.id C) :=
+λ J 𝒥 K, by exactI ⟨λ c h,
+  ⟨λ s, h.lift ⟨s.X, λ j, s.π.app j, λ j j' f, s.π.naturality f⟩,
+   by cases K; rcases c with ⟨_, _, _⟩; intros s j; cases s; exact h.fac _ j,
+   by cases K; rcases c with ⟨_, _, _⟩; intros s m w; rcases s with ⟨_, _, _⟩; exact h.uniq _ m w⟩⟩
+
+instance id_reflects_colimits : reflects_colimits (functor.id C) :=
+λ J 𝒥 K, by exactI ⟨λ c h,
+  ⟨λ s, h.desc ⟨s.X, λ j, s.ι.app j, λ j j' f, s.ι.naturality f⟩,
+   by cases K; rcases c with ⟨_, _, _⟩; intros s j; cases s; exact h.fac _ j,
+   by cases K; rcases c with ⟨_, _, _⟩; intros s m w; rcases s with ⟨_, _, _⟩; exact h.uniq _ m w⟩⟩
+
+section
+variables {E : Type u₃} [ℰ : category.{u₃ v} E]
+variables (F : C ⥤ D) (G : D ⥤ E)
+
+instance comp_reflects_limit [reflects_limit K F] [reflects_limit (K ⋙ F) G] :
+  reflects_limit K (F ⋙ G) :=
+⟨λ c h, reflects_limit.reflects (reflects_limit.reflects h)⟩
+
+instance comp_reflects_colimit [reflects_colimit K F] [reflects_colimit (K ⋙ F) G] :
+  reflects_colimit K (F ⋙ G) :=
+⟨λ c h, reflects_colimit.reflects (reflects_colimit.reflects h)⟩
+
+end
+
+end category_theory.limits

category_theory/natural_transformation.lean

@@ -59,6 +59,8 @@ begin
   subst hc
 end
 
+lemma congr_app {α β : F ⟹ G} (h : α = β) (X : C) : α.app X = β.app X := by rw h
+
 /-- `vcomp α β` is the vertical compositions of natural transformations. -/
 def vcomp (α : F ⟹ G) (β : G ⟹ H) : F ⟹ H :=
 { app         := λ X, (α.app X) ≫ (β.app X),