From cba2f37b0a101c57e2e976fa3b29a87c41e49268 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Calle=20S=C3=B6nne?= Date: Wed, 24 Apr 2024 19:18:10 +0000 Subject: [PATCH] feat(CategoryTheory/EqToHom): generalize Functor.congr_map to Prefunctor.congr_map (#12384) --- Mathlib/CategoryTheory/Category/Cat/Limit.lean | 2 +- Mathlib/CategoryTheory/EqToHom.lean | 3 --- Mathlib/Combinatorics/Quiver/Basic.lean | 4 ++++ 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/Mathlib/CategoryTheory/Category/Cat/Limit.lean b/Mathlib/CategoryTheory/Category/Cat/Limit.lean index 57c2e1eb6137d..7e7c336d3907e 100644 --- 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 index 2ba66d8ca9700..02713bf3e88ec 100644 --- 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 index a5479c2228b5b..4c5943253855d 100644 --- 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