mathlib3

d3684bc3 - feat(category_theory/abelian): constructor in terms of coimage-image comparison (#12972)

feat(category_theory/abelian): constructor in terms of coimage-image comparison (#12972) The "stacks constructor" for an abelian category, following https://stacks.math.columbia.edu/tag/0109. I also factored out the canonical morphism from the abelian coimage to the abelian image (which exists whether or not the category is abelian), and reformulated `abelian.coimage_iso_image` in terms of an `is_iso` instance for this morphism. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>