Documentation

Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Zero morphisms and zero objects #

A category "has zero morphisms" if there is a designated "zero morphism" in each morphism space, and compositions of zero morphisms with anything give the zero morphism. (Notice this is extra structure, not merely a property.)

A category "has a zero object" if it has an object which is both initial and terminal. Having a zero object provides zero morphisms, as the unique morphisms factoring through the zero object.

References #

source
class CategoryTheory.Limits.HasZeroMorphisms (C : Type u) [Category.{v, u} C] :
Type (max u v)

A category "has zero morphisms" if there is a designated "zero morphism" in each morphism space, and compositions of zero morphisms with anything give the zero morphism.

Instances
    source
    @[simp]
    theorem CategoryTheory.Limits.comp_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {Z : C} :
    CategoryStruct.comp f 0 = 0
    source
    @[simp]
    theorem CategoryTheory.Limits.zero_comp {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} {f : Y ⟶ Z} :
    CategoryStruct.comp 0 f = 0
    source
    instance CategoryTheory.Limits.hasZeroMorphismsPEmpty :
    HasZeroMorphisms (Discrete PEmpty.{u_1 + 1})
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance CategoryTheory.Limits.hasZeroMorphismsPUnit :
    HasZeroMorphisms (Discrete PUnit.{u_1 + 1})
    Equations
    • One or more equations did not get rendered due to their size.
    source
    theorem CategoryTheory.Limits.HasZeroMorphisms.ext {C : Type u} [Category.{v, u} C] (I J : HasZeroMorphisms C) :
    I = J

    If you're tempted to use this lemma "in the wild", you should probably carefully consider whether you've made a mistake in allowing two instances of HasZeroMorphisms to exist at all.

    See, particularly, the note on zeroMorphismsOfZeroObject below.

    source
    instance CategoryTheory.Limits.HasZeroMorphisms.instSubsingleton {C : Type u} [Category.{v, u} C] :
    Subsingleton (HasZeroMorphisms C)
    source
    instance CategoryTheory.Limits.hasZeroMorphismsOpposite {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] :
    HasZeroMorphisms Cᵒᵖ
    Equations
    source
    @[simp]
    theorem CategoryTheory.Limits.op_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) :
    Quiver.Hom.op 0 = 0
    source
    @[simp]
    theorem CategoryTheory.Limits.unop_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : Cᵒᵖ) :
    Quiver.Hom.unop 0 = 0
    source
    theorem CategoryTheory.Limits.zero_of_comp_mono {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} {f : X ⟶ Y} (g : Y ⟶ Z) [Mono g] (h : CategoryStruct.comp f g = 0) :
    f = 0
    source
    theorem CategoryTheory.Limits.zero_of_epi_comp {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) {g : Y ⟶ Z} [Epi f] (h : CategoryStruct.comp f g = 0) :
    g = 0
    source
    theorem CategoryTheory.Limits.eq_zero_of_image_eq_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [HasImage f] (w : image.ι f = 0) :
    f = 0
    source
    theorem CategoryTheory.Limits.nonzero_image_of_nonzero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [HasImage f] (w : f ≠ 0) :
    image.ι f ≠ 0
    source
    instance CategoryTheory.Limits.instHasZeroMorphismsFunctor {C : Type u} [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [HasZeroMorphisms D] :
    HasZeroMorphisms (Functor C D)
    Equations
    source
    @[simp]
    theorem CategoryTheory.Limits.zero_app {C : Type u} [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [HasZeroMorphisms D] (F G : Functor C D) (j : C) :
    NatTrans.app 0 j = 0
    source
    theorem CategoryTheory.Limits.IsZero.eq_zero_of_src {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (o : IsZero X) (f : X ⟶ Y) :
    f = 0
    source
    theorem CategoryTheory.Limits.IsZero.eq_zero_of_tgt {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (o : IsZero Y) (f : X ⟶ Y) :
    f = 0
    source
    theorem CategoryTheory.Limits.IsZero.iff_id_eq_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X : C) :
    IsZero X ↔ CategoryStruct.id X = 0
    source
    theorem CategoryTheory.Limits.IsZero.of_mono_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [Mono 0] :
    IsZero X
    source
    theorem CategoryTheory.Limits.IsZero.of_epi_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [Epi 0] :
    IsZero Y
    source
    theorem CategoryTheory.Limits.IsZero.of_mono_eq_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [Mono f] (h : f = 0) :
    IsZero X
    source
    theorem CategoryTheory.Limits.IsZero.of_epi_eq_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [Epi f] (h : f = 0) :
    IsZero Y
    source
    theorem CategoryTheory.Limits.IsZero.iff_isSplitMono_eq_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [IsSplitMono f] :
    IsZero X ↔ f = 0
    source
    theorem CategoryTheory.Limits.IsZero.iff_isSplitEpi_eq_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [IsSplitEpi f] :
    IsZero Y ↔ f = 0
    source
    theorem CategoryTheory.Limits.IsZero.of_mono {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [Mono f] (i : IsZero Y) :
    IsZero X
    source
    theorem CategoryTheory.Limits.IsZero.of_epi {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [Epi f] (i : IsZero X) :
    IsZero Y
    source
    def CategoryTheory.Limits.IsZero.hasZeroMorphisms {C : Type u} [Category.{v, u} C] {O : C} (hO : IsZero O) :
    HasZeroMorphisms C

    A category with a zero object has zero morphisms.

    It is rarely a good idea to use this. Many categories that have a zero object have zero morphisms for some other reason, for example from additivity. Library code that uses zeroMorphismsOfZeroObject will then be incompatible with these categories because the HasZeroMorphisms instances will not be definitionally equal. For this reason library code should generally ask for an instance of HasZeroMorphisms separately, even if it already asks for an instance of HasZeroObjects.

    Equations
    Instances For
      source
      def CategoryTheory.Limits.HasZeroObject.zeroMorphismsOfZeroObject {C : Type u} [Category.{v, u} C] [HasZeroObject C] :
      HasZeroMorphisms C

      A category with a zero object has zero morphisms.

      It is rarely a good idea to use this. Many categories that have a zero object have zero morphisms for some other reason, for example from additivity. Library code that uses zeroMorphismsOfZeroObject will then be incompatible with these categories because the has_zero_morphisms instances will not be definitionally equal. For this reason library code should generally ask for an instance of HasZeroMorphisms separately, even if it already asks for an instance of HasZeroObjects.

      Equations
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial_hom {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X : C} (t : IsInitial X) :
        (zeroIsoIsInitial t).hom = 0
        source
        @[simp]
        theorem CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial_inv {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X : C} (t : IsInitial X) :
        (zeroIsoIsInitial t).inv = 0
        source
        @[simp]
        theorem CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal_hom {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X : C} (t : IsTerminal X) :
        (zeroIsoIsTerminal t).hom = 0
        source
        @[simp]
        theorem CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal_inv {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X : C} (t : IsTerminal X) :
        (zeroIsoIsTerminal t).inv = 0
        source
        @[simp]
        theorem CategoryTheory.Limits.HasZeroObject.zeroIsoInitial_hom {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] [HasInitial C] :
        zeroIsoInitial.hom = 0
        source
        @[simp]
        theorem CategoryTheory.Limits.HasZeroObject.zeroIsoInitial_inv {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] [HasInitial C] :
        zeroIsoInitial.inv = 0
        source
        @[simp]
        theorem CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal_hom {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] [HasTerminal C] :
        zeroIsoTerminal.hom = 0
        source
        @[simp]
        theorem CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal_inv {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] [HasTerminal C] :
        zeroIsoTerminal.inv = 0
        source
        instance CategoryTheory.Limits.HasZeroObject.instFunctor {C : Type u} [Category.{v, u} C] [HasZeroObject C] {B : Type u_1} [Category.{u_2, u_1} B] :
        HasZeroObject (Functor B C)
        source
        @[simp]
        theorem CategoryTheory.Limits.IsZero.map {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasZeroObject D] [HasZeroMorphisms D] {F : Functor C D} (hF : IsZero F) {X Y : C} (f : X ⟶ Y) :
        F.map f = 0
        source
        @[simp]
        theorem CategoryTheory.Functor.zero_obj {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [Limits.HasZeroObject D] (X : C) :
        Limits.IsZero ((toPrefunctor 0).obj X)
        source
        @[simp]
        theorem CategoryTheory.zero_map {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [Limits.HasZeroObject D] [Limits.HasZeroMorphisms D] {X Y : C} (f : X ⟶ Y) :
        (Functor.toPrefunctor 0).map f = 0
        source
        @[simp]
        theorem CategoryTheory.Limits.id_zero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] :
        CategoryStruct.id 0 = 0
        source
        theorem CategoryTheory.Limits.zero_of_to_zero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X : C} (f : X ⟶ 0) :
        f = 0

        An arrow ending in the zero object is zero

        source
        theorem CategoryTheory.Limits.zero_of_target_iso_zero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : Y ≅ 0) :
        f = 0
        source
        theorem CategoryTheory.Limits.zero_of_from_zero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X : C} (f : 0 ⟶ X) :
        f = 0

        An arrow starting at the zero object is zero

        source
        theorem CategoryTheory.Limits.zero_of_source_iso_zero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : X ≅ 0) :
        f = 0
        source
        theorem CategoryTheory.Limits.zero_of_source_iso_zero' {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : IsIsomorphic X 0) :
        f = 0
        source
        theorem CategoryTheory.Limits.zero_of_target_iso_zero' {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : IsIsomorphic Y 0) :
        f = 0
        source
        theorem CategoryTheory.Limits.mono_of_source_iso_zero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : X ≅ 0) :
        Mono f
        source
        theorem CategoryTheory.Limits.epi_of_target_iso_zero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : Y ≅ 0) :
        Epi f
        source
        def CategoryTheory.Limits.idZeroEquivIsoZero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) :
        CategoryStruct.id X = 0 ≃ (X ≅ 0)

        An object X has 𝟙 X = 0 if and only if it is isomorphic to the zero object.

        Because X ≅ 0 contains data (even if a subsingleton), we express this ↔ as an ≃.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Limits.idZeroEquivIsoZero_apply_hom {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) (h : CategoryStruct.id X = 0) :
          ((idZeroEquivIsoZero X) h).hom = 0
          source
          @[simp]
          theorem CategoryTheory.Limits.idZeroEquivIsoZero_apply_inv {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) (h : CategoryStruct.id X = 0) :
          ((idZeroEquivIsoZero X) h).inv = 0
          source
          def CategoryTheory.Limits.isoZeroOfMonoZero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} :
          Mono 0 → (X ≅ 0)

          If 0 : X ⟶ Y is a monomorphism, then X ≅ 0.

          Equations
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Limits.isoZeroOfMonoZero_hom {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} (x✝ : Mono 0) :
            (isoZeroOfMonoZero x✝).hom = 0
            source
            @[simp]
            theorem CategoryTheory.Limits.isoZeroOfMonoZero_inv {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} (x✝ : Mono 0) :
            (isoZeroOfMonoZero x✝).inv = 0
            source
            def CategoryTheory.Limits.isoZeroOfEpiZero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} :
            Epi 0 → (Y ≅ 0)

            If 0 : X ⟶ Y is an epimorphism, then Y ≅ 0.

            Equations
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Limits.isoZeroOfEpiZero_inv {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} (x✝ : Epi 0) :
              (isoZeroOfEpiZero x✝).inv = 0
              source
              @[simp]
              theorem CategoryTheory.Limits.isoZeroOfEpiZero_hom {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} (x✝ : Epi 0) :
              (isoZeroOfEpiZero x✝).hom = 0
              source
              def CategoryTheory.Limits.isoZeroOfMonoEqZero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [Mono f] (h : f = 0) :
              X ≅ 0

              If a monomorphism out of X is zero, then X ≅ 0.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def CategoryTheory.Limits.isoZeroOfEpiEqZero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [Epi f] (h : f = 0) :
                Y ≅ 0

                If an epimorphism in to Y is zero, then Y ≅ 0.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def CategoryTheory.Limits.isoOfIsIsomorphicZero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X : C} (P : IsIsomorphic X 0) :
                  X ≅ 0

                  If an object X is isomorphic to 0, there's no need to use choice to construct an explicit isomorphism: the zero morphism suffices.

                  Equations
                  Instances For
                    source
                    def CategoryTheory.Limits.isIsoZeroEquiv {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) :
                    IsIso 0 ≃ CategoryStruct.id X = 0 ∧ CategoryStruct.id Y = 0

                    A zero morphism 0 : X ⟶ Y is an isomorphism if and only if the identities on both X and Y are zero.

                    Equations
                    Instances For
                      source
                      def CategoryTheory.Limits.isIsoZeroSelfEquiv {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X : C) :
                      IsIso 0 ≃ CategoryStruct.id X = 0

                      A zero morphism 0 : X ⟶ X is an isomorphism if and only if the identity on X is zero.

                      Equations
                      Instances For
                        source
                        def CategoryTheory.Limits.isIsoZeroEquivIsoZero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] (X Y : C) :
                        IsIso 0 ≃ (X ≅ 0) × (Y ≅ 0)

                        A zero morphism 0 : X ⟶ Y is an isomorphism if and only if X and Y are isomorphic to the zero object.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          theorem CategoryTheory.Limits.isIso_of_source_target_iso_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] {X Y : C} (f : X ⟶ Y) (i : X ≅ 0) (j : Y ≅ 0) :
                          IsIso f
                          source
                          def CategoryTheory.Limits.isIsoZeroSelfEquivIsoZero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] (X : C) :
                          IsIso 0 ≃ (X ≅ 0)

                          A zero morphism 0 : X ⟶ X is an isomorphism if and only if X is isomorphic to the zero object.

                          Equations
                          Instances For
                            source
                            theorem CategoryTheory.Limits.hasZeroObject_of_hasInitial_object {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasInitial C] :
                            HasZeroObject C

                            If there are zero morphisms, any initial object is a zero object.

                            source
                            theorem CategoryTheory.Limits.hasZeroObject_of_hasTerminal_object {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasTerminal C] :
                            HasZeroObject C

                            If there are zero morphisms, any terminal object is a zero object.

                            source
                            theorem CategoryTheory.Limits.image_ι_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 (factorThruImage f)] (h : CategoryStruct.comp f g = 0) :
                            CategoryStruct.comp (image.ι f) g = 0
                            source
                            theorem CategoryTheory.Limits.comp_factorThruImage_eq_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [HasImage g] (h : CategoryStruct.comp f g = 0) :
                            CategoryStruct.comp f (factorThruImage g) = 0
                            source
                            def CategoryTheory.Limits.monoFactorisationZero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] (X Y : C) :
                            MonoFactorisation 0

                            The zero morphism has a MonoFactorisation through the zero object.

                            Equations
                            Instances For
                              source
                              @[simp]
                              theorem CategoryTheory.Limits.monoFactorisationZero_I {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] (X Y : C) :
                              (monoFactorisationZero X Y).I = 0
                              source
                              @[simp]
                              theorem CategoryTheory.Limits.monoFactorisationZero_e {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] (X Y : C) :
                              (monoFactorisationZero X Y).e = 0
                              source
                              @[simp]
                              theorem CategoryTheory.Limits.monoFactorisationZero_m {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] (X Y : C) :
                              (monoFactorisationZero X Y).m = 0
                              source
                              def CategoryTheory.Limits.imageFactorisationZero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] (X Y : C) :
                              ImageFactorisation 0

                              The factorisation through the zero object is an image factorisation.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                instance CategoryTheory.Limits.hasImage_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] {X Y : C} :
                                HasImage 0
                                source
                                def CategoryTheory.Limits.imageZero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] {X Y : C} :
                                image 0 ≅ 0

                                The image of a zero morphism is the zero object.

                                Equations
                                Instances For
                                  source
                                  def CategoryTheory.Limits.imageZero' {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] {X Y : C} {f : X ⟶ Y} (h : f = 0) [HasImage f] :
                                  image f ≅ 0

                                  The image of a morphism which is equal to zero is the zero object.

                                  Equations
                                  Instances For
                                    source
                                    @[simp]
                                    theorem CategoryTheory.Limits.image.ι_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] {X Y : C} [HasImage 0] :
                                    ι 0 = 0
                                    source
                                    @[simp]
                                    theorem CategoryTheory.Limits.image.ι_zero' {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] [HasEqualizers C] {X Y : C} {f : X ⟶ Y} (h : f = 0) [HasImage f] :
                                    ι f = 0

                                    If we know f = 0, it requires a little work to conclude image.ι f = 0, because f = g only implies image f ≅ image g.

                                    source
                                    instance CategoryTheory.Limits.isSplitMono_sigma_ι {C : Type u} [Category.{v, u} C] {β : Type u'} [HasZeroMorphisms C] (f : β → C) [HasColimit (Discrete.functor f)] (b : β) :
                                    IsSplitMono (Sigma.ι f b)

                                    In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms.

                                    source
                                    instance CategoryTheory.Limits.isSplitEpi_pi_π {C : Type u} [Category.{v, u} C] {β : Type u'} [HasZeroMorphisms C] (f : β → C) [HasLimit (Discrete.functor f)] (b : β) :
                                    IsSplitEpi (Pi.π f b)

                                    In the presence of zero morphisms, projections into a product are (split) epimorphisms.

                                    source
                                    instance CategoryTheory.Limits.isSplitMono_coprod_inl {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} [HasColimit (pair X Y)] :
                                    IsSplitMono coprod.inl

                                    In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms.

                                    source
                                    instance CategoryTheory.Limits.isSplitMono_coprod_inr {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} [HasColimit (pair X Y)] :
                                    IsSplitMono coprod.inr

                                    In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms.

                                    source
                                    instance CategoryTheory.Limits.isSplitEpi_prod_fst {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} [HasLimit (pair X Y)] :
                                    IsSplitEpi prod.fst

                                    In the presence of zero morphisms, projections into a product are (split) epimorphisms.

                                    source
                                    instance CategoryTheory.Limits.isSplitEpi_prod_snd {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} [HasLimit (pair X Y)] :
                                    IsSplitEpi prod.snd

                                    In the presence of zero morphisms, projections into a product are (split) epimorphisms.

                                    source
                                    def CategoryTheory.Limits.IsLimit.ofIsZero {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasZeroMorphisms C] [HasZeroObject C] {F : Functor D C} (c : Cone F) (hF : IsZero F) (hc : IsZero c.pt) :
                                    IsLimit c

                                    If a functor F is zero, then any cone for F with a zero point is limit.

                                    Equations
                                    Instances For
                                      source
                                      def CategoryTheory.Limits.IsColimit.ofIsZero {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasZeroMorphisms C] [HasZeroObject C] {F : Functor D C} (c : Cocone F) (hF : IsZero F) (hc : IsZero c.pt) :
                                      IsColimit c

                                      If a functor F is zero, then any cocone for F with a zero point is colimit.

                                      Equations
                                      Instances For
                                        source
                                        theorem CategoryTheory.Limits.IsLimit.isZero_pt {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasZeroMorphisms C] [HasZeroObject C] {F : Functor D C} {c : Cone F} (hc : IsLimit c) (hF : IsZero F) :
                                        IsZero c.pt
                                        source
                                        theorem CategoryTheory.Limits.IsColimit.isZero_pt {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasZeroMorphisms C] [HasZeroObject C] {F : Functor D C} {c : Cocone F} (hc : IsColimit c) (hF : IsZero F) :
                                        IsZero c.pt
                                        source
                                        theorem CategoryTheory.Limits.IsTerminal.isZero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X : C} (hX : IsTerminal X) :
                                        IsZero X
                                        source
                                        theorem CategoryTheory.Limits.IsInitial.isZero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X : C} (hX : IsInitial X) :
                                        IsZero X