English
For a functor F: C ⥤ D, an isomorphism α: X ≅ Y, and f ∈ Aut X, the conjAut is preserved by F: F.mapIso (α.conjAut f) = (F.mapIso α).conjAut (F.map f).
Русский
Пусть F: C ⥤ D, α: X ≅ Y и f ∈ Aut X. Тогда сопряжение автоморфизмов сохраняется под F: F.mapIso (α.conjAut f) = (F.mapIso α).conjAut (F.map f).
LaTeX
$$$ \\mathrm{F.mapIso}(\\alpha.\\mathrm{conjAut} f) = (\\mathrm{F.mapIso}\\alpha).\\mathrm{conjAut}(\\mathrm{F.map} f) $$$
Lean4
theorem map_conjAut (F : C ⥤ D) {X Y : C} (α : X ≅ Y) (f : Aut X) :
F.mapIso (α.conjAut f) = (F.mapIso α).conjAut (F.mapIso f) := by ext;
simp only [mapIso_hom, Iso.conjAut_hom, F.map_conj]
-- alternative proof: by simp only [Iso.conjAut_apply, F.mapIso_trans, F.mapIso_symm]
