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
                        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
                            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
                                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
                                    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
                                                    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
                                                        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