chore(category_theory/limits/preserves): split up files and remove redundant defs (#4717)

Broken off from #4163 and #4716.
While the diff of this PR is quite big, it actually doesn't do very much: 

- I removed the definitions of `preserves_(co)limits_iso` from `preserves/basic`, since there's already a version in `preserves/shapes` which has lemmas about it. (I didn't keep them in `preserves/basic` since that file is already getting quite big, so I chose to instead put them into the smaller file.
- I split up `preserves/shapes` into two files: `preserves/limits` and `preserves/shapes`. From my other PRs my plan is for `shapes` to contain isomorphisms and constructions for special shapes, eg `fan.mk` and `fork`s, some of which aren't already present, and `limits` to have things for the general case. In this PR I don't change the situation for special shapes (other than simplifying some proofs), other than moving it into a separate file for clarity.

Author: b-mehta

src/algebraic_geometry/presheafed_space/has_colimits.lean

@@ -233,6 +233,19 @@ def colimit_cocone_is_colimit (F : J ⥤ PresheafedSpace C) : is_colimit (colimi
     c :=
     { app := λ U, desc_c_app F s U,
       naturality' := λ U V i, desc_c_naturality F s i }, },
+  fac' := -- tidy can do this but it takes too long
+  begin
+    intros s j,
+    dsimp,
+    fapply PresheafedSpace.ext,
+    { simp, },
+    { ext,
+      dsimp [desc_c_app],
+      simp only [eq_to_hom_op, limit.lift_π_assoc, eq_to_hom_map, assoc, pushforward.comp_inv_app,
+                 limit_obj_iso_limit_comp_evaluation_inv_π_app_assoc],
+      dsimp,
+      simp },
+  end,
   uniq' := λ s m w,
   begin
     -- We need to use the identity on the continuous maps twice, so we prepare that first:

src/category_theory/limits/functor_category.lean

@@ -3,7 +3,7 @@ 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.limits.preserves.basic
+import category_theory.limits.preserves.limits
 
 open category_theory category_theory.category
 
@@ -155,15 +155,15 @@ then the evaluation of that limit at `k` is the limit of the evaluations of `F.o
 -/
 def limit_obj_iso_limit_comp_evaluation [has_limits_of_shape J C] (F : J ⥤ K ⥤ C) (k : K) :
   (limit F).obj k ≅ limit (F ⋙ ((evaluation K C).obj k)) :=
-preserves_limit_iso F ((evaluation K C).obj k)
+preserves_limit_iso ((evaluation K C).obj k) F
 
 @[simp, reassoc]
 lemma limit_obj_iso_limit_comp_evaluation_hom_π
   [has_limits_of_shape J C] (F : J ⥤ (K ⥤ C)) (j : J) (k : K) :
   (limit_obj_iso_limit_comp_evaluation F k).hom ≫ limit.π (F ⋙ ((evaluation K C).obj k)) j =
     (limit.π F j).app k :=
 begin
-  dsimp [limit_obj_iso_limit_comp_evaluation, limits.preserves_limit_iso],
+  dsimp [limit_obj_iso_limit_comp_evaluation],
   simp,
 end
 
@@ -173,7 +173,7 @@ lemma limit_obj_iso_limit_comp_evaluation_inv_π_app
   (limit_obj_iso_limit_comp_evaluation F k).inv ≫ (limit.π F j).app k =
     limit.π (F ⋙ ((evaluation K C).obj k)) j :=
 begin
-  dsimp [limit_obj_iso_limit_comp_evaluation, limits.preserves_limit_iso],
+  dsimp [limit_obj_iso_limit_comp_evaluation],
   rw iso.inv_comp_eq,
   simp,
 end
@@ -201,15 +201,15 @@ then the evaluation of that colimit at `k` is the colimit of the evaluations of
 -/
 def colimit_obj_iso_colimit_comp_evaluation [has_colimits_of_shape J C] (F : J ⥤ K ⥤ C) (k : K) :
   (colimit F).obj k ≅ colimit (F ⋙ ((evaluation K C).obj k)) :=
-preserves_colimit_iso F ((evaluation K C).obj k)
+preserves_colimit_iso ((evaluation K C).obj k) F
 
 @[simp, reassoc]
 lemma colimit_obj_iso_colimit_comp_evaluation_ι_inv
   [has_colimits_of_shape J C] (F : J ⥤ (K ⥤ C)) (j : J) (k : K) :
   colimit.ι (F ⋙ ((evaluation K C).obj k)) j ≫ (colimit_obj_iso_colimit_comp_evaluation F k).inv =
     (colimit.ι F j).app k :=
 begin
-  dsimp [colimit_obj_iso_colimit_comp_evaluation, limits.preserves_colimit_iso],
+  dsimp [colimit_obj_iso_colimit_comp_evaluation],
   simp,
 end
 
@@ -219,7 +219,7 @@ lemma colimit_obj_iso_colimit_comp_evaluation_ι_app_hom
   (colimit.ι F j).app k ≫ (colimit_obj_iso_colimit_comp_evaluation F k).hom =
      colimit.ι (F ⋙ ((evaluation K C).obj k)) j :=
 begin
-  dsimp [colimit_obj_iso_colimit_comp_evaluation, limits.preserves_colimit_iso],
+  dsimp [colimit_obj_iso_colimit_comp_evaluation],
   rw ←iso.eq_comp_inv,
   simp,
 end

src/category_theory/limits/preserves/basic.lean

@@ -58,21 +58,6 @@ if `F` maps any colimit cocone over `K` to a colimit cocone.
 class preserves_colimit (K : J ⥤ C) (F : C ⥤ D) : Type (max u₁ u₂ v) :=
 (preserves : Π {c : cocone K}, is_colimit c → is_colimit (F.map_cocone c))
 
-/--
-A functor which preserves limits preserves
-the arbitrary choice of limit provided by `has_limit`, up to isomorphism.
--/
-def preserves_limit_iso (K : J ⥤ C) [has_limit K] (F : C ⥤ D) [has_limit (K ⋙ F)] [preserves_limit K F] :
-  F.obj (limit K) ≅ limit (K ⋙ F) :=
-is_limit.cone_point_unique_up_to_iso (preserves_limit.preserves (limit.is_limit K)) (limit.is_limit (K ⋙ F))
-/--
-A functor which preserves colimits preserves
-the arbitrary choice of colimit provided by `has_colimit` up to isomorphism.
--/
-def preserves_colimit_iso (K : J ⥤ C) [has_colimit K] (F : C ⥤ D) [has_colimit (K ⋙ F)] [preserves_colimit K F] :
-  F.obj (colimit K) ≅ colimit (K ⋙ F) :=
-is_colimit.cocone_point_unique_up_to_iso (preserves_colimit.preserves (colimit.is_colimit K)) (colimit.is_colimit (K ⋙ F))
-
 /-- We say that `F` preserves limits of shape `J` if `F` preserves limits for every diagram
     `K : J ⥤ C`, i.e., `F` maps limit cones over `K` to limit cones. -/
 class preserves_limits_of_shape (J : Type v) [small_category J] (F : C ⥤ D) : Type (max u₁ u₂ v) :=

src/category_theory/limits/preserves/limits.lean

@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison, Bhavik Mehta
+-/
+import category_theory.limits.preserves.basic
+import category_theory.limits.shapes
+
+/-!
+# Isomorphisms about functors which preserve (co)limits
+
+If `G` preserves limits, and `C` and `D` have limits, then for any diagram `F : J ⥤ C` we have a
+canonical isomorphism `preserves_limit_iso : G.obj (limit F) ≅ limit (F ⋙ G)`.
+We also show that we can commute `is_limit.lift` of a preserved limit with `functor.map_cone`:
+`(preserves_limit.preserves t).lift (G.map_cone c₂) = G.map (t.lift c₂)`.
+
+The duals of these are also given. For functors which preserve (co)limits of specific shapes, see
+`preserves/shapes.lean`.
+-/
+
+universes v u₁ u₂
+
+noncomputable theory
+
+open category_theory category_theory.category category_theory.limits
+
+variables {C : Type u₁} [category.{v} C]
+variables {D : Type u₂} [category.{v} D]
+variables (G : C ⥤ D)
+variables {J : Type v} [small_category J]
+variables (F : J ⥤ C)
+
+section
+variables [preserves_limit F G]
+
+@[simp]
+lemma preserves_lift_map_cone (c₁ c₂ : cone F) (t : is_limit c₁) :
+  (preserves_limit.preserves t).lift (G.map_cone c₂) = G.map (t.lift c₂) :=
+((preserves_limit.preserves t).uniq (G.map_cone c₂) _ (by simp [← G.map_comp])).symm
+
+variables [has_limit F] [has_limit (F ⋙ G)]
+/--
+If `G` preserves limits, we have an isomorphism from the image of the limit of a functor `F`
+to the limit of the functor `F ⋙ G`.
+-/
+def preserves_limit_iso : G.obj (limit F) ≅ limit (F ⋙ G) :=
+(preserves_limit.preserves (limit.is_limit _)).cone_point_unique_up_to_iso (limit.is_limit _)
+
+@[simp, reassoc]
+lemma preserves_limits_iso_hom_π (j) :
+  (preserves_limit_iso G F).hom ≫ limit.π _ j = G.map (limit.π F j) :=
+is_limit.cone_point_unique_up_to_iso_hom_comp _ _ j
+
+@[simp, reassoc]
+lemma preserves_limits_iso_inv_π (j) :
+  (preserves_limit_iso G F).inv ≫ G.map (limit.π F j) = limit.π _ j :=
+is_limit.cone_point_unique_up_to_iso_inv_comp _ _ j
+
+@[simp, reassoc]
+lemma lift_comp_preserves_limits_iso_hom (t : cone F) :
+  G.map (limit.lift _ t) ≫ (preserves_limit_iso G F).hom = limit.lift (F ⋙ G) (G.map_cone _) :=
+by { ext, simp [← G.map_comp] }
+end
+
+section
+variables [preserves_colimit F G]
+
+@[simp]
+lemma preserves_desc_map_cocone (c₁ c₂ : cocone F) (t : is_colimit c₁) :
+  (preserves_colimit.preserves t).desc (G.map_cocone _) = G.map (t.desc c₂) :=
+((preserves_colimit.preserves t).uniq (G.map_cocone _) _ (by simp [← G.map_comp])).symm
+
+variables [has_colimit F] [has_colimit (F ⋙ G)]
+/--
+If `G` preserves colimits, we have an isomorphism from the image of the colimit of a functor `F`
+to the colimit of the functor `F ⋙ G`.
+-/
+-- TODO: think about swapping the order here
+def preserves_colimit_iso : G.obj (colimit F) ≅ colimit (F ⋙ G) :=
+(preserves_colimit.preserves (colimit.is_colimit _)).cocone_point_unique_up_to_iso
+  (colimit.is_colimit _)
+
+@[simp, reassoc]
+lemma ι_preserves_colimits_iso_inv (j : J) :
+  colimit.ι _ j ≫ (preserves_colimit_iso G F).inv = G.map (colimit.ι F j) :=
+is_colimit.comp_cocone_point_unique_up_to_iso_inv _ (colimit.is_colimit (F ⋙ G)) j
+
+@[simp, reassoc]
+lemma ι_preserves_colimits_iso_hom (j : J) :
+  G.map (colimit.ι F j) ≫ (preserves_colimit_iso G F).hom = colimit.ι (F ⋙ G) j :=
+(preserves_colimit.preserves (colimit.is_colimit _)).comp_cocone_point_unique_up_to_iso_hom _ j
+
+@[simp, reassoc]
+lemma preserves_colimits_iso_inv_comp_desc (t : cocone F) :
+  (preserves_colimit_iso G F).inv ≫ G.map (colimit.desc _ t) = colimit.desc _ (G.map_cocone t) :=
+by { ext, simp [← G.map_comp] }
+end

src/category_theory/limits/preserves/shapes.lean

@@ -3,43 +3,22 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import category_theory.limits.preserves.basic
-import category_theory.limits.shapes.products
+import category_theory.limits.preserves.limits
+import category_theory.limits.shapes
 
 universes v u₁ u₂
 
 noncomputable theory
 
-open category_theory
-open category_theory.limits
+open category_theory category_theory.category category_theory.limits
 
 variables {C : Type u₁} [category.{v} C]
 variables {D : Type u₂} [category.{v} D]
 variables (G : C ⥤ D) [preserves_limits G]
 
-section
-variables {J : Type v} [small_category J]
+section preserve_products
 
-/--
-If `G` preserves limits, we have an isomorphism from the image of the limit of a functor `F`
-to the limit of the functor `F ⋙ G`.
--/
-def preserves_limits_iso (F : J ⥤ C) [has_limit F] [has_limit (F ⋙ G)] :
-  G.obj (limit F) ≅ limit (F ⋙ G) :=
-(cones.forget _).map_iso
-  (is_limit.unique_up_to_iso
-    (preserves_limit.preserves (limit.is_limit F))
-    (limit.is_limit (F ⋙ G)))
-
-@[simp, reassoc]
-lemma preserves_limits_iso_hom_π
-  (F : J ⥤ C) [has_limit F] [has_limit (F ⋙ G)] (j) :
-  (preserves_limits_iso G F).hom ≫ limit.π _ j = G.map (limit.π F j) :=
-begin
-  dsimp [preserves_limits_iso, has_limit.iso_of_nat_iso, cones.postcompose,
-    is_limit.unique_up_to_iso, is_limit.lift_cone_morphism],
-  simp,
-end
+variables {J : Type v} (f : J → C)
 
 /--
 If `G` preserves limits, we have an isomorphism
@@ -48,30 +27,19 @@ from the image of a product to the product of the images.
 -- TODO perhaps weaken the assumptions here, to just require the relevant limits?
 def preserves_products_iso {J : Type v} (f : J → C) [has_limits C] [has_limits D] :
   G.obj (pi_obj f) ≅ pi_obj (λ j, G.obj (f j)) :=
-preserves_limits_iso G (discrete.functor f) ≪≫
+preserves_limit_iso G (discrete.functor f) ≪≫
   has_limit.iso_of_nat_iso (discrete.nat_iso (λ j, iso.refl _))
 
 @[simp, reassoc]
 lemma preserves_products_iso_hom_π
   {J : Type v} (f : J → C) [has_limits C] [has_limits D] (j) :
   (preserves_products_iso G f).hom ≫ pi.π _ j = G.map (pi.π f j) :=
-begin
-  dsimp [preserves_products_iso, preserves_limits_iso, has_limit.iso_of_nat_iso, cones.postcompose,
-         is_limit.unique_up_to_iso, is_limit.lift_cone_morphism, is_limit.map],
-  simp only [limit.lift_π, discrete.nat_iso_hom_app, limit.cone_π, limit.lift_π_assoc,
-             nat_trans.comp_app, category.assoc, functor.map_cone_π, is_limit.map_π],
-  dsimp, simp, -- See note [dsimp, simp],
-end
+by simp [preserves_products_iso]
 
 @[simp, reassoc]
 lemma map_lift_comp_preserves_products_iso_hom
   {J : Type v} (f : J → C) [has_limits C] [has_limits D] (P : C) (g : Π j, P ⟶ f j) :
   G.map (pi.lift g) ≫ (preserves_products_iso G f).hom = pi.lift (λ j, G.map (g j)) :=
-begin
-  ext,
-  simp only [limit.lift_π, fan.mk_π_app, preserves_products_iso_hom_π, category.assoc],
-  simp only [←G.map_comp],
-  simp only [limit.lift_π, fan.mk_π_app],
-end
+by { ext, simp [←G.map_comp] }
 
-end
+end preserve_products