English
There is a natural isomorphism between kernelSubobject (f ≫ g) and kernelSubobject g when f is an isomorphism; this isomorphism is compatible with the kernelSubobjectIso and kernelIsIso components.
Русский
Существует естественный изоморфизм kernelSubobject (f ≫ g) ≅ kernelSubobject g при том, что f — изоморфизм; изоморфизм согласуется с компонентами kernelSubobjectIso и kernelIsIso.
LaTeX
$$$${X' }\\!\\!\\; (f:\\; X' \\to X) \\text{IsIso} \\Rightarrow (kernelSubobject (f \\!\\gg g) : C) \\cong (kernelSubobject g : C) $$$$
Lean4
/-- The isomorphism between the kernel of `f ≫ g` and the kernel of `g`,
when `f` is an isomorphism.
-/
def kernelSubobjectIsoComp {X' : C} (f : X' ⟶ X) [IsIso f] (g : X ⟶ Y) [HasKernel g] :
(kernelSubobject (f ≫ g) : C) ≅ (kernelSubobject g : C) :=
kernelSubobjectIso _ ≪≫ kernelIsIsoComp f g ≪≫ (kernelSubobjectIso _).symm
