feat: transfer Functor.Final across natural isomorphisms (#6232)

Mathlib/CategoryTheory/Comma.lean

@@ -239,6 +239,20 @@ def mapLeftComp (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃) :
           right := 𝟙 _ } }
 #align category_theory.comma.map_left_comp CategoryTheory.Comma.mapLeftComp
 
+/-- Two equal natural transformations `L₁ ⟶ L₂` yield naturally isomorphic functors
+    `Comma L₁ R ⥤ Comma L₂ R`. -/
+@[simps!]
+def mapLeftEq (l l' : L₁ ⟶ L₂) (h : l = l') : mapLeft R l ≅ mapLeft R l' :=
+  NatIso.ofComponents (fun X => isoMk (Iso.refl _) (Iso.refl _) (by aesop_cat)) (by aesop_cat)
+
+/-- A natural isomorphism `L₁ ≅ L₂` induces an equivalence of categories
+    `Comma L₁ R ≌ Comma L₂ R`. -/
+@[simps!]
+def mapLeftIso (i : L₁ ≅ L₂) : Comma L₁ R ≌ Comma L₂ R :=
+  Equivalence.mk (mapLeft _ i.inv) (mapLeft _ i.hom)
+    ((mapLeftId _ _).symm ≪≫ mapLeftEq _ _ _ i.hom_inv_id.symm ≪≫ mapLeftComp _ _ _)
+    ((mapLeftComp _ _ _).symm ≪≫ mapLeftEq _ _ _ i.inv_hom_id ≪≫ mapLeftId _ _)
+
 /-- A natural transformation `R₁ ⟶ R₂` induces a functor `Comma L R₁ ⥤ Comma L R₂`. -/
 @[simps]
 def mapRight (r : R₁ ⟶ R₂) : Comma L R₁ ⥤ Comma L R₂ where
@@ -281,6 +295,20 @@ def mapRightComp (r : R₁ ⟶ R₂) (r' : R₂ ⟶ R₃) :
           right := 𝟙 _ } }
 #align category_theory.comma.map_right_comp CategoryTheory.Comma.mapRightComp
 
+/-- Two equal natural transformations `R₁ ⟶ R₂` yield naturally isomorphic functors
+    `Comma L R₁ ⥤ Comma L R₂`. -/
+@[simps!]
+def mapRightEq (r r' : R₁ ⟶ R₂) (h : r = r') : mapRight L r ≅ mapRight L r' :=
+  NatIso.ofComponents (fun X => isoMk (Iso.refl _) (Iso.refl _) (by aesop_cat)) (by aesop_cat)
+
+/-- A natural isomorphism `R₁ ≅ R₂` induces an equivalence of categories
+    `Comma L R₁ ≌ Comma L R₂`. -/
+@[simps!]
+def mapRightIso (i : R₁ ≅ R₂) : Comma L R₁ ≌ Comma L R₂ :=
+  Equivalence.mk (mapRight _ i.hom) (mapRight _ i.inv)
+    ((mapRightId _ _).symm ≪≫ mapRightEq _ _ _ i.hom_inv_id.symm ≪≫ mapRightComp _ _ _)
+    ((mapRightComp _ _ _).symm ≪≫ mapRightEq _ _ _ i.inv_hom_id ≪≫ mapRightId _ _)
+
 end
 
 section

Mathlib/CategoryTheory/Limits/Final.lean

@@ -157,6 +157,12 @@ instance (priority := 100) initial_of_isLeftAdjoint (F : C ⥤ D) [h : IsLeftAdj
   initial_of_adjunction h.adj
 #align category_theory.functor.initial_of_is_left_adjoint CategoryTheory.Functor.initial_of_isLeftAdjoint
 
+theorem final_of_natIso {F F' : C ⥤ D} [Final F] (i : F ≅ F') : Final F' where
+  out _ := isConnected_of_equivalent (StructuredArrow.mapNatIso i)
+
+theorem initial_of_natIso {F F' : C ⥤ D} [Initial F] (i : F ≅ F') : Initial F' where
+  out _ := isConnected_of_equivalent (CostructuredArrow.mapNatIso i)
+
 namespace Final
 
 variable (F : C ⥤ D) [Final F]

Mathlib/CategoryTheory/StructuredArrow.lean

@@ -49,7 +49,7 @@ def proj (S : D) (T : C ⥤ D) : StructuredArrow S T ⥤ C :=
   Comma.snd _ _
 #align category_theory.structured_arrow.proj CategoryTheory.StructuredArrow.proj
 
-variable {S S' S'' : D} {Y Y' : C} {T : C ⥤ D}
+variable {S S' S'' : D} {Y Y' : C} {T T' : C ⥤ D}
 
 -- porting note: this lemma was added because `Comma.hom_ext`
 -- was not triggered automatically
@@ -216,6 +216,17 @@ theorem map_comp {f : S ⟶ S'} {f' : S' ⟶ S''} {h : StructuredArrow S'' T} :
   simp
 #align category_theory.structured_arrow.map_comp CategoryTheory.StructuredArrow.map_comp
 
+/-- An isomorphism `S ≅ S'` induces an equivalence `StructuredArrow S T ≌ StructuredArrow S' T`. -/
+@[simp]
+def mapIso (i : S ≅ S') : StructuredArrow S T ≌ StructuredArrow S' T :=
+  Comma.mapLeftIso _ ((Functor.const _).mapIso i)
+
+/-- A natural isomorphism `T ≅ T'` induces an equivalence
+    `StructuredArrow S T ≌ StructuredArrow S T'`.-/
+@[simp]
+def mapNatIso (i : T ≅ T') : StructuredArrow S T ≌ StructuredArrow S T' :=
+  Comma.mapRightIso _ i
+
 instance proj_reflectsIsomorphisms : ReflectsIsomorphisms (proj S T) where
   reflects {Y Z} f t :=
     ⟨⟨StructuredArrow.homMk
@@ -309,7 +320,7 @@ def proj (S : C ⥤ D) (T : D) : CostructuredArrow S T ⥤ C :=
   Comma.fst _ _
 #align category_theory.costructured_arrow.proj CategoryTheory.CostructuredArrow.proj
 
-variable {T T' T'' : D} {Y Y' : C} {S : C ⥤ D}
+variable {T T' T'' : D} {Y Y' : C} {S S' : C ⥤ D}
 
 -- porting note: this lemma was added because `Comma.hom_ext`
 -- was not triggered automatically
@@ -468,6 +479,18 @@ theorem map_comp {f : T ⟶ T'} {f' : T' ⟶ T''} {h : CostructuredArrow S T} :
   simp
 #align category_theory.costructured_arrow.map_comp CategoryTheory.CostructuredArrow.map_comp
 
+/-- An isomorphism `T ≅ T'` induces an equivalence
+    `CostructuredArrow S T ≌ CostructuredArrow S T'`. -/
+@[simp]
+def mapIso (i : T ≅ T') : CostructuredArrow S T ≌ CostructuredArrow S T' :=
+  Comma.mapRightIso _ ((Functor.const _).mapIso i)
+
+/-- A natural isomorphism `S ≅ S'` induces an equivalence
+    `CostrucutredArrow S T ≌ CostructuredArrow S' T`. -/
+@[simp]
+def mapNatIso (i : S ≅ S') : CostructuredArrow S T ≌ CostructuredArrow S' T :=
+  Comma.mapLeftIso _ i
+
 instance proj_reflectsIsomorphisms : ReflectsIsomorphisms (proj S T) where
   reflects {Y Z} f t :=
     ⟨⟨CostructuredArrow.homMk