English
For functors F,G : C ⥤ D and a natural transformation α : F ⟶ G, and any isomorphism e: X ≅ Y in C, the component maps α.app X and α.app Y are isomorphic in D exactly when each other is so: IsIso(α.X) ↔ IsIso(α.Y).
Русский
Для функторов F,G : C ⥤ D и естественного преобразования α : F ⟶ G, и для любого изоморфизма e: X ≅ Y в C, компонентные отображения α.app X и α.app Y являются изоморфными в D тогда и только тогда, когда они взаимно изоморфны.
LaTeX
$$$\\forall {F,G: C \\to D}\\, (\\alpha: F \\to G)\\; {\\forall X,Y: C}\\; (e: X \\cong Y)\\; \\big( \\text{IsIso}(\\alpha.app X) \\iff \\text{IsIso}(\\alpha.app Y) \\big)$$$
Lean4
theorem isIso_app_iff_of_iso {F G : C ⥤ D} (α : F ⟶ G) {X Y : C} (e : X ≅ Y) : IsIso (α.app X) ↔ IsIso (α.app Y) :=
(MorphismProperty.isomorphisms D).arrow_mk_iso_iff (Arrow.isoMk (F.mapIso e) (G.mapIso e) (by simp))
