feat(category_theory): nat_trans.equiv_of_comp_fully_faithful (#17304)

If `H` is a fully faithful functor, there are bijections `(F ⟶ G) ≃ (F ⋙ H ⟶ G ⋙ H)` and `(F ≅ G) ≃ (F ⋙ H ≅ G ⋙ H)`.

src/category_theory/functor/fully_faithful.lean

@@ -171,6 +171,24 @@ lemma nat_iso_of_comp_fully_faithful_inv (i : F ⋙ H ≅ G ⋙ H) :
   (nat_iso_of_comp_fully_faithful H i).inv = nat_trans_of_comp_fully_faithful H i.inv :=
 by { ext, simp [←preimage_comp], dsimp, simp, }
 
+/-- Horizontal composition with a fully faithful functor induces a bijection on
+natural transformations. -/
+@[simps]
+def nat_trans.equiv_of_comp_fully_faithful : (F ⟶ G) ≃ (F ⋙ H ⟶ G ⋙ H) :=
+{ to_fun := λ α, α ◫ 𝟙 H,
+  inv_fun := nat_trans_of_comp_fully_faithful H,
+  left_inv := by tidy,
+  right_inv := by tidy, }
+
+/-- Horizontal composition with a fully faithful functor induces a bijection on
+natural isomorphisms. -/
+@[simps]
+def nat_iso.equiv_of_comp_fully_faithful : (F ≅ G) ≃ (F ⋙ H ≅ G ⋙ H) :=
+{ to_fun := λ e, nat_iso.hcomp e (iso.refl H),
+  inv_fun := nat_iso_of_comp_fully_faithful H,
+  left_inv := by tidy,
+  right_inv := by tidy, }
+
 end
 
 end category_theory

src/category_theory/natural_isomorphism.lean

@@ -188,6 +188,7 @@ lemma is_iso_of_is_iso_app (α : F ⟶ G) [∀ X : C, is_iso (α.app X)] : is_is
 ⟨(is_iso.of_iso (of_components (λ X, as_iso (α.app X)) (by tidy))).1⟩
 
 /-- Horizontal composition of natural isomorphisms. -/
+@[simps]
 def hcomp {F G : C ⥤ D} {H I : D ⥤ E} (α : F ≅ G) (β : H ≅ I) : F ⋙ H ≅ G ⋙ I :=
 begin
   refine ⟨α.hom ◫ β.hom, α.inv ◫ β.inv, _, _⟩,