feat(category_theory/subobject): kernels and images as subobjects (#6301)
feat(category_theory/subobject): kernels and images as subobjects (#6301)

Further work on subobjects,  building on the initial definition in #6278.

* Add noncomputable functions to obtain representatives of subobjects.
* Realise kernel/equalizer/image as subobjects.



Co-authored-by: Scott Morrison <63f04b4d96235eb042cc46d94f14d241d2a26722@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib