Documentation

Mathlib.CategoryTheory.Abelian.Subobject

Equivalence between subobjects and quotients in an abelian category #

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.

Equations
Instances For
    @[simp]
    theorem CategoryTheory.Abelian.subobjectIsoSubobjectOp_apply {C : Type u} [Category.{v, u} C] [Abelian C] (X : C) (a : Subobject X) :
    (subobjectIsoSubobjectOp X) a = Subobject.lift (fun (x : C) (f : x X) (x_1 : Mono f) => Subobject.mk (Limits.cokernel.π f).op) a

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