theorem
SingularCohomology.exact_kernel_ι_ModuleCat
{R : Type}
[CommRing R]
{A B : ModuleCat R}
(f : A ⟶ B)
:
Categorical exactness of the kernel inclusion in ModuleCat (Section
28 helper for the cup product). For any morphism f : A ⟶ B in
ModuleCat R, the underlying linear-map sequence
kernel.ι f → f is exact in the sense of Function.Exact: the image of
kernel.ι f coincides with the kernel of f. This bridges Mathlib's
categorical kernel.ι with the concrete linear-algebra notion of
exactness used in the cohomology development.