Documentation

Mathlib.CategoryTheory.WithTerminal

WithInitial and WithTerminal #

Given a category C, this file constructs two objects:

  1. WithTerminal C, the category built from C by formally adjoining a terminal object.
  2. WithInitial C, the category built from C by formally adjoining an initial object.

The terminal resp. initial object is WithTerminal.star resp. WithInitial.star, and the proofs that these are terminal resp. initial are in WithTerminal.star_terminal and WithInitial.star_initial.

The inclusion from C into WithTerminal C resp. WithInitial C is denoted WithTerminal.incl resp. WithInitial.incl.

The relevant constructions needed for the universal properties of these constructions are:

  1. lift, which lifts F : C ⥤ D to a functor from WithTerminal C resp. WithInitial C in the case where an object Z : D is provided satisfying some additional conditions.
  2. inclLift shows that the composition of lift with incl is isomorphic to the functor which was lifted.
  3. liftUnique provides the uniqueness property of lift.

In addition to this, we provide WithTerminal.map and WithInitial.map providing the functoriality of these constructions with respect to functors on the base categories.

We define corresponding pseudofunctors WithTerminal.pseudofunctor and WithInitial.pseudofunctor from Cat to Cat.

Formally adjoin a terminal object to a category.

Instances For
    Equations
    • CategoryTheory.instInhabitedWithTerminal = { default := CategoryTheory.WithTerminal.star }
    inductive CategoryTheory.WithInitial (C : Type u) :

    Formally adjoin an initial object to a category.

    Instances For
      Equations
      • CategoryTheory.instInhabitedWithInitial = { default := CategoryTheory.WithInitial.star }

      Morphisms for WithTerminal C.

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

        Identity morphisms for WithTerminal C.

        Equations
        Instances For

          Composition of morphisms for WithTerminal C.

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

            The inclusion from C into WithTerminal C.

            Equations
            • CategoryTheory.WithTerminal.incl = { obj := CategoryTheory.WithTerminal.of, map := fun {X Y : C} (f : X Y) => f, map_id := , map_comp := }
            Instances For
              instance CategoryTheory.WithTerminal.instFullIncl {C : Type u} [CategoryTheory.Category.{v, u} C] :
              CategoryTheory.WithTerminal.incl.Full
              Equations
              • =
              instance CategoryTheory.WithTerminal.instFaithfulIncl {C : Type u} [CategoryTheory.Category.{v, u} C] :
              CategoryTheory.WithTerminal.incl.Faithful
              Equations
              • =
              @[simp]
              theorem CategoryTheory.WithTerminal.map_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (F : CategoryTheory.Functor C D) (X : CategoryTheory.WithTerminal C) :
              (CategoryTheory.WithTerminal.map F).obj X = match X with | CategoryTheory.WithTerminal.of x => CategoryTheory.WithTerminal.of (F.obj x) | CategoryTheory.WithTerminal.star => CategoryTheory.WithTerminal.star
              @[simp]
              theorem CategoryTheory.WithTerminal.map_map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (F : CategoryTheory.Functor C D) {X : CategoryTheory.WithTerminal C} {Y : CategoryTheory.WithTerminal C} (f : X Y) :
              (CategoryTheory.WithTerminal.map F).map f = match X, Y, f with | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.of y, f => F.map (CategoryTheory.WithTerminal.down f) | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.star, x => PUnit.unit | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => PUnit.unit

              Map WithTerminal with respect to a functor F : C ⥤ D.

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

                A natural isomorphism between the functor map (𝟭 C) and 𝟭 (WithTerminal C).

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

                  A natural isomorphism between the functor map (F ⋙ G) and map F ⋙ map G .

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem CategoryTheory.WithTerminal.map₂_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (η : F G) (X : CategoryTheory.WithTerminal C) :
                    (CategoryTheory.WithTerminal.map₂ η).app X = match X with | CategoryTheory.WithTerminal.of x => η.app x | CategoryTheory.WithTerminal.star => CategoryTheory.CategoryStruct.id CategoryTheory.WithTerminal.star

                    From a natural transformation of functors C ⥤ D, the induced natural transformation of functors WithTerminal C ⥤ WithTerminal D.

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

                      The prelax functor from Cat to Cat defined with WithTerminal.

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

                        The pseudofunctor from Cat to Cat defined with WithTerminal.

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

                          WithTerminal.star is terminal.

                          Equations
                          Instances For
                            @[simp]
                            theorem CategoryTheory.WithTerminal.lift_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x Z) (hM : ∀ (x y : C) (f : x y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) (X : CategoryTheory.WithTerminal C) :
                            (CategoryTheory.WithTerminal.lift F M hM).obj X = match X with | CategoryTheory.WithTerminal.of x => F.obj x | CategoryTheory.WithTerminal.star => Z
                            @[simp]
                            theorem CategoryTheory.WithTerminal.lift_map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x Z) (hM : ∀ (x y : C) (f : x y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) {X : CategoryTheory.WithTerminal C} {Y : CategoryTheory.WithTerminal C} (f : X Y) :
                            (CategoryTheory.WithTerminal.lift F M hM).map f = match X, Y, f with | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.of y, f => F.map (CategoryTheory.WithTerminal.down f) | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => M x | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id Z
                            def CategoryTheory.WithTerminal.lift {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x Z) (hM : ∀ (x y : C) (f : x y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) :

                            Lift a functor F : C ⥤ D to WithTerminal C ⥤ D.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[simp]
                              theorem CategoryTheory.WithTerminal.inclLift_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x Z) (hM : ∀ (x y : C) (f : x y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) (X : C) :
                              @[simp]
                              theorem CategoryTheory.WithTerminal.inclLift_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x Z) (hM : ∀ (x y : C) (f : x y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) (X : C) :
                              (CategoryTheory.WithTerminal.inclLift F M hM).hom.app X = CategoryTheory.CategoryStruct.id (match CategoryTheory.WithTerminal.incl.obj X with | CategoryTheory.WithTerminal.of x => F.obj x | CategoryTheory.WithTerminal.star => Z)
                              def CategoryTheory.WithTerminal.inclLift {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x Z) (hM : ∀ (x y : C) (f : x y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) :
                              CategoryTheory.WithTerminal.incl.comp (CategoryTheory.WithTerminal.lift F M hM) F

                              The isomorphism between incllift F _ _ with F.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[simp]
                                @[simp]
                                def CategoryTheory.WithTerminal.liftStar {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x Z) (hM : ∀ (x y : C) (f : x y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) :
                                (CategoryTheory.WithTerminal.lift F M hM).obj CategoryTheory.WithTerminal.star Z

                                The isomorphism between (lift F _ _).obj WithTerminal.star with Z.

                                Equations
                                Instances For
                                  theorem CategoryTheory.WithTerminal.lift_map_liftStar {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x Z) (hM : ∀ (x y : C) (f : x y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) (x : C) :
                                  CategoryTheory.CategoryStruct.comp ((CategoryTheory.WithTerminal.lift F M hM).map (CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.incl.obj x))) (CategoryTheory.WithTerminal.liftStar F M hM).hom = CategoryTheory.CategoryStruct.comp ((CategoryTheory.WithTerminal.inclLift F M hM).hom.app x) (M x)
                                  def CategoryTheory.WithTerminal.liftUnique {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x Z) (hM : ∀ (x y : C) (f : x y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (h : CategoryTheory.WithTerminal.incl.comp G F) (hG : G.obj CategoryTheory.WithTerminal.star Z) (hh : ∀ (x : C), CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.incl.obj x))) hG.hom = CategoryTheory.CategoryStruct.comp (h.hom.app x) (M x)) :

                                  The uniqueness of lift.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[simp]
                                    theorem CategoryTheory.WithTerminal.liftToTerminal_map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) {X : CategoryTheory.WithTerminal C} {Y : CategoryTheory.WithTerminal C} (f : X Y) :
                                    (CategoryTheory.WithTerminal.liftToTerminal F hZ).map f = match X, Y, f with | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.of y, f => F.map (CategoryTheory.WithTerminal.down f) | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => hZ.from (F.obj x) | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id Z
                                    @[simp]
                                    theorem CategoryTheory.WithTerminal.inclLiftToTerminal_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) (X : C) :
                                    (CategoryTheory.WithTerminal.inclLiftToTerminal F hZ).hom.app X = CategoryTheory.CategoryStruct.id (match CategoryTheory.WithTerminal.incl.obj X with | CategoryTheory.WithTerminal.of x => F.obj x | CategoryTheory.WithTerminal.star => Z)

                                    A variant of incl_lift with Z a terminal object.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem CategoryTheory.WithTerminal.liftToTerminalUnique_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (h : CategoryTheory.WithTerminal.incl.comp G F) (hG : G.obj CategoryTheory.WithTerminal.star Z) (X : CategoryTheory.WithTerminal C) :
                                      (CategoryTheory.WithTerminal.liftToTerminalUnique F hZ G h hG).inv.app X = (match X with | CategoryTheory.WithTerminal.of x => h.app x | CategoryTheory.WithTerminal.star => hG).inv
                                      @[simp]
                                      theorem CategoryTheory.WithTerminal.liftToTerminalUnique_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (h : CategoryTheory.WithTerminal.incl.comp G F) (hG : G.obj CategoryTheory.WithTerminal.star Z) (X : CategoryTheory.WithTerminal C) :
                                      (CategoryTheory.WithTerminal.liftToTerminalUnique F hZ G h hG).hom.app X = (match X with | CategoryTheory.WithTerminal.of x => h.app x | CategoryTheory.WithTerminal.star => hG).hom
                                      def CategoryTheory.WithTerminal.liftToTerminalUnique {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z) (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (h : CategoryTheory.WithTerminal.incl.comp G F) (hG : G.obj CategoryTheory.WithTerminal.star Z) :

                                      A variant of lift_unique with Z a terminal object.

                                      Equations
                                      Instances For
                                        def CategoryTheory.WithTerminal.homFrom {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) :
                                        CategoryTheory.WithTerminal.incl.obj X CategoryTheory.WithTerminal.star

                                        Constructs a morphism to star from of X.

                                        Equations
                                        Instances For
                                          Equations
                                          • =

                                          Morphisms for WithInitial C.

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

                                            Identity morphisms for WithInitial C.

                                            Equations
                                            Instances For

                                              Composition of morphisms for WithInitial C.

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

                                                Helper function for typechecking.

                                                Equations
                                                Instances For

                                                  The inclusion of C into WithInitial C.

                                                  Equations
                                                  • CategoryTheory.WithInitial.incl = { obj := CategoryTheory.WithInitial.of, map := fun {X Y : C} (f : X Y) => f, map_id := , map_comp := }
                                                  Instances For
                                                    instance CategoryTheory.WithInitial.instFullIncl {C : Type u} [CategoryTheory.Category.{v, u} C] :
                                                    CategoryTheory.WithInitial.incl.Full
                                                    Equations
                                                    • =
                                                    instance CategoryTheory.WithInitial.instFaithfulIncl {C : Type u} [CategoryTheory.Category.{v, u} C] :
                                                    CategoryTheory.WithInitial.incl.Faithful
                                                    Equations
                                                    • =
                                                    @[simp]
                                                    theorem CategoryTheory.WithInitial.map_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (F : CategoryTheory.Functor C D) (X : CategoryTheory.WithInitial C) :
                                                    (CategoryTheory.WithInitial.map F).obj X = match X with | CategoryTheory.WithInitial.of x => CategoryTheory.WithInitial.of (F.obj x) | CategoryTheory.WithInitial.star => CategoryTheory.WithInitial.star
                                                    @[simp]
                                                    theorem CategoryTheory.WithInitial.map_map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (F : CategoryTheory.Functor C D) {X : CategoryTheory.WithInitial C} {Y : CategoryTheory.WithInitial C} (f : X Y) :
                                                    (CategoryTheory.WithInitial.map F).map f = match X, Y, f with | CategoryTheory.WithInitial.of x, CategoryTheory.WithInitial.of y, f => F.map (CategoryTheory.WithInitial.down f) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => PUnit.unit | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => PUnit.unit

                                                    Map WithInitial with respect to a functor F : C ⥤ D.

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

                                                      A natural isomorphism between the functor map (𝟭 C) and 𝟭 (WithInitial C).

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

                                                        A natural isomorphism between the functor map (F ⋙ G) and map F ⋙ map G .

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          @[simp]
                                                          theorem CategoryTheory.WithInitial.map₂_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (η : F G) (X : CategoryTheory.WithInitial C) :
                                                          (CategoryTheory.WithInitial.map₂ η).app X = match X with | CategoryTheory.WithInitial.of x => η.app x | CategoryTheory.WithInitial.star => CategoryTheory.CategoryStruct.id CategoryTheory.WithInitial.star

                                                          From a natrual transformation of functors C ⥤ D, the induced natural transformation of functors WithInitial C ⥤ WithInitial D.

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

                                                            The prelax functor from Cat to Cat defined with WithInitial.

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

                                                              The pseudofunctor from Cat to Cat defined with WithInitial.

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

                                                                WithInitial.star is initial.

                                                                Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem CategoryTheory.WithInitial.lift_map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z F.obj x) (hM : ∀ (x y : C) (f : x y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) {X : CategoryTheory.WithInitial C} {Y : CategoryTheory.WithInitial C} (f : X Y) :
                                                                  (CategoryTheory.WithInitial.lift F M hM).map f = match X, Y, f with | CategoryTheory.WithInitial.of x, CategoryTheory.WithInitial.of y, f => F.map (CategoryTheory.WithInitial.down f) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of x, x_1 => M x | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => CategoryTheory.CategoryStruct.id ((fun (X : CategoryTheory.WithInitial C) => match X with | CategoryTheory.WithInitial.of x => F.obj x | CategoryTheory.WithInitial.star => Z) CategoryTheory.WithInitial.star)
                                                                  @[simp]
                                                                  theorem CategoryTheory.WithInitial.lift_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z F.obj x) (hM : ∀ (x y : C) (f : x y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) (X : CategoryTheory.WithInitial C) :
                                                                  (CategoryTheory.WithInitial.lift F M hM).obj X = match X with | CategoryTheory.WithInitial.of x => F.obj x | CategoryTheory.WithInitial.star => Z
                                                                  def CategoryTheory.WithInitial.lift {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z F.obj x) (hM : ∀ (x y : C) (f : x y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) :

                                                                  Lift a functor F : C ⥤ D to WithInitial C ⥤ D.

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem CategoryTheory.WithInitial.inclLift_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z F.obj x) (hM : ∀ (x y : C) (f : x y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) (X : C) :
                                                                    (CategoryTheory.WithInitial.inclLift F M hM).hom.app X = CategoryTheory.CategoryStruct.id (match CategoryTheory.WithInitial.incl.obj X with | CategoryTheory.WithInitial.of x => F.obj x | CategoryTheory.WithInitial.star => Z)
                                                                    @[simp]
                                                                    theorem CategoryTheory.WithInitial.inclLift_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z F.obj x) (hM : ∀ (x y : C) (f : x y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) (X : C) :
                                                                    def CategoryTheory.WithInitial.inclLift {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z F.obj x) (hM : ∀ (x y : C) (f : x y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) :
                                                                    CategoryTheory.WithInitial.incl.comp (CategoryTheory.WithInitial.lift F M hM) F

                                                                    The isomorphism between incllift F _ _ with F.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      @[simp]
                                                                      @[simp]
                                                                      def CategoryTheory.WithInitial.liftStar {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z F.obj x) (hM : ∀ (x y : C) (f : x y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) :
                                                                      (CategoryTheory.WithInitial.lift F M hM).obj CategoryTheory.WithInitial.star Z

                                                                      The isomorphism between (lift F _ _).obj WithInitial.star with Z.

                                                                      Equations
                                                                      Instances For
                                                                        theorem CategoryTheory.WithInitial.liftStar_lift_map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z F.obj x) (hM : ∀ (x y : C) (f : x y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) (x : C) :
                                                                        CategoryTheory.CategoryStruct.comp (CategoryTheory.WithInitial.liftStar F M hM).hom ((CategoryTheory.WithInitial.lift F M hM).map (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.incl.obj x))) = CategoryTheory.CategoryStruct.comp (M x) ((CategoryTheory.WithInitial.inclLift F M hM).hom.app x)
                                                                        def CategoryTheory.WithInitial.liftUnique {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z F.obj x) (hM : ∀ (x y : C) (f : x y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y) (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (h : CategoryTheory.WithInitial.incl.comp G F) (hG : G.obj CategoryTheory.WithInitial.star Z) (hh : ∀ (x : C), CategoryTheory.CategoryStruct.comp hG.symm.hom (G.map (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.incl.obj x))) = CategoryTheory.CategoryStruct.comp (M x) (h.symm.hom.app x)) :

                                                                        The uniqueness of lift.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem CategoryTheory.WithInitial.liftToInitial_map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) {X : CategoryTheory.WithInitial C} {Y : CategoryTheory.WithInitial C} (f : X Y) :
                                                                          (CategoryTheory.WithInitial.liftToInitial F hZ).map f = match X, Y, f with | CategoryTheory.WithInitial.of x, CategoryTheory.WithInitial.of y, f => F.map (CategoryTheory.WithInitial.down f) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of x, x_1 => hZ.to (F.obj x) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => CategoryTheory.CategoryStruct.id Z
                                                                          @[simp]
                                                                          theorem CategoryTheory.WithInitial.inclLiftToInitial_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (X : C) :
                                                                          (CategoryTheory.WithInitial.inclLiftToInitial F hZ).hom.app X = CategoryTheory.CategoryStruct.id (match CategoryTheory.WithInitial.incl.obj X with | CategoryTheory.WithInitial.of x => F.obj x | CategoryTheory.WithInitial.star => Z)

                                                                          A variant of incl_lift with Z an initial object.

                                                                          Equations
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem CategoryTheory.WithInitial.liftToInitialUnique_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (h : CategoryTheory.WithInitial.incl.comp G F) (hG : G.obj CategoryTheory.WithInitial.star Z) (X : CategoryTheory.WithInitial C) :
                                                                            (CategoryTheory.WithInitial.liftToInitialUnique F hZ G h hG).hom.app X = (match X with | CategoryTheory.WithInitial.of x => h.app x | CategoryTheory.WithInitial.star => hG).hom
                                                                            @[simp]
                                                                            theorem CategoryTheory.WithInitial.liftToInitialUnique_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (h : CategoryTheory.WithInitial.incl.comp G F) (hG : G.obj CategoryTheory.WithInitial.star Z) (X : CategoryTheory.WithInitial C) :
                                                                            (CategoryTheory.WithInitial.liftToInitialUnique F hZ G h hG).inv.app X = (match X with | CategoryTheory.WithInitial.of x => h.app x | CategoryTheory.WithInitial.star => hG).inv
                                                                            def CategoryTheory.WithInitial.liftToInitialUnique {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (h : CategoryTheory.WithInitial.incl.comp G F) (hG : G.obj CategoryTheory.WithInitial.star Z) :

                                                                            A variant of lift_unique with Z an initial object.

                                                                            Equations
                                                                            Instances For
                                                                              def CategoryTheory.WithInitial.homTo {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) :
                                                                              CategoryTheory.WithInitial.star CategoryTheory.WithInitial.incl.obj X

                                                                              Constructs a morphism from star to of X.

                                                                              Equations
                                                                              Instances For
                                                                                Equations
                                                                                • =