Commit 2025-06-09 15:16 d9ad6f7f

feat(CategoryTheory.Abelian.Images, CategoryTheory.Limits.Preserves.Shapes.AbelianImages): minimize hypotheses (#25185) Minimize the hypotheses needed for the definition of Abelian.image, Abelian.Coimage and the definitions associated to them, as well as for PreservesImage.iso and PreservesCoimage.iso (the isomorphisms expressing that a functor commutes with images/coimages). Basically, just replace the HasKernels/HasCokernels instances by instances involving only the precise kernels/cokernels that are needed. (This is useful for one of my projects, where I don't yet know that all kernels exist.)