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 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_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
                                        • =

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

                                                  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 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_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) :
                                                                @[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)
                                                                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_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
                                                                        @[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
                                                                        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
                                                                            • =