Unify naming of lemmas related to the (co)lim functor (leanprover-com…

…munity#2040) Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
anrddh · May 15, 2020 · 6599524 · 6599524
1 parent c20b96e
commit 6599524
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 13 deletions.
diff --git a/src/algebraic_geometry/stalks.lean b/src/algebraic_geometry/stalks.lean
@@ -55,7 +55,7 @@ begin
   ext U,
   op_induction U,
   cases U,
-  simp only [colim.ι_map_assoc, colimit.ι_pre_assoc, colimit.ι_pre,
+  simp only [colimit.ι_map_assoc, colimit.ι_pre_assoc, colimit.ι_pre,
     whisker_left_app, whisker_right_app,
     assoc, id_comp, map_id, map_comp],
   dsimp,

diff --git a/src/category_theory/limits/limits.lean b/src/category_theory/limits/limits.lean
@@ -616,16 +616,16 @@ def lim : (J ⥤ C) ⥤ C :=
 
 variables {F} {G : J ⥤ C} (α : F ⟶ G)
 
-@[simp, reassoc] lemma lim.map_π (j : J) : lim.map α ≫ limit.π G j = limit.π F j ≫ α.app j :=
+@[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, lim.map_π, ←assoc, limit.lift_π, limit.lift_π]; refl
+by ext; rw [assoc, limit.map_π, ←assoc, limit.lift_π, limit.lift_π]; refl
 
 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_π, lim.map_π, assoc, lim.map_π, ←assoc, limit.pre_π]; refl
+by ext; rw [assoc, limit.pre_π, limit.map_π, assoc, limit.map_π, ←assoc, limit.pre_π]; refl
 
 lemma limit.map_pre' [has_limits_of_shape.{v} K C]
   (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟶ E₂) :
@@ -641,8 +641,8 @@ lemma limit.map_post {D : Type u'} [category.{v} D] [has_limits_of_shape J D] (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, lim.map_π, H.map_comp],
-  rw [assoc, lim.map_π, ←assoc, limit.post_π],
+  rw [assoc, limit.post_π, ←H.map_comp, limit.map_π, H.map_comp],
+  rw [assoc, limit.map_π, ←assoc, limit.post_π],
   refl
 end
 
@@ -898,16 +898,16 @@ def colim : (J ⥤ C) ⥤ C :=
 
 variables {F} {G : J ⥤ C} (α : F ⟶ G)
 
-@[simp, reassoc] lemma colim.ι_map (j : J) : colimit.ι F j ≫ colim.map α = α.app j ≫ colimit.ι G j :=
+@[simp, reassoc] lemma colimit.ι_map (j : J) : colimit.ι F j ≫ colim.map α = α.app j ≫ colimit.ι G j :=
 by apply is_colimit.fac
 
 @[simp] lemma colimit.map_desc (c : cocone G) :
   colim.map α ≫ colimit.desc G c = colimit.desc F ((cocones.precompose α).obj c) :=
-by ext; rw [←assoc, colim.ι_map, assoc, colimit.ι_desc, colimit.ι_desc]; refl
+by ext; rw [←assoc, colimit.ι_map, assoc, colimit.ι_desc, colimit.ι_desc]; refl
 
 lemma colimit.pre_map [has_colimits_of_shape K C] (E : K ⥤ J) :
   colimit.pre F E ≫ colim.map α = colim.map (whisker_left E α) ≫ colimit.pre G E :=
-by ext; rw [←assoc, colimit.ι_pre, colim.ι_map, ←assoc, colim.ι_map, assoc, colimit.ι_pre]; refl
+by ext; rw [←assoc, colimit.ι_pre, colimit.ι_map, ←assoc, colimit.ι_map, assoc, colimit.ι_pre]; refl
 
 lemma colimit.pre_map' [has_colimits_of_shape.{v} K C]
   (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟶ E₂) :
@@ -923,8 +923,8 @@ lemma colimit.map_post {D : Type u'} [category.{v} D] [has_colimits_of_shape J D
   colimit.post F H ≫ H.map (colim.map α) = colim.map (whisker_right α H) ≫ colimit.post G H:=
 begin
   ext,
-  rw [←assoc, colimit.ι_post, ←H.map_comp, colim.ι_map, H.map_comp],
-  rw [←assoc, colim.ι_map, assoc, colimit.ι_post],
+  rw [←assoc, colimit.ι_post, ←H.map_comp, colimit.ι_map, H.map_comp],
+  rw [←assoc, colimit.ι_map, assoc, colimit.ι_post],
   refl
 end
 

diff --git a/src/topology/sheaves/stalks.lean b/src/topology/sheaves/stalks.lean
@@ -74,7 +74,7 @@ begin
   ext1,
   tactic.op_induction',
   cases j, cases j_val,
-  rw [colim.ι_map_assoc, colim.ι_map, colimit.ι_pre, whisker_left_app, whisker_right_app,
+  rw [colimit.ι_map_assoc, colimit.ι_map, colimit.ι_pre, whisker_left_app, whisker_right_app,
        pushforward.id_hom_app, eq_to_hom_map, eq_to_hom_refl],
   dsimp,
   -- FIXME A simp lemma which unfortunately doesn't fire:
@@ -92,7 +92,7 @@ begin
   op_induction U,
   cases U,
   cases U_val,
-  simp only [colim.ι_map_assoc, colimit.ι_pre_assoc,
+  simp only [colimit.ι_map_assoc, colimit.ι_pre_assoc,
              whisker_right_app, category.assoc],
   dsimp,
   -- FIXME: Some of these are simp lemmas, but don't fire successfully: