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 }

      Identity morphisms for WithTerminal C.

      Equations
      Instances For

        Composition of morphisms for WithTerminal C.

        Equations
        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_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
            @[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

            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
                        • CategoryTheory.WithTerminal.instUniqueHomStar = { default := PUnit.unit, uniq := }
                        • CategoryTheory.WithTerminal.instUniqueHomStar = { default := PUnit.unit, uniq := }

                        WithTerminal.star is terminal.

                        Equations
                        Instances For
                          @[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
                          @[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
                          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_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
                                    @[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
                                    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
                                        • =

                                        Identity morphisms for WithInitial C.

                                        Equations
                                        Instances For

                                          Composition of morphisms for WithInitial C.

                                          Equations
                                          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 natural 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
                                                            • CategoryTheory.WithInitial.instUniqueHomStar = { default := PUnit.unit, uniq := }
                                                            • CategoryTheory.WithInitial.instUniqueHomStar = { default := PUnit.unit, uniq := }

                                                            WithInitial.star is initial.

                                                            Equations
                                                            Instances For
                                                              @[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
                                                              @[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)
                                                              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
                                                                            • =