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

@[reducible, inline]

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

Equations
Instances For

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

    Equations
    Instances For
      theorem CategoryTheory.Limits.equalizerSubobject_factors {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X Y) [HasEqualizer f g] {W : C} (h : W X) (w : CategoryStruct.comp h f = CategoryStruct.comp h g) :
      (equalizerSubobject f g).Factors h
      @[reducible, inline]

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

      Equations
      Instances For

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

        Equations
        Instances For
          @[simp]
          @[simp]
          theorem CategoryTheory.Limits.kernelSubobject_arrow'_apply {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] (f : X Y) [HasKernel f] [inst : HasForget C] (x : (forget C).obj (kernel f)) :
          (kernelSubobject f).arrow ((kernelSubobjectIso f).inv x) = (kernel.ι f) x
          @[simp]
          theorem CategoryTheory.Limits.kernelSubobject_arrow_comp_apply {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] (f : X Y) [HasKernel f] [inst : HasForget C] (x : (forget C).obj (Subobject.underlying.obj (kernelSubobject f))) :
          f ((kernelSubobject f).arrow x) = 0 x
          theorem CategoryTheory.Limits.kernelSubobject_factors {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] (f : X Y) [HasKernel f] {W : C} (h : W X) (w : CategoryStruct.comp h f = 0) :
          (kernelSubobject f).Factors h
          theorem CategoryTheory.Limits.kernelSubobject_factors_iff {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] (f : X Y) [HasKernel f] {W : C} (h : W X) :

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

          Equations
          Instances For

            A commuting square induces a morphism between the kernel subobjects.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem CategoryTheory.Limits.kernelSubobjectMap_arrow {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] {f : X Y} [HasKernel f] {X' Y' : C} {f' : X' Y'} [HasKernel f'] (sq : Arrow.mk f Arrow.mk f') :
              @[simp]
              @[simp]
              theorem CategoryTheory.Limits.kernelSubobjectMap_arrow_apply {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] {f : X Y} [HasKernel f] {X' Y' : C} {f' : X' Y'} [HasKernel f'] (sq : Arrow.mk f Arrow.mk f') [inst : HasForget C] (x : (forget C).obj (Subobject.underlying.obj (kernelSubobject f))) :
              (kernelSubobject f').arrow ((kernelSubobjectMap sq) x) = sq.left ((kernelSubobject f).arrow x)
              @[simp]
              theorem CategoryTheory.Limits.kernelSubobjectMap_comp {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] {f : X Y} [HasKernel f] {X' Y' : C} {f' : X' Y'} [HasKernel f'] {X'' Y'' : C} {f'' : X'' Y''} [HasKernel f''] (sq : Arrow.mk f Arrow.mk f') (sq' : Arrow.mk f' Arrow.mk f'') :

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

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

                @[simp]

                Postcomposing by a monomorphism does not change the kernel subobject.

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

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem CategoryTheory.Limits.cokernelOrderHom_coe {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasCokernels C] (X : C) (a✝ : Subobject X) :
                  (cokernelOrderHom X) a✝ = Subobject.lift (fun (x : C) (f : x X) (x_1 : Mono f) => Subobject.mk (cokernel.π f).op) a✝

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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem CategoryTheory.Limits.kernelOrderHom_coe {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasKernels C] (X : C) (a✝ : Subobject (Opposite.op X)) :
                    (kernelOrderHom X) a✝ = Subobject.lift (fun (x : Cᵒᵖ) (f : x Opposite.op X) (x_1 : Mono f) => Subobject.mk (kernel.ι f.unop)) a✝
                    @[reducible, inline]
                    abbrev CategoryTheory.Limits.imageSubobject {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) [HasImage f] :

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

                    Equations
                    Instances For

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

                      Equations
                      Instances For
                        @[simp]
                        theorem CategoryTheory.Limits.imageSubobject_arrow_comp_apply {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) [HasImage f] [inst : HasForget C] (x : (forget C).obj X) :
                        theorem CategoryTheory.Limits.imageSubobject_factors_comp_self {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) [HasImage f] {W : C} (k : W X) :

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

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

                        Postcomposing by an isomorphism gives an isomorphism between image subobjects.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          Precomposing by an isomorphism does not change the image subobject.

                          theorem CategoryTheory.Limits.imageSubobject_le {C : Type u} [Category.{v, u} C] {A B : C} {X : Subobject B} (f : A B) [HasImage f] (h : A Subobject.underlying.obj X) (w : CategoryStruct.comp h X.arrow = f) :
                          theorem CategoryTheory.Limits.imageSubobject_le_mk {C : Type u} [Category.{v, u} C] {A B X : C} (g : X B) [Mono g] (f : A B) [HasImage f] (h : A X) (w : CategoryStruct.comp h g = f) :

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

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]