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

source
@[reducible, inline]
abbrev CategoryTheory.Limits.equalizerSubobject {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] :
Subobject X

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

Equations
Instances For
    source
    def CategoryTheory.Limits.equalizerSubobjectIso {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] :
    Subobject.underlying.obj (equalizerSubobject f g) ≅ equalizer f g

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

    Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Limits.equalizerSubobject_arrow {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] :
      CategoryStruct.comp (equalizerSubobjectIso f g).hom (equalizer.ι f g) = (equalizerSubobject f g).arrow
      source
      @[simp]
      theorem CategoryTheory.Limits.equalizerSubobject_arrow_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] {Z : C} (h : X ⟶ Z) :
      CategoryStruct.comp (equalizerSubobjectIso f g).hom (CategoryStruct.comp (equalizer.ι f g) h) = CategoryStruct.comp (equalizerSubobject f g).arrow h
      source
      @[simp]
      theorem CategoryTheory.Limits.equalizerSubobject_arrow' {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] :
      CategoryStruct.comp (equalizerSubobjectIso f g).inv (equalizerSubobject f g).arrow = equalizer.ι f g
      source
      @[simp]
      theorem CategoryTheory.Limits.equalizerSubobject_arrow'_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] {Z : C} (h : X ⟶ Z) :
      CategoryStruct.comp (equalizerSubobjectIso f g).inv (CategoryStruct.comp (equalizerSubobject f g).arrow h) = CategoryStruct.comp (equalizer.ι f g) h
      source
      theorem CategoryTheory.Limits.equalizerSubobject_arrow_comp {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] :
      CategoryStruct.comp (equalizerSubobject f g).arrow f = CategoryStruct.comp (equalizerSubobject f g).arrow g
      source
      theorem CategoryTheory.Limits.equalizerSubobject_arrow_comp_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] {Z : C} (h : Y ⟶ Z) :
      CategoryStruct.comp (equalizerSubobject f g).arrow (CategoryStruct.comp f h) = CategoryStruct.comp (equalizerSubobject f g).arrow (CategoryStruct.comp g h)
      source
      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
      source
      theorem CategoryTheory.Limits.equalizerSubobject_factors_iff {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] {W : C} (h : W ⟶ X) :
      (equalizerSubobject f g).Factors h ↔ CategoryStruct.comp h f = CategoryStruct.comp h g
      source
      @[reducible, inline]
      abbrev CategoryTheory.Limits.kernelSubobject {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] (f : X ⟶ Y) [HasKernel f] :
      Subobject X

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

      Equations
      Instances For
        source
        def CategoryTheory.Limits.kernelSubobjectIso {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] (f : X ⟶ Y) [HasKernel f] :
        Subobject.underlying.obj (kernelSubobject f) ≅ kernel f

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

        Equations
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Limits.kernelSubobject_arrow {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] (f : X ⟶ Y) [HasKernel f] :
          CategoryStruct.comp (kernelSubobjectIso f).hom (kernel.ι f) = (kernelSubobject f).arrow
          source
          @[simp]
          theorem CategoryTheory.Limits.kernelSubobject_arrow_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] (f : X ⟶ Y) [HasKernel f] {Z : C} (h : X ⟶ Z) :
          CategoryStruct.comp (kernelSubobjectIso f).hom (CategoryStruct.comp (kernel.ι f) h) = CategoryStruct.comp (kernelSubobject f).arrow h
          source
          @[simp]
          theorem CategoryTheory.Limits.kernelSubobject_arrow_apply {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] (f : X ⟶ Y) [HasKernel f] {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : ConcreteCategory C F] (x : ToType (Subobject.underlying.obj (kernelSubobject f))) :
          (ConcreteCategory.hom (kernel.ι f)) ((ConcreteCategory.hom (kernelSubobjectIso f).hom) x) = (ConcreteCategory.hom (kernelSubobject f).arrow) x
          source
          @[simp]
          theorem CategoryTheory.Limits.kernelSubobject_arrow' {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] (f : X ⟶ Y) [HasKernel f] :
          CategoryStruct.comp (kernelSubobjectIso f).inv (kernelSubobject f).arrow = kernel.ι f
          source
          @[simp]
          theorem CategoryTheory.Limits.kernelSubobject_arrow'_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] (f : X ⟶ Y) [HasKernel f] {Z : C} (h : X ⟶ Z) :
          CategoryStruct.comp (kernelSubobjectIso f).inv (CategoryStruct.comp (kernelSubobject f).arrow h) = CategoryStruct.comp (kernel.ι f) h
          source
          @[simp]
          theorem CategoryTheory.Limits.kernelSubobject_arrow'_apply {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] (f : X ⟶ Y) [HasKernel f] {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : ConcreteCategory C F] (x : ToType (kernel f)) :
          (ConcreteCategory.hom (kernelSubobject f).arrow) ((ConcreteCategory.hom (kernelSubobjectIso f).inv) x) = (ConcreteCategory.hom (kernel.ι f)) x
          source
          @[simp]
          theorem CategoryTheory.Limits.kernelSubobject_arrow_comp {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] (f : X ⟶ Y) [HasKernel f] :
          CategoryStruct.comp (kernelSubobject f).arrow f = 0
          source
          @[simp]
          theorem CategoryTheory.Limits.kernelSubobject_arrow_comp_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] (f : X ⟶ Y) [HasKernel f] {Z : C} (h : Y ⟶ Z) :
          CategoryStruct.comp (kernelSubobject f).arrow (CategoryStruct.comp f h) = CategoryStruct.comp 0 h
          source
          @[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] {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : ConcreteCategory C F] (x : ToType (Subobject.underlying.obj (kernelSubobject f))) :
          (ConcreteCategory.hom f) ((ConcreteCategory.hom (kernelSubobject f).arrow) x) = (ConcreteCategory.hom 0) x
          source
          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
          source
          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) :
          (kernelSubobject f).Factors h ↔ CategoryStruct.comp h f = 0
          source
          def CategoryTheory.Limits.factorThruKernelSubobject {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) :
          W ⟶ Subobject.underlying.obj (kernelSubobject f)

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

          Equations
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Limits.factorThruKernelSubobject_comp_arrow {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) :
            CategoryStruct.comp (factorThruKernelSubobject f h w) (kernelSubobject f).arrow = h
            source
            @[simp]
            theorem CategoryTheory.Limits.factorThruKernelSubobject_comp_kernelSubobjectIso {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) :
            CategoryStruct.comp (factorThruKernelSubobject f h w) (kernelSubobjectIso f).hom = kernel.lift f h w
            source
            def CategoryTheory.Limits.kernelSubobjectMap {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') :
            Subobject.underlying.obj (kernelSubobject f) ⟶ Subobject.underlying.obj (kernelSubobject f')

            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
              source
              @[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') :
              CategoryStruct.comp (kernelSubobjectMap sq) (kernelSubobject f').arrow = CategoryStruct.comp (kernelSubobject f).arrow sq.left
              source
              @[simp]
              theorem CategoryTheory.Limits.kernelSubobjectMap_arrow_assoc {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') {Z : C} (h : X' ⟶ Z) :
              CategoryStruct.comp (kernelSubobjectMap sq) (CategoryStruct.comp (kernelSubobject f').arrow h) = CategoryStruct.comp (kernelSubobject f).arrow (CategoryStruct.comp sq.left h)
              source
              @[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') {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : ConcreteCategory C F] (x : ToType (Subobject.underlying.obj (kernelSubobject f))) :
              (ConcreteCategory.hom (kernelSubobject f').arrow) ((ConcreteCategory.hom (kernelSubobjectMap sq)) x) = (CategoryStruct.comp (kernelSubobject f).arrow sq.left) x
              source
              @[simp]
              theorem CategoryTheory.Limits.kernelSubobjectMap_id {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] {f : X ⟶ Y} [HasKernel f] :
              kernelSubobjectMap (CategoryStruct.id (Arrow.mk f)) = CategoryStruct.id (Subobject.underlying.obj (kernelSubobject f))
              source
              @[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'') :
              kernelSubobjectMap (CategoryStruct.comp sq sq') = CategoryStruct.comp (kernelSubobjectMap sq) (kernelSubobjectMap sq')
              source
              theorem CategoryTheory.Limits.kernel_map_comp_kernelSubobjectIso_inv {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') :
              CategoryStruct.comp (kernel.map f f' sq.left sq.right ⋯) (kernelSubobjectIso f').inv = CategoryStruct.comp (kernelSubobjectIso f).inv (kernelSubobjectMap sq)
              source
              theorem CategoryTheory.Limits.kernel_map_comp_kernelSubobjectIso_inv_assoc {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') {Z : C} (h : Subobject.underlying.obj (kernelSubobject f') ⟶ Z) :
              CategoryStruct.comp (kernel.map f f' sq.left sq.right ⋯) (CategoryStruct.comp (kernelSubobjectIso f').inv h) = CategoryStruct.comp (kernelSubobjectIso f).inv (CategoryStruct.comp (kernelSubobjectMap sq) h)
              source
              theorem CategoryTheory.Limits.kernelSubobjectIso_comp_kernel_map {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') :
              CategoryStruct.comp (kernelSubobjectIso f).hom (kernel.map f f' sq.left sq.right ⋯) = CategoryStruct.comp (kernelSubobjectMap sq) (kernelSubobjectIso f').hom
              source
              theorem CategoryTheory.Limits.kernelSubobjectIso_comp_kernel_map_assoc {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') {Z : C} (h : kernel f' ⟶ Z) :
              CategoryStruct.comp (kernelSubobjectIso f).hom (CategoryStruct.comp (kernel.map f f' sq.left sq.right ⋯) h) = CategoryStruct.comp (kernelSubobjectMap sq) (CategoryStruct.comp (kernelSubobjectIso f').hom h)
              source
              @[simp]
              theorem CategoryTheory.Limits.kernelSubobject_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {A B : C} :
              kernelSubobject 0 = ⊤
              source
              instance CategoryTheory.Limits.isIso_kernelSubobject_zero_arrow {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] :
              IsIso (kernelSubobject 0).arrow
              source
              theorem CategoryTheory.Limits.le_kernelSubobject {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] (f : X ⟶ Y) [HasKernel f] (A : Subobject X) (h : CategoryStruct.comp A.arrow f = 0) :
              A ≤ kernelSubobject f
              source
              def CategoryTheory.Limits.kernelSubobjectIsoComp {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] {X' : C} (f : X' ⟶ X) [IsIso f] (g : X ⟶ Y) [HasKernel g] :
              Subobject.underlying.obj (kernelSubobject (CategoryStruct.comp f g)) ≅ Subobject.underlying.obj (kernelSubobject g)

              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
                source
                @[simp]
                theorem CategoryTheory.Limits.kernelSubobjectIsoComp_hom_arrow {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] {X' : C} (f : X' ⟶ X) [IsIso f] (g : X ⟶ Y) [HasKernel g] :
                CategoryStruct.comp (kernelSubobjectIsoComp f g).hom (kernelSubobject g).arrow = CategoryStruct.comp (kernelSubobject (CategoryStruct.comp f g)).arrow f
                source
                @[simp]
                theorem CategoryTheory.Limits.kernelSubobjectIsoComp_inv_arrow {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] {X' : C} (f : X' ⟶ X) [IsIso f] (g : X ⟶ Y) [HasKernel g] :
                CategoryStruct.comp (kernelSubobjectIsoComp f g).inv (kernelSubobject (CategoryStruct.comp f g)).arrow = CategoryStruct.comp (kernelSubobject g).arrow (inv f)
                source
                theorem CategoryTheory.Limits.kernelSubobject_comp_le {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] (f : X ⟶ Y) [HasKernel f] {Z : C} (h : Y ⟶ Z) [HasKernel (CategoryStruct.comp f h)] :
                kernelSubobject f ≤ kernelSubobject (CategoryStruct.comp f h)

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

                source
                @[simp]
                theorem CategoryTheory.Limits.kernelSubobject_comp_mono {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] (f : X ⟶ Y) [HasKernel f] {Z : C} (h : Y ⟶ Z) [Mono h] :
                kernelSubobject (CategoryStruct.comp f h) = kernelSubobject f

                Postcomposing by a monomorphism does not change the kernel subobject.

                source
                instance CategoryTheory.Limits.kernelSubobject_comp_mono_isIso {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] (f : X ⟶ Y) [HasKernel f] {Z : C} (h : Y ⟶ Z) [Mono h] :
                IsIso ((kernelSubobject f).ofLE (kernelSubobject (CategoryStruct.comp f h)) ⋯)
                source
                def CategoryTheory.Limits.cokernelOrderHom {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasCokernels C] (X : C) :
                Subobject X →o (Subobject (Opposite.op X))ᵒᵈ

                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
                  source
                  @[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✝
                  source
                  def CategoryTheory.Limits.kernelOrderHom {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasKernels C] (X : C) :
                  (Subobject (Opposite.op X))ᵒᵈ →o Subobject X

                  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
                    source
                    @[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✝
                    source
                    @[reducible, inline]
                    abbrev CategoryTheory.Limits.imageSubobject {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] :
                    Subobject Y

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

                    Equations
                    Instances For
                      source
                      def CategoryTheory.Limits.imageSubobjectIso {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] :
                      Subobject.underlying.obj (imageSubobject f) ≅ image f

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

                      Equations
                      Instances For
                        source
                        @[simp]
                        theorem CategoryTheory.Limits.imageSubobject_arrow {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] :
                        CategoryStruct.comp (imageSubobjectIso f).hom (image.ι f) = (imageSubobject f).arrow
                        source
                        @[simp]
                        theorem CategoryTheory.Limits.imageSubobject_arrow_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] {Z : C} (h : Y ⟶ Z) :
                        CategoryStruct.comp (imageSubobjectIso f).hom (CategoryStruct.comp (image.ι f) h) = CategoryStruct.comp (imageSubobject f).arrow h
                        source
                        @[simp]
                        theorem CategoryTheory.Limits.imageSubobject_arrow' {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] :
                        CategoryStruct.comp (imageSubobjectIso f).inv (imageSubobject f).arrow = image.ι f
                        source
                        @[simp]
                        theorem CategoryTheory.Limits.imageSubobject_arrow'_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] {Z : C} (h : Y ⟶ Z) :
                        CategoryStruct.comp (imageSubobjectIso f).inv (CategoryStruct.comp (imageSubobject f).arrow h) = CategoryStruct.comp (image.ι f) h
                        source
                        def CategoryTheory.Limits.factorThruImageSubobject {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] :
                        X ⟶ Subobject.underlying.obj (imageSubobject f)

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

                        Equations
                        Instances For
                          source
                          instance CategoryTheory.Limits.instEpiFactorThruImageSubobjectOfHasEqualizers {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] [HasEqualizers C] :
                          Epi (factorThruImageSubobject f)
                          source
                          @[simp]
                          theorem CategoryTheory.Limits.imageSubobject_arrow_comp {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] :
                          CategoryStruct.comp (factorThruImageSubobject f) (imageSubobject f).arrow = f
                          source
                          @[simp]
                          theorem CategoryTheory.Limits.imageSubobject_arrow_comp_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] {Z : C} (h : Y ⟶ Z) :
                          CategoryStruct.comp (factorThruImageSubobject f) (CategoryStruct.comp (imageSubobject f).arrow h) = CategoryStruct.comp f h
                          source
                          @[simp]
                          theorem CategoryTheory.Limits.imageSubobject_arrow_comp_apply {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : ConcreteCategory C F] (x : ToType X) :
                          (ConcreteCategory.hom (imageSubobject f).arrow) ((ConcreteCategory.hom (factorThruImageSubobject f)) x) = (ConcreteCategory.hom f) x
                          source
                          theorem CategoryTheory.Limits.imageSubobject_arrow_comp_eq_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [HasImage f] [Epi (factorThruImageSubobject f)] (h : CategoryStruct.comp f g = 0) :
                          CategoryStruct.comp (imageSubobject f).arrow g = 0
                          source
                          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) :
                          (imageSubobject f).Factors (CategoryStruct.comp k f)
                          source
                          @[simp]
                          theorem CategoryTheory.Limits.factorThruImageSubobject_comp_self {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] {W : C} (k : W ⟶ X) (h : (imageSubobject f).Factors (CategoryStruct.comp k f)) :
                          (imageSubobject f).factorThru (CategoryStruct.comp k f) h = CategoryStruct.comp k (factorThruImageSubobject f)
                          source
                          @[simp]
                          theorem CategoryTheory.Limits.factorThruImageSubobject_comp_self_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasImage f] {W W' : C} (k : W ⟶ W') (k' : W' ⟶ X) (h : (imageSubobject f).Factors (CategoryStruct.comp k (CategoryStruct.comp k' f))) :
                          (imageSubobject f).factorThru (CategoryStruct.comp k (CategoryStruct.comp k' f)) h = CategoryStruct.comp k (CategoryStruct.comp k' (factorThruImageSubobject f))
                          source
                          theorem CategoryTheory.Limits.imageSubobject_comp_le {C : Type u} [Category.{v, u} C] {X Y X' : C} (h : X' ⟶ X) (f : X ⟶ Y) [HasImage f] [HasImage (CategoryStruct.comp h f)] :
                          imageSubobject (CategoryStruct.comp h f) ≤ imageSubobject f

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

                          source
                          @[simp]
                          theorem CategoryTheory.Limits.imageSubobject_zero_arrow {C : Type u} [Category.{v, u} C] {X Y : C} [HasZeroMorphisms C] [HasZeroObject C] :
                          (imageSubobject 0).arrow = 0
                          source
                          @[simp]
                          theorem CategoryTheory.Limits.imageSubobject_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] {A B : C} :
                          imageSubobject 0 = ⊥
                          source
                          instance CategoryTheory.Limits.imageSubobject_comp_le_epi_of_epi {C : Type u} [Category.{v, u} C] {X Y : C} [HasEqualizers C] {X' : C} (h : X' ⟶ X) [Epi h] (f : X ⟶ Y) [HasImage f] [HasImage (CategoryStruct.comp h f)] :
                          Epi ((imageSubobject (CategoryStruct.comp h f)).ofLE (imageSubobject 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.

                          source
                          def CategoryTheory.Limits.imageSubobjectCompIso {C : Type u} [Category.{v, u} C] {X Y : C} [HasEqualizers C] (f : X ⟶ Y) [HasImage f] {Y' : C} (h : Y ⟶ Y') [IsIso h] :
                          Subobject.underlying.obj (imageSubobject (CategoryStruct.comp f h)) ≅ Subobject.underlying.obj (imageSubobject f)

                          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
                            source
                            @[simp]
                            theorem CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow {C : Type u} [Category.{v, u} C] {X Y : C} [HasEqualizers C] (f : X ⟶ Y) [HasImage f] {Y' : C} (h : Y ⟶ Y') [IsIso h] :
                            CategoryStruct.comp (imageSubobjectCompIso f h).hom (imageSubobject f).arrow = CategoryStruct.comp (imageSubobject (CategoryStruct.comp f h)).arrow (inv h)
                            source
                            @[simp]
                            theorem CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasEqualizers C] (f : X ⟶ Y) [HasImage f] {Y' : C} (h : Y ⟶ Y') [IsIso h] {Z : C} (h✝ : Y ⟶ Z) :
                            CategoryStruct.comp (imageSubobjectCompIso f h).hom (CategoryStruct.comp (imageSubobject f).arrow h✝) = CategoryStruct.comp (imageSubobject (CategoryStruct.comp f h)).arrow (CategoryStruct.comp (inv h) h✝)
                            source
                            @[simp]
                            theorem CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow {C : Type u} [Category.{v, u} C] {X Y : C} [HasEqualizers C] (f : X ⟶ Y) [HasImage f] {Y' : C} (h : Y ⟶ Y') [IsIso h] :
                            CategoryStruct.comp (imageSubobjectCompIso f h).inv (imageSubobject (CategoryStruct.comp f h)).arrow = CategoryStruct.comp (imageSubobject f).arrow h
                            source
                            @[simp]
                            theorem CategoryTheory.Limits.imageSubobjectCompIso_inv_arrow_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasEqualizers C] (f : X ⟶ Y) [HasImage f] {Y' : C} (h : Y ⟶ Y') [IsIso h] {Z : C} (h✝ : Y' ⟶ Z) :
                            CategoryStruct.comp (imageSubobjectCompIso f h).inv (CategoryStruct.comp (imageSubobject (CategoryStruct.comp f h)).arrow h✝) = CategoryStruct.comp (imageSubobject f).arrow (CategoryStruct.comp h h✝)
                            source
                            theorem CategoryTheory.Limits.imageSubobject_mono {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [Mono f] :
                            imageSubobject f = Subobject.mk f
                            source
                            theorem CategoryTheory.Limits.imageSubobject_iso_comp {C : Type u} [Category.{v, u} C] {X Y : C} [HasEqualizers C] {X' : C} (h : X' ⟶ X) [IsIso h] (f : X ⟶ Y) [HasImage f] :
                            imageSubobject (CategoryStruct.comp h f) = imageSubobject f

                            Precomposing by an isomorphism does not change the image subobject.

                            source
                            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) :
                            imageSubobject f ≤ X
                            source
                            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) :
                            imageSubobject f ≤ Subobject.mk g
                            source
                            def CategoryTheory.Limits.imageSubobjectMap {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} [HasImage f] {g : Y ⟶ Z} [HasImage g] (sq : Arrow.mk f ⟶ Arrow.mk g) [HasImageMap sq] :
                            Subobject.underlying.obj (imageSubobject f) ⟶ Subobject.underlying.obj (imageSubobject g)

                            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
                              source
                              @[simp]
                              theorem CategoryTheory.Limits.imageSubobjectMap_arrow {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} [HasImage f] {g : Y ⟶ Z} [HasImage g] (sq : Arrow.mk f ⟶ Arrow.mk g) [HasImageMap sq] :
                              CategoryStruct.comp (imageSubobjectMap sq) (imageSubobject g).arrow = CategoryStruct.comp (imageSubobject f).arrow sq.right
                              source
                              @[simp]
                              theorem CategoryTheory.Limits.imageSubobjectMap_arrow_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} [HasImage f] {g : Y ⟶ Z} [HasImage g] (sq : Arrow.mk f ⟶ Arrow.mk g) [HasImageMap sq] {Z✝ : C} (h : Z ⟶ Z✝) :
                              CategoryStruct.comp (imageSubobjectMap sq) (CategoryStruct.comp (imageSubobject g).arrow h) = CategoryStruct.comp (imageSubobject f).arrow (CategoryStruct.comp sq.right h)
                              source
                              theorem CategoryTheory.Limits.image_map_comp_imageSubobjectIso_inv {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} [HasImage f] {g : Y ⟶ Z} [HasImage g] (sq : Arrow.mk f ⟶ Arrow.mk g) [HasImageMap sq] :
                              CategoryStruct.comp (image.map sq) (imageSubobjectIso (Arrow.mk g).hom).inv = CategoryStruct.comp (imageSubobjectIso f).inv (imageSubobjectMap sq)
                              source
                              theorem CategoryTheory.Limits.imageSubobjectIso_comp_image_map {C : Type u} [Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} [HasImage f] {g : Y ⟶ Z} [HasImage g] (sq : Arrow.mk f ⟶ Arrow.mk g) [HasImageMap sq] :
                              CategoryStruct.comp (imageSubobjectIso (Arrow.mk f).hom).hom (image.map sq) = CategoryStruct.comp (imageSubobjectMap sq) (imageSubobjectIso g).hom