English
In an abelian category, the image-to-kernel morphism for unop is identified with a canonical composite obtained from imageSubobject/unop and cokernel/kernel factorizations in the unop setting.
Русский
В абелевой категории отображение образ-ядро для unop идентифицируется с канонической композицией через подобразообразование/unop и факторизацию через кокернел/ядро в установке unop.
LaTeX
$$$\\operatorname{imageToKernel} g.unop f.unop = \\bigl(\\operatorname{imageSubobjectIso} g.unop \\circ (\\operatorname{imageUnopUnop} g)^{-1}\\bigr) \\circ \\bigl(\\operatorname{cokernel.desc} f (\\operatorname{factorThruImage} g)\\bigr)^{unop} \\circ \\bigl(\\operatorname{kernelSubobjectIso} f.unop \\circ (\\operatorname{kernelUnopUnop} f)^{-1}\\bigr)$$$
Lean4
theorem imageToKernel_unop {X Y Z : Vᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) (w : f ≫ g = 0) :
imageToKernel g.unop f.unop (by rw [← unop_comp, w, unop_zero]) =
(imageSubobjectIso _ ≪≫ (imageUnopUnop _).symm).hom ≫
(cokernel.desc f (factorThruImage g)
(by rw [← cancel_mono (image.ι g), Category.assoc, image.fac, w, zero_comp])).unop ≫
(kernelSubobjectIso _ ≪≫ kernelUnopUnop _).inv :=
by
ext
dsimp only [imageUnopUnop]
simp only [Iso.trans_hom, Iso.symm_hom, Iso.trans_inv, kernelUnopUnop_inv, Category.assoc, imageToKernel_arrow,
kernelSubobject_arrow', kernel.lift_ι, cokernel.π_desc, Iso.unop_inv, ← unop_comp,
factorThruImage_comp_imageUnopOp_inv, Quiver.Hom.unop_op, imageSubobject_arrow]
