English
For a natural transformation α: F ⇒ G in Fun(C,D) with D abelian, the app component at X satisfies a specific composition identity involving coimageObjIso α X and imageObjIso α X.
Русский
Для натурального преобразования α: F ⇒ G в категорию-функторов, где D абелевана, компонентa α.app X удовлетворяет определённому тождеству композиции, включающему coimageObjIso α X и imageObjIso α X.
LaTeX
$$$\mathrm{coimageImageComparison}(\alpha).\mathrm{app} X = (\mathrm{coimageObjIso}(\alpha,X)).\mathrm{inv} \,\circ \, (\mathrm{coimageImageComparison}(\alpha)).\mathrm{app}X \circ (\mathrm{imageObjIso}(\alpha,X)).\mathrm{hom}$$$
Lean4
theorem coimageImageComparison_app :
coimageImageComparison (α.app X) =
(coimageObjIso α X).inv ≫ (coimageImageComparison α).app X ≫ (imageObjIso α X).hom :=
by
ext
dsimp
dsimp [imageObjIso, coimageObjIso, cokernel.map]
simp only [coimage_image_factorisation, PreservesKernel.iso_hom, Category.assoc, kernel.lift_ι, Category.comp_id,
PreservesCokernel.iso_inv, cokernel.π_desc_assoc, Category.id_comp]
erw [kernelComparison_comp_ι _ ((evaluation C D).obj X)]
erw [π_comp_cokernelComparison_assoc _ ((evaluation C D).obj X)]
conv_lhs => rw [← coimage_image_factorisation α]
rfl
