English
The imageToKernel map composes with the kernelArrow to yield the imageArrow: imageToKernel f g w ≫ kernelSubobject g .arrow = imageSubobject f .arrow.
Русский
Образово-ядровый переход совместим с образной стрелкой: imageToKernel f g w ≫ kernelSubobject g .arrow = imageSubobject f .arrow.
LaTeX
$$$\text{imageToKernel}(f,g,w) \;≪≫\; \text{kernelSubobject}(g).arrow = \text{imageSubobject}(f).arrow$$$
Lean4
@[reassoc (attr := simp), elementwise (attr := simp)]
theorem imageToKernel_arrow (w : f ≫ g = 0) :
imageToKernel f g w ≫ (kernelSubobject g).arrow = (imageSubobject f).arrow := by
simp [imageToKernel]
-- This is less useful as a `simp` lemma than it initially appears,
-- as it "loses" the information the morphism factors through the image.
