English
In an abelian category, the morphism from the image of g^{op} to the kernel of f^{op} obtained by the standard image-to-kernel construction equals a canonical composite built from the image and kernel subobject isomorphisms and the cokernel/kernel factorisations of f and g under op.
Русский
В абелевой категории каноническое отображение из образа g^{op} в ядро f^{op} через стандартное преобразование образ-ядро равняется конкретной композиции через соответствующие изоморфизмы образа и ядра и факторизации черезнор.
LaTeX
$$$\\operatorname{imageToKernel} g^{op} f^{op} = \\bigl(\\operatorname{imageSubobjectIso} _ \\xrightarrow{\\simeq} (\\operatorname{imageOpOp} g)^{op}\\bigr) \\cdot \\bigl(\\operatorname{cokernel.desc} f (\\operatorname{factorThruImage} g) \\bigr)^{op} \\cdot \\bigl(\\operatorname{kernelSubobjectIso} _ \\xrightarrow{\\simeq} \\operatorname{kernelOpOp} f\\bigr)^{-1} \\, .$$$$
Lean4
theorem imageToKernel_op {X Y Z : V} (f : X ⟶ Y) (g : Y ⟶ Z) (w : f ≫ g = 0) :
imageToKernel g.op f.op (by rw [← op_comp, w, op_zero]) =
(imageSubobjectIso _ ≪≫ (imageOpOp _).symm).hom ≫
(cokernel.desc f (factorThruImage g)
(by rw [← cancel_mono (image.ι g), Category.assoc, image.fac, w, zero_comp])).op ≫
(kernelSubobjectIso _ ≪≫ kernelOpOp _).inv :=
by
ext
simp only [Iso.trans_hom, Iso.symm_hom, Iso.trans_inv, kernelOpOp_inv, Category.assoc, imageToKernel_arrow,
kernelSubobject_arrow', kernel.lift_ι, ← op_comp, cokernel.π_desc, ← imageSubobject_arrow,
← imageUnopOp_inv_comp_op_factorThruImage g.op]
rfl
