Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-29 18:32 d3684bc3

View on Github →

feat(category_theory/abelian): constructor in terms of coimage-image comparison (#12972) The "stacks constructor" for an abelian category, following 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.

Estimated changes