English
Let f: X' → X be an isomorphism and g: X → Y have a kernel. Then the canonical isomorphism between kernel subobjects coheres with composition, i.e. the kernel arrows satisfy (kernelSubobjectIsoComp(f,g).hom) ∘ (kernelSubobject g).arrow = (kernelSubobject (f ≫ g)).arrow ∘ f.
Русский
Пусть f: X' → X — изоморфизм и g: X → Y имеет ядро. Тогда каноническая изоморфия между подобъектами ядра совместима с композициией: (kernelSubobjectIsoComp(f,g).hom) ∘ (kernelSubobject g).arrow = (kernelSubobject (f ≫ g)).arrow ∘ f.
LaTeX
$$$\left(\mathrm{kernelSubobjectIsoComp}(f,g).\mathrm{hom}\right) \circ \left(\mathrm{kernelSubobject}(g).\mathrm{arrow}\right) = \left(\mathrm{kernelSubobject}(f \;\gg\; g).\mathrm{arrow}\right) \circ f$$$
Lean4
@[simp]
theorem kernelSubobjectIsoComp_hom_arrow {X' : C} (f : X' ⟶ X) [IsIso f] (g : X ⟶ Y) [HasKernel g] :
(kernelSubobjectIsoComp f g).hom ≫ (kernelSubobject g).arrow = (kernelSubobject (f ≫ g)).arrow ≫ f := by
simp [kernelSubobjectIsoComp]
