Commit 2022-03-29 18:32 d3684bc3

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.