Documentation

Mathlib.CategoryTheory.Subobject.Limits

Specific subobjects #

We define equalizerSubobject, kernelSubobject and imageSubobject, 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 (imageSubobject f).Factors h

@[inline, reducible]

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

Instances For

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

    Instances For
      @[inline, reducible]

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

      Instances For

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

        Instances For

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

          Instances For

            A commuting square induces a morphism between the kernel subobjects.

            Instances For

              The isomorphism between the kernel of f ≫ g and the kernel of g, when f is an isomorphism.

              Instances For

                Taking cokernels is an order-reversing map from the subobjects of X to the quotient objects of X.

                Instances For

                  Taking kernels is an order-reversing map from the quotient objects of X to the subobjects of X.

                  Instances For
                    @[inline, reducible]

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

                    Instances For

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

                      Instances For

                        A factorisation of f : X ⟶ Y through imageSubobject f.

                        Instances For

                          Postcomposing by an isomorphism gives an isomorphism between image subobjects.

                          Instances For

                            Given a commutative square between morphisms f and g, we have a morphism in the category from imageSubobject f to imageSubobject g.

                            Instances For