mathlib documentation


Specific subobjects #

We define equalizer_subobject, kernel_subobject and image_subobject, which are the subobjects represented by the equalizer, kernel and image of (a pair of) morphism(s) and provide conditions for P.factors f, where P is one of these special subobjects.

TODO: Add conditions for when P is a pullback subobject. TODO: an iff characterisation of (image_subobject f).factors h

The equalizer of morphisms f g : X ⟶ Y as a subobject X.

The underlying object of equalizer_subobject f g is (up to isomorphism!) the same as the chosen object equalizer f g.


The kernel of a morphism f : X ⟶ Y as a subobject X.

A factorisation of h : W ⟶ X through kernel_subobject f, assuming h ≫ f = 0.


Postcomposing by an monomorphism does not change the kernel subobject.

The image of a morphism f g : X ⟶ Y as a subobject Y.

The image of h ≫ f is always a smaller subobject than the image of f.


The morphism image_subobject (h ≫ f) ⟶ image_subobject f is an epimorphism when h is an epimorphism. In general this does not imply that image_subobject (h ≫ f) = image_subobject f, although it will when the ambient category is abelian.