mathlib3 documentation


Equivalence between subobjects and quotients in an abelian category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In an abelian category, the subobjects and quotient objects of an object X are order-isomorphic via taking kernels and cokernels. Implemented here using subobjects in the opposite category, since mathlib does not have a notion of quotient objects at the time of writing.

@[protected, instance]

A well-powered abelian category is also well-copowered.