chore(category_theory/limits): correct lemma names (#12606)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Mar 12, 2022 · 956f3db · 956f3db
1 parent 9456a74
commit 956f3db
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/src/category_theory/abelian/exact.lean b/src/category_theory/abelian/exact.lean
@@ -115,7 +115,7 @@ lemma is_equivalence.exact_iff {D : Type u₁} [category.{v₁} D] [abelian D]
   exact (F.map f) (F.map g) ↔ exact f g :=
 begin
   simp only [exact_iff, ← F.map_eq_zero_iff, F.map_comp, category.assoc,
-    ← kernel_comparison_comp_π g F, ← ι_comp_cokernel_comparison f F],
+    ← kernel_comparison_comp_ι g F, ← π_comp_cokernel_comparison f F],
   rw [is_iso.comp_left_eq_zero (kernel_comparison g F), ← category.assoc,
     is_iso.comp_right_eq_zero _ (cokernel_comparison f F)],
 end

diff --git a/src/category_theory/limits/shapes/kernels.lean b/src/category_theory/limits/shapes/kernels.lean
@@ -757,7 +757,7 @@ def kernel_comparison [has_kernel f] [has_kernel (G.map f)] :
 kernel.lift _ (G.map (kernel.ι f)) (by simp only [←G.map_comp, kernel.condition, functor.map_zero])
 
 @[simp, reassoc]
-lemma kernel_comparison_comp_π [has_kernel f] [has_kernel (G.map f)] :
+lemma kernel_comparison_comp_ι [has_kernel f] [has_kernel (G.map f)] :
   kernel_comparison f G ≫ kernel.ι (G.map f) = G.map (kernel.ι f) :=
 kernel.lift_ι _ _ _
 
@@ -775,7 +775,7 @@ cokernel.desc _ (G.map (coequalizer.π _ _))
   (by simp only [←G.map_comp, cokernel.condition, functor.map_zero])
 
 @[simp, reassoc]
-lemma ι_comp_cokernel_comparison [has_cokernel f] [has_cokernel (G.map f)] :
+lemma π_comp_cokernel_comparison [has_cokernel f] [has_cokernel (G.map f)] :
   cokernel.π (G.map f) ≫ cokernel_comparison f G = G.map (cokernel.π _) :=
 cokernel.π_desc _ _ _