English
If F, G: C ⥤ D are functors, e: X ≅ Y an isomorphism, and equalities hX, hY hold between F.obj and G.obj, then F.map e.inv equals the corresponding eqToHom compositions with G.map e.inv.
Русский
Если F, G: C ⥤ D — функторы, e: X ≅ Y — изоморфизм, и существуют равенства hX, hY между F.obj и G.obj, то F.map e.inv равно соответствующим композициям eqToHom с G.map e.inv.
LaTeX
$$$ F.map(e^{-1}) = eqToHom(·) \\circ G.map(e^{-1}) \\circ eqToHom(·) $$$
Lean4
/-- This is not always a good idea as a `@[simp]` lemma,
as we lose the ability to use results that interact with `F`,
e.g. the naturality of a natural transformation.
In some files it may be appropriate to use `attribute [local simp] eqToHom_map`, however.
-/
theorem eqToHom_map (F : C ⥤ D) {X Y : C} (p : X = Y) : F.map (eqToHom p) = eqToHom (congr_arg F.obj p) := by cases p;
simp
