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 #

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
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.

    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.

    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

      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

        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

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

          Equations
          Instances For

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

            Equations
            Instances For

              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

                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

                  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

                    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

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

                      Equations
                      Instances For

                        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

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

                          Equations
                          Instances For

                            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

                              The image of a zero morphism is the zero object.

                              Equations
                              Instances For

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

                                Equations
                                Instances For
                                  @[simp]

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

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

                                  Equations
                                  • =

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

                                  Equations
                                  • =

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

                                  Equations
                                  • =

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

                                  Equations
                                  • =

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

                                  Equations
                                  • =

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

                                  Equations
                                  • =