Documentation

Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Zero objects #

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; see CategoryTheory.Limits.Shapes.ZeroMorphisms.

References #

  • unique_to : ∀ (Y : C), Nonempty (Unique (X Y))

    there are unique morphisms to the object

  • unique_from : ∀ (Y : C), Nonempty (Unique (Y X))

    there are unique morphisms from the object

An object X in a category is a zero object if for every object Y there is a unique morphism to : X → Y and a unique morphism from : Y → X.

This is a characteristic predicate for has_zero_object.

Instances For

    If h : IsZero X, then h.to_ Y is a choice of unique morphism X → Y.

    Instances For

      If h : is_zero X, then h.from_ Y is a choice of unique morphism Y → X.

      Instances For
        theorem CategoryTheory.Limits.IsZero.eq_of_src {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (hX : CategoryTheory.Limits.IsZero X) (f : X Y) (g : X Y) :
        f = g
        theorem CategoryTheory.Limits.IsZero.eq_of_tgt {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (hX : CategoryTheory.Limits.IsZero X) (f : Y X) (g : Y X) :
        f = g

        Any two zero objects are isomorphic.

        Instances For

          A zero object is in particular initial.

          Instances For

            A zero object is in particular terminal.

            Instances For

              The (unique) isomorphism between any initial object and the zero object.

              Instances For

                The (unique) isomorphism between any terminal object and the zero object.

                Instances For

                  A category "has a zero object" if it has an object which is both initial and terminal.

                  Instances

                    Construct a Zero C for a category with a zero object. This can not be a global instance as it will trigger for every Zero C typeclass search.

                    Instances For

                      Every zero object is isomorphic to the zero object.

                      Instances For

                        There is a unique morphism from the zero object to any object X.

                        Instances For

                          There is a unique morphism from any object X to the zero object.

                          Instances For

                            The (unique) isomorphism between any initial object and the zero object.

                            Instances For

                              The (unique) isomorphism between any terminal object and the zero object.

                              Instances For

                                The (unique) isomorphism between the chosen initial object and the chosen zero object.

                                Instances For

                                  The (unique) isomorphism between the chosen terminal object and the chosen zero object.

                                  Instances For