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