mathlib3 documentation

category_theory.subobject.limits

Specific subobjects #

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

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

@[reducible]

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.

Equations
@[reducible]

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.

Equations
Instances for category_theory.limits.factor_thru_kernel_subobject
@[reducible]

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

The underlying object of image_subobject f is (up to isomorphism!) the same as the chosen object image f.

Equations

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

@[protected, instance]

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.