chore(category_theory/limits): Use lim_map over lim.map (#4856)

Modify the simp-normal form for `lim.map` to be `lim_map` instead, and express lemmas in terms of `lim_map` instead, as well as use it in special shapes so that the assumptions can be weakened.

src/category_theory/limits/colimit_limit.lean

@@ -64,7 +64,7 @@ limit.lift ((curry.obj F) ⋙ colim)
         begin
           dsimp,
           intros k k' f,
-          simp only [functor.comp_map, curry.obj_map_app, limits.limit.map_π_assoc, swap_map,
+          simp only [functor.comp_map, curry.obj_map_app, limits.lim_map_π_assoc, swap_map,
             category.comp_id, map_id_left_eq_curry_map, colimit.w],
         end }, },
     naturality' :=

src/category_theory/limits/connected.lean

@@ -102,14 +102,14 @@ def prod_preserves_connected_limits [is_connected J] (X : C) :
       fac' := λ s j,
       begin
         apply prod.hom_ext,
-        { erw [assoc, limit.map_π, comp_id, limit.lift_π],
+        { erw [assoc, lim_map_π, comp_id, limit.lift_π],
           exact (nat_trans_from_is_connected (s.π ≫ γ₁ X) j (classical.arbitrary _)).symm },
         { simp [← l.fac (forget_cone s) j] }
       end,
       uniq' := λ s m L,
       begin
         apply prod.hom_ext,
-        { erw [limit.lift_π, ← L (classical.arbitrary J), assoc, limit.map_π, comp_id],
+        { erw [limit.lift_π, ← L (classical.arbitrary J), assoc, lim_map_π, comp_id],
           refl },
         { rw limit.lift_π,
           apply l.uniq (forget_cone s),

src/category_theory/limits/limits.lean

@@ -1033,6 +1033,10 @@ by { dsimp [limit.iso_limit_cone, is_limit.cone_point_unique_up_to_iso], tidy, }
   (w : ∀ j, f ≫ limit.π F j = f' ≫ limit.π F j) : f = f' :=
 (limit.is_limit F).hom_ext w
 
+@[simp] lemma limit.lift_map {F G : J ⥤ C} [has_limit F] [has_limit G] (c : cone F) (α : F ⟶ G) :
+  limit.lift F c ≫ lim_map α = limit.lift G ((cones.postcompose α).obj c) :=
+by { ext, rw [assoc, lim_map_π, limit.lift_π_assoc, limit.lift_π], refl }
+
 @[simp] lemma limit.lift_cone {F : J ⥤ C} [has_limit F] :
   limit.lift F (limit.cone F) = 𝟙 (limit F) :=
 (limit.is_limit _).lift_self
@@ -1149,7 +1153,7 @@ The canonical morphism from the limit of `F` to the limit of `E ⋙ F`.
 def limit.pre : limit F ⟶ limit (E ⋙ F) :=
 limit.lift (E ⋙ F) ((limit.cone F).whisker E)
 
-@[simp] lemma limit.pre_π (k : K) : limit.pre F E ≫ limit.π (E ⋙ F) k = limit.π F (E.obj k) :=
+@[simp, reassoc] lemma limit.pre_π (k : K) : limit.pre F E ≫ limit.π (E ⋙ F) k = limit.π F (E.obj k) :=
 by { erw is_limit.fac, refl }
 
 @[simp] lemma limit.lift_pre (c : cone F) :
@@ -1187,7 +1191,8 @@ The canonical morphism from `G` applied to the limit of `F` to the limit of `F 
 def limit.post : G.obj (limit F) ⟶ limit (F ⋙ G) :=
 limit.lift (F ⋙ G) (G.map_cone (limit.cone F))
 
-@[simp] lemma limit.post_π (j : J) : limit.post F G ≫ limit.π (F ⋙ G) j = G.map (limit.π F j) :=
+@[simp, reassoc] lemma limit.post_π (j : J) :
+  limit.post F G ≫ limit.π (F ⋙ G) j = G.map (limit.π F j) :=
 by { erw is_limit.fac, refl }
 
 @[simp] lemma limit.lift_post (c : cone F) :
@@ -1236,7 +1241,6 @@ section lim_functor
 variables [has_limits_of_shape J C]
 
 section
-local attribute [simp] lim_map
 
 /-- `limit F` is functorial in `F`, when `C` has all limits of shape `J`. -/
 @[simps obj]
@@ -1250,16 +1254,12 @@ end
 
 variables {F} {G : J ⥤ C} (α : F ⟶ G)
 
-@[simp, reassoc] lemma limit.map_π (j : J) : lim.map α ≫ limit.π G j = limit.π F j ≫ α.app j :=
-by apply is_limit.fac
-
-@[simp] lemma limit.lift_map (c : cone F) :
-  limit.lift F c ≫ lim.map α = limit.lift G ((cones.postcompose α).obj c) :=
-by ext; rw [assoc, limit.map_π, ←assoc, limit.lift_π, limit.lift_π]; refl
+-- We generate this manually since `simps` gives it a weird name.
+@[simp] lemma lim_map_eq_lim_map : lim.map α = lim_map α := rfl
 
 lemma limit.map_pre [has_limits_of_shape K C] (E : K ⥤ J) :
   lim.map α ≫ limit.pre G E = limit.pre F E ≫ lim.map (whisker_left E α) :=
-by ext; rw [assoc, limit.pre_π, limit.map_π, assoc, limit.map_π, ←assoc, limit.pre_π]; refl
+by { ext, simp }
 
 lemma limit.map_pre' [has_limits_of_shape K C]
   (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟶ E₂) :
@@ -1272,12 +1272,10 @@ limit.pre F (𝟭 _) = lim.map (functor.left_unitor F).inv := by tidy
 lemma limit.map_post {D : Type u'} [category.{v} D] [has_limits_of_shape J D] (H : C ⥤ D) :
 /- H (limit F) ⟶ H (limit G) ⟶ limit (G ⋙ H) vs
    H (limit F) ⟶ limit (F ⋙ H) ⟶ limit (G ⋙ H) -/
-  H.map (lim.map α) ≫ limit.post G H = limit.post F H ≫ lim.map (whisker_right α H) :=
+  H.map (lim_map α) ≫ limit.post G H = limit.post F H ≫ lim_map (whisker_right α H) :=
 begin
   ext,
-  rw [assoc, limit.post_π, ←H.map_comp, limit.map_π, H.map_comp],
-  rw [assoc, limit.map_π, ←assoc, limit.post_π],
-  refl
+  simp only [whisker_right_app, lim_map_π, assoc, limit.post_π_assoc, limit.post_π, ← H.map_comp],
 end
 
 /--

src/category_theory/limits/shapes/products.lean

@@ -82,9 +82,9 @@ colimit.desc _ (cofan.mk P p)
 Construct a morphism between categorical products (indexed by the same type)
 from a family of morphisms between the factors.
 -/
-abbreviation pi.map {f g : β → C} [has_products_of_shape β C]
+abbreviation pi.map {f g : β → C} [has_product f] [has_product g]
   (p : Π b, f b ⟶ g b) : ∏ f ⟶ ∏ g :=
-lim.map (discrete.nat_trans p)
+lim_map (discrete.nat_trans p)
 /--
 Construct an isomorphism between categorical products (indexed by the same type)
 from a family of isomorphisms between the factors.
@@ -96,9 +96,9 @@ lim.map_iso (discrete.nat_iso p)
 Construct a morphism between categorical coproducts (indexed by the same type)
 from a family of morphisms between the factors.
 -/
-abbreviation sigma.map {f g : β → C} [has_coproducts_of_shape β C]
+abbreviation sigma.map {f g : β → C} [has_coproduct f] [has_coproduct g]
   (p : Π b, f b ⟶ g b) : ∐ f ⟶ ∐ g :=
-colim.map (discrete.nat_trans p)
+colim_map (discrete.nat_trans p)
 /--
 Construct an isomorphism between categorical coproducts (indexed by the same type)
 from a family of isomorphisms between the factors.

src/category_theory/limits/types.lean

@@ -120,8 +120,8 @@ congr_fun (limit.lift_π s j) x
 
 @[simp]
 lemma limit.map_π_apply {F G : J ⥤ Type u} (α : F ⟶ G) (j : J) (x) :
-  limit.π G j (lim.map α x) = α.app j (limit.π F j x) :=
-congr_fun (limit.map_π α j) x
+  limit.π G j (lim_map α x) = α.app j (limit.π F j x) :=
+congr_fun (lim_map_π α j) x
 
 /--
 The relation defining the quotient type which implements the colimit of a functor `F : J ⥤ Type u`.

src/category_theory/monoidal/limits.lean

@@ -52,7 +52,7 @@ instance limit_lax_monoidal : lax_monoidal (λ F : J ⥤ C, limit F) :=
   begin
     ext, dsimp,
     simp only [limit.lift_π, cones.postcompose_obj_π, monoidal.tensor_hom_app, limit.lift_map,
-      nat_trans.comp_app, category.assoc, ←tensor_comp, limit.map_π],
+      nat_trans.comp_app, category.assoc, ←tensor_comp, lim_map_π],
   end,
   associativity' := λ X Y Z,
   begin

src/topology/sheaves/local_predicate.lean

@@ -180,14 +180,14 @@ def diagram_subtype {ι : Type v} (U : ι → opens X) :
     { dsimp [left_res, subpresheaf_to_Types, presheaf_to_Types],
       simp only [limit.lift_map],
       ext1 ⟨i₁,i₂⟩,
-      simp only [limit.lift_π, cones.postcompose_obj_π, discrete.nat_trans_app, limit.map_π_assoc,
+      simp only [limit.lift_π, cones.postcompose_obj_π, discrete.nat_trans_app, lim_map_π_assoc,
         fan.mk_π_app, nat_trans.comp_app, category.assoc],
       ext,
       simp only [types_comp_apply, subtype.val_eq_coe], },
     { dsimp [right_res, subpresheaf_to_Types, presheaf_to_Types],
       simp only [limit.lift_map],
       ext1 ⟨i₁,i₂⟩,
-      simp only [limit.lift_π, cones.postcompose_obj_π, discrete.nat_trans_app, limit.map_π_assoc,
+      simp only [limit.lift_π, cones.postcompose_obj_π, discrete.nat_trans_app, lim_map_π_assoc,
         fan.mk_π_app, nat_trans.comp_app, category.assoc],
       ext,
       simp only [types_comp_apply, subtype.val_eq_coe], },
@@ -241,13 +241,13 @@ begin
   rcases j with ⟨_|_⟩,
   { apply limit.hom_ext,
     intro i,
-    simp only [category.assoc, limit.map_π],
+    simp only [category.assoc, lim_map_π],
     ext f' ⟨x, mem⟩,
     dsimp [res, subpresheaf_to_Types, presheaf_to_Types],
     simp only [discrete.nat_trans_app, limit.map_π_apply, fan.mk_π_app, limit.lift_π_apply], },
   { apply limit.hom_ext,
     intro i,
-    simp only [category.assoc, limit.map_π],
+    simp only [category.assoc, lim_map_π],
     ext f' ⟨x, mem⟩,
     dsimp [res, left_res, subpresheaf_to_Types, presheaf_to_Types],
     simp only [discrete.nat_trans_app, limit.map_π_apply, pi_lift_π_apply, types_comp_apply,
@@ -292,7 +292,7 @@ begin
         nat_trans.comp_app, category.assoc] at fac_i,
       have fac_i_f := congr_fun fac_i f,
       simp only [diagram_subtype, discrete.nat_trans_app, types_comp_apply,
-        presheaf_to_Types_map, limit.map_π, subtype.val_eq_coe] at fac_i_f,
+        presheaf_to_Types_map, lim_map_π, subtype.val_eq_coe] at fac_i_f,
       erw fac_i_f,
       apply subtype.property, }, },
   { -- Proving the factorisation condition is straightforward:

src/topology/sheaves/sheaf_condition/equalizer_products.lean

@@ -194,15 +194,15 @@ nat_iso.of_components
     { ext,
       dsimp [left_res, is_open_map.functor],
       simp only [limit.lift_π, cones.postcompose_obj_π, iso.op_hom, discrete.nat_iso_hom_app,
-        functor.map_iso_refl, functor.map_iso_hom, limit.map_π_assoc, limit.lift_map, fan.mk_π_app,
+        functor.map_iso_refl, functor.map_iso_hom, lim_map_π_assoc, limit.lift_map, fan.mk_π_app,
         nat_trans.comp_app, category.assoc],
       dsimp,
       rw [category.id_comp, ←F.map_comp],
       refl, },
     { ext,
       dsimp [right_res, is_open_map.functor],
       simp only [limit.lift_π, cones.postcompose_obj_π, iso.op_hom, discrete.nat_iso_hom_app,
-        functor.map_iso_refl, functor.map_iso_hom, limit.map_π_assoc, limit.lift_map, fan.mk_π_app,
+        functor.map_iso_refl, functor.map_iso_hom, lim_map_π_assoc, limit.lift_map, fan.mk_π_app,
         nat_trans.comp_app, category.assoc],
       dsimp,
       rw [category.id_comp, ←F.map_comp],
@@ -235,7 +235,7 @@ begin
       limit.lift_π, cones.postcompose_obj_π, functor.comp_map,
       fork_π_app_walking_parallel_pair_zero, pi_opens.iso_of_open_embedding,
       nat_iso.of_components.inv_app, functor.map_iso_refl, functor.op_map, limit.lift_map,
-      fan.mk_π_app, nat_trans.comp_app, has_hom.hom.unop_op, category.assoc],
+      fan.mk_π_app, nat_trans.comp_app, has_hom.hom.unop_op, category.assoc, lim_map_eq_lim_map],
     dsimp,
     rw [category.comp_id, ←F.map_comp],
     refl, },