English
If G ≅ G' are naturally isomorphic functors, there is a natural equivalence between Hom-sets (X → G.obj Y) and (X → G'.obj Y) given by composing on the right with the isomorphism.
Русский
Если G и G' естественно изоморфны, существует естественное эквивалентное соответствие между множествами гомоморфизмов (X → G.obj Y) и (X → G'.obj Y), задаваемое композициями справа с изоморфизмом.
LaTeX
$$$\text{equivHomsetRightOfNatIso } {G G'} (iso : G \cong G') {X} {Y} : (X \to G.obj Y) \simeq (X \to G'.obj Y)$, с отображениями $f \mapsto f \circ iso.hom.app _$ и $g \mapsto g \circ iso.inv.app _$.$$
Lean4
/-- If G and H are naturally isomorphic functors, establish an equivalence of hom-sets. -/
@[simps]
def equivHomsetRightOfNatIso {G G' : D ⥤ C} (iso : G ≅ G') {X : C} {Y : D} : (X ⟶ G.obj Y) ≃ (X ⟶ G'.obj Y)
where
toFun f := f ≫ iso.hom.app _
invFun g := g ≫ iso.inv.app _
left_inv f := by simp
right_inv g := by simp
