English
There is an isomorphism between the categorical kernel ker f and the module-theoretic kernel ker f.hom.
Русский
Существует изоморфизм между категориальным ядром ker f и модульным ядром ker f.hom.
LaTeX
$$$$ \\ker f \\cong_M \\ker(f^{\\mathrm{hom}}) $$$$
Lean4
/-- The categorical kernel of a morphism in `ModuleCat`
agrees with the usual module-theoretical kernel.
-/
noncomputable def kernelIsoKer {G H : ModuleCat.{v} R} (f : G ⟶ H) :
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11036): broken dot notation
kernel f ≅ ModuleCat.of R (LinearMap.ker f.hom) :=
limit.isoLimitCone
⟨_, kernelIsLimit f⟩
-- We now show this isomorphism commutes with the inclusion of the kernel into the source.
