Documentation

Mathlib.CategoryTheory.Limits.Shapes.Terminal

Initial and terminal objects in a category. #

References #

Construct a cone for the empty diagram given an object.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Construct a cocone for the empty diagram given an object.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[reducible, inline]
      abbrev CategoryTheory.Limits.IsTerminal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) :
      Type (max (max 0 u₁) v₁)

      X is terminal if the cone it induces on the empty diagram is limiting.

      Equations
      Instances For
        @[reducible, inline]
        abbrev CategoryTheory.Limits.IsInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) :
        Type (max (max 0 u₁) v₁)

        X is initial if the cocone it induces on the empty diagram is colimiting.

        Equations
        Instances For

          An object Y is terminal iff for every X there is a unique morphism X ⟶ Y.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            An object Y is terminal if for every X there is a unique morphism X ⟶ Y (as an instance).

            Equations
            Instances For
              def CategoryTheory.Limits.IsTerminal.ofUniqueHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y : C} (h : (X : C) → X Y) (uniq : ∀ (X : C) (m : X Y), m = h X) :

              An object Y is terminal if for every X there is a unique morphism X ⟶ Y (as explicit arguments).

              Equations
              Instances For

                If α is a preorder with top, then is a terminal object.

                Equations
                Instances For

                  Transport a term of type IsTerminal across an isomorphism.

                  Equations
                  Instances For

                    If X and Y are isomorphic, then X is terminal iff Y is.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      An object X is initial iff for every Y there is a unique morphism X ⟶ Y.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        An object X is initial if for every Y there is a unique morphism X ⟶ Y (as an instance).

                        Equations
                        Instances For
                          def CategoryTheory.Limits.IsInitial.ofUniqueHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (h : (Y : C) → X Y) (uniq : ∀ (Y : C) (m : X Y), m = h Y) :

                          An object X is initial if for every Y there is a unique morphism X ⟶ Y (as explicit arguments).

                          Equations
                          Instances For

                            If α is a preorder with bot, then is an initial object.

                            Equations
                            Instances For

                              Transport a term of type is_initial across an isomorphism.

                              Equations
                              Instances For

                                If X and Y are isomorphic, then X is initial iff Y is.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  Give the morphism to a terminal object from any other.

                                  Equations
                                  Instances For

                                    Any two morphisms to a terminal object are equal.

                                    Give the morphism from an initial object to any other.

                                    Equations
                                    Instances For
                                      theorem CategoryTheory.Limits.IsInitial.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (t : CategoryTheory.Limits.IsInitial X) (f : X Y) (g : X Y) :
                                      f = g

                                      Any two morphisms from an initial object are equal.

                                      Any morphism from a terminal object is split mono.

                                      Any morphism to an initial object is split epi.

                                      Any morphism from a terminal object is mono.

                                      Any morphism to an initial object is epi.

                                      @[simp]
                                      theorem CategoryTheory.Limits.IsTerminal.uniqueUpToIso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : C} {T' : C} (hT : CategoryTheory.Limits.IsTerminal T) (hT' : CategoryTheory.Limits.IsTerminal T') :
                                      (hT.uniqueUpToIso hT').inv = hT.from T'
                                      @[simp]
                                      theorem CategoryTheory.Limits.IsTerminal.uniqueUpToIso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : C} {T' : C} (hT : CategoryTheory.Limits.IsTerminal T) (hT' : CategoryTheory.Limits.IsTerminal T') :
                                      (hT.uniqueUpToIso hT').hom = hT'.from T

                                      If T and T' are terminal, they are isomorphic.

                                      Equations
                                      • hT.uniqueUpToIso hT' = { hom := hT'.from T, inv := hT.from T', hom_inv_id := , inv_hom_id := }
                                      Instances For
                                        @[simp]
                                        theorem CategoryTheory.Limits.IsInitial.uniqueUpToIso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : C} {I' : C} (hI : CategoryTheory.Limits.IsInitial I) (hI' : CategoryTheory.Limits.IsInitial I') :
                                        (hI.uniqueUpToIso hI').inv = hI'.to I
                                        @[simp]
                                        theorem CategoryTheory.Limits.IsInitial.uniqueUpToIso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {I : C} {I' : C} (hI : CategoryTheory.Limits.IsInitial I) (hI' : CategoryTheory.Limits.IsInitial I') :
                                        (hI.uniqueUpToIso hI').hom = hI.to I'

                                        If I and I' are initial, they are isomorphic.

                                        Equations
                                        • hI.uniqueUpToIso hI' = { hom := hI.to I', inv := hI'.to I, hom_inv_id := , inv_hom_id := }
                                        Instances For
                                          @[reducible, inline]

                                          A category has a terminal object if it has a limit over the empty diagram. Use hasTerminal_of_unique to construct instances.

                                          Equations
                                          Instances For
                                            @[reducible, inline]

                                            A category has an initial object if it has a colimit over the empty diagram. Use hasInitial_of_unique to construct instances.

                                            Equations
                                            Instances For

                                              Being terminal is independent of the empty diagram, its universe, and the cone over it, as long as the cone points are isomorphic.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For

                                                Replacing an empty cone in IsLimit by another with the same cone point is an equivalence.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For

                                                  Being initial is independent of the empty diagram, its universe, and the cocone over it, as long as the cocone points are isomorphic.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For

                                                    Replacing an empty cocone in IsColimit by another with the same cocone point is an equivalence.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      @[reducible, inline]

                                                      An arbitrary choice of terminal object, if one exists. You can use the notation ⊤_ C. This object is characterized by having a unique morphism from any object.

                                                      Equations
                                                      Instances For
                                                        @[reducible, inline]

                                                        An arbitrary choice of initial object, if one exists. You can use the notation ⊥_ C. This object is characterized by having a unique morphism to any object.

                                                        Equations
                                                        Instances For

                                                          Notation for the terminal object in C

                                                          Equations
                                                          Instances For

                                                            Notation for the initial object in C

                                                            Equations
                                                            Instances For

                                                              We can more explicitly show that a category has a terminal object by specifying the object, and showing there is a unique morphism to it from any other object.

                                                              We can more explicitly show that a category has an initial object by specifying the object, and showing there is a unique morphism from it to any other object.

                                                              A terminal object is terminal.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For

                                                                An initial object is initial.

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For

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

                                                                  Equations
                                                                  Instances For

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

                                                                    Equations
                                                                    Instances For

                                                                      Any morphism from a terminal object is split mono.

                                                                      Equations
                                                                      • =

                                                                      Any morphism to an initial object is split epi.

                                                                      Equations
                                                                      • =

                                                                      An initial object is terminal in the opposite category.

                                                                      Equations
                                                                      Instances For

                                                                        An initial object in the opposite category is terminal in the original category.

                                                                        Equations
                                                                        Instances For

                                                                          A terminal object is initial in the opposite category.

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For

                                                                            A terminal object in the opposite category is initial in the original category.

                                                                            Equations
                                                                            Instances For

                                                                              The limit of the constant ⊤_ C functor is ⊤_ C.

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For

                                                                                The colimit of the constant ⊥_ C functor is ⊥_ C.

                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For

                                                                                  A category is an InitialMonoClass if the canonical morphism of an initial object is a monomorphism. In practice, this is most useful when given an arbitrary morphism out of the chosen initial object, see initial.mono_from. Given a terminal object, this is equivalent to the assumption that the unique morphism from initial to terminal is a monomorphism, which is the second of Freyd's axioms for an AT category.

                                                                                  TODO: This is a condition satisfied by categories with zero objects and morphisms.

                                                                                  Instances

                                                                                    The map from the (any as stated) initial object to any other object is a monomorphism

                                                                                    To show a category is an InitialMonoClass it suffices to give an initial object such that every morphism out of it is a monomorphism.

                                                                                    To show a category is an InitialMonoClass it suffices to show every morphism out of the initial object is a monomorphism.

                                                                                    To show a category is an InitialMonoClass it suffices to show the unique morphism from an initial object to a terminal object is a monomorphism.

                                                                                    To show a category is an InitialMonoClass it suffices to show the unique morphism from the initial object to a terminal object is a monomorphism.

                                                                                    The comparison morphism from the image of a terminal object to the terminal object in the target category. This is an isomorphism iff G preserves terminal objects, see CategoryTheory.Limits.PreservesTerminal.ofIsoComparison.

                                                                                    Equations
                                                                                    Instances For

                                                                                      The comparison morphism from the initial object in the target category to the image of the initial object.

                                                                                      Equations
                                                                                      Instances For

                                                                                        From a functor F : J ⥤ C, given an initial object of J, construct a cone for J. In limitOfDiagramInitial we show it is a limit cone.

                                                                                        Equations
                                                                                        Instances For

                                                                                          From a functor F : J ⥤ C, given an initial object of J, show the cone coneOfDiagramInitial is a limit.

                                                                                          Equations
                                                                                          Instances For
                                                                                            @[reducible, inline]

                                                                                            For a functor F : J ⥤ C, if J has an initial object then the image of it is isomorphic to the limit of F.

                                                                                            Equations
                                                                                            Instances For

                                                                                              From a functor F : J ⥤ C, given a terminal object of J, construct a cone for J, provided that the morphisms in the diagram are isomorphisms. In limitOfDiagramTerminal we show it is a limit cone.

                                                                                              Equations
                                                                                              Instances For

                                                                                                From a functor F : J ⥤ C, given a terminal object of J and that the morphisms in the diagram are isomorphisms, show the cone coneOfDiagramTerminal is a limit.

                                                                                                Equations
                                                                                                Instances For
                                                                                                  @[reducible, inline]

                                                                                                  For a functor F : J ⥤ C, if J has a terminal object and all the morphisms in the diagram are isomorphisms, then the image of the terminal object is isomorphic to the limit of F.

                                                                                                  Equations
                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                  Instances For

                                                                                                    From a functor F : J ⥤ C, given a terminal object of J, construct a cocone for J. In colimitOfDiagramTerminal we show it is a colimit cocone.

                                                                                                    Equations
                                                                                                    Instances For

                                                                                                      From a functor F : J ⥤ C, given a terminal object of J, show the cocone coconeOfDiagramTerminal is a colimit.

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        @[reducible, inline]

                                                                                                        For a functor F : J ⥤ C, if J has a terminal object then the image of it is isomorphic to the colimit of F.

                                                                                                        Equations
                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                        Instances For

                                                                                                          From a functor F : J ⥤ C, given an initial object of J, construct a cocone for J, provided that the morphisms in the diagram are isomorphisms. In colimitOfDiagramInitial we show it is a colimit cocone.

                                                                                                          Equations
                                                                                                          Instances For

                                                                                                            From a functor F : J ⥤ C, given an initial object of J and that the morphisms in the diagram are isomorphisms, show the cone coconeOfDiagramInitial is a colimit.

                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              @[reducible, inline]

                                                                                                              For a functor F : J ⥤ C, if J has an initial object and all the morphisms in the diagram are isomorphisms, then the image of the initial object is isomorphic to the colimit of F.

                                                                                                              Equations
                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                              Instances For

                                                                                                                Any morphism between terminal objects is an isomorphism.

                                                                                                                Any morphism between initial objects is an isomorphism.