English
Let f: X' → X be an isomorphism and g: X → Y with kernel. Then the inverse part of kernelSubobjectIsoComp relates the kernel arrows as (kernelSubobjectIsoComp(f,g).inv) ≫ (kernelSubobject (f ≫ g)).arrow = (kernelSubobject g).arrow ≫ (inv f).
Русский
Пусть f: X' → X — изоморфизм и g: X → Y имеет ядро. Тогда инверсиальная часть kernelSubobjectIsoComp связывает вставку ядра: (kernelSubobjectIsoComp(f,g).inv) ≫ (kernelSubobject(f ≫ g)).arrow = (kernelSubobject g).arrow ≫ (inv f).
LaTeX
$$$\left(\mathrm{kernelSubobjectIsoComp}(f,g).\mathrm{inv}\right) \circ \left(\mathrm{kernelSubobject}(f \;\gg\; g).\mathrm{arrow}\right) = \left(\mathrm{kernelSubobject}(g).\mathrm{arrow}\right) \circ (\mathrm{inv} \, f)$$$
Lean4
@[simp]
theorem kernelSubobjectIsoComp_inv_arrow {X' : C} (f : X' ⟶ X) [IsIso f] (g : X ⟶ Y) [HasKernel g] :
(kernelSubobjectIsoComp f g).inv ≫ (kernelSubobject (f ≫ g)).arrow = (kernelSubobject g).arrow ≫ inv f := by
simp [kernelSubobjectIsoComp]
