feat(CategoryTheory/EqToHom): generalize Functor.congr_map to Prefunc…

…tor.congr_map (#12384)
leanprover-community · Apr 24, 2024 · cba2f37 · cba2f37
1 parent d0ecb3c
commit cba2f37
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 4 deletions.
diff --git a/Mathlib/CategoryTheory/Category/Cat/Limit.lean b/Mathlib/CategoryTheory/Category/Cat/Limit.lean
@@ -106,7 +106,7 @@ def limitConeLift (F : J ⥤ Cat.{v, v}) (s : Cone F) : s.pt ⟶ limitConeX F wh
       { pt := s.pt
         π :=
           { app := fun j => (s.π.app j).obj
-            naturality := fun _ _ f => Functor.congr_map objects (s.π.naturality f) } }
+            naturality := fun _ _ f => objects.congr_map (s.π.naturality f) } }
   map f := by
     fapply Types.Limit.mk.{v, v}
     · intro j

diff --git a/Mathlib/CategoryTheory/EqToHom.lean b/Mathlib/CategoryTheory/EqToHom.lean
@@ -250,9 +250,6 @@ theorem congr_inv_of_congr_hom (F G : C ⥤ D) {X Y : C} (e : X ≅ Y) (hX : F.o
     Category.assoc]
 #align category_theory.functor.congr_inv_of_congr_hom CategoryTheory.Functor.congr_inv_of_congr_hom
 
-theorem congr_map (F : C ⥤ D) {X Y : C} {f g : X ⟶ Y} (h : f = g) : F.map f = F.map g := by rw [h]
-#align category_theory.functor.congr_map CategoryTheory.Functor.congr_map
-
 section HEq
 
 -- Composition of functors and maps w.r.t. heq

diff --git a/Mathlib/Combinatorics/Quiver/Basic.lean b/Mathlib/Combinatorics/Quiver/Basic.lean
@@ -135,6 +135,10 @@ infixl:60 " ⋙q " => Prefunctor.comp
 /-- Notation for the identity prefunctor on a quiver. -/
 notation "𝟭q" => id
 
+theorem congr_map {U V : Type*} [Quiver U] [Quiver V] (F : U ⥤q V) {X Y : U} {f g : X ⟶ Y}
+    (h : f = g) : F.map f = F.map g := by
+  rw [h]
+
 end Prefunctor
 
 namespace Quiver