English
Suppose F, G: C ⥤ D are functors, e: X ≅ Y an isomorphism, and hX, hY witness equalities F.obj X = G.obj X and F.obj Y = G.obj Y. If F.map e.hom equals eqToHom of the construction from hX and hY, then F.map e.inv equals the corresponding conjugate on e.inv.
Русский
Пусть F, G: C ⥤ D — функторы, e: X ≅ Y — изоморфизм, и hX, hY дают равенства F.obj X = G.obj X и F.obj Y = G.obj Y. Если F.map e.hom = eqToHom(из hX, hY), тогда F.map e.inv равно соответствующему сопряжению на e.inv.
LaTeX
$$$ F.map(e.hom) = eqToHom(⋯) \\Rightarrow F.map(e.inv) = eqToHom(⋯) $$$
Lean4
theorem congr_inv_of_congr_hom (F G : C ⥤ D) {X Y : C} (e : X ≅ Y) (hX : F.obj X = G.obj X) (hY : F.obj Y = G.obj Y)
(h₂ : F.map e.hom = eqToHom (by rw [hX]) ≫ G.map e.hom ≫ eqToHom (by rw [hY])) :
F.map e.inv = eqToHom (by rw [hY]) ≫ G.map e.inv ≫ eqToHom (by rw [hX]) := by
simp only [← IsIso.Iso.inv_hom e, Functor.map_inv, h₂, IsIso.inv_comp, inv_eqToHom, Category.assoc]
