English
Let f: A → B and g: B → C with f ∘ g = 0 in a category with kernels and images. Then the canonical map from the image of f to the kernel of g is compatible with the natural isomorphisms relating images and kernels, i.e., a certain square commutes.
Русский
Пусть f: A → B и g: B → C удовлетворяют f ∘ g = 0 в категории, где существуют образы и ядра. Тогда каноническое отображение от образа f к ядру g согласуется с естественными изоморфизмами образа и ядра, то есть диаграмма коммутирует.
LaTeX
$$$(\\text{imageSubobjectIso } f).hom \\; \\circ \\; \\text{imageToKernel}'\; f\; g\; w = \\text{imageToKernel } f\; g\; w \\; \\circ \\; (\\text{kernelSubobjectIso } g).hom$$$
Lean4
@[simp]
theorem imageSubobjectIso_imageToKernel' (w : f ≫ g = 0) :
(imageSubobjectIso f).hom ≫ imageToKernel' f g w = imageToKernel f g w ≫ (kernelSubobjectIso g).hom :=
by
ext
simp [imageToKernel']
