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 intro 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.

source
inductive CategoryTheory.WithTerminal (C : Type u) :
Type u

Formally adjoin a terminal object to a category.

Instances For
    source
    instance CategoryTheory.instInhabitedWithTerminal :
    {a : Type u_1} → Inhabited (CategoryTheory.WithTerminal a)
    Equations
    • CategoryTheory.instInhabitedWithTerminal = { default := CategoryTheory.WithTerminal.star }
    source
    inductive CategoryTheory.WithInitial (C : Type u) :
    Type u

    Formally adjoin an initial object to a category.

    Instances For
      source
      instance CategoryTheory.instInhabitedWithInitial :
      {a : Type u_1} → Inhabited (CategoryTheory.WithInitial a)
      Equations
      • CategoryTheory.instInhabitedWithInitial = { default := CategoryTheory.WithInitial.star }
      source
      def CategoryTheory.WithTerminal.Hom {C : Type u} [CategoryTheory.Category.{v, u} C] :
      CategoryTheory.WithTerminal C → CategoryTheory.WithTerminal C → Type v

      Morphisms for WithTerminal C.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def CategoryTheory.WithTerminal.id {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.WithTerminal C) :
        CategoryTheory.WithTerminal.Hom X X

        Identity morphisms for WithTerminal C.

        Equations
        Instances For
          source
          def CategoryTheory.WithTerminal.comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.WithTerminal C} {Y : CategoryTheory.WithTerminal C} {Z : CategoryTheory.WithTerminal C} :
          CategoryTheory.WithTerminal.Hom X Y → CategoryTheory.WithTerminal.Hom Y Z → CategoryTheory.WithTerminal.Hom X Z

          Composition of morphisms for WithTerminal C.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            instance CategoryTheory.WithTerminal.instCategoryWithTerminal {C : Type u} [CategoryTheory.Category.{v, u} C] :
            CategoryTheory.Category.{v, u} (CategoryTheory.WithTerminal C)
            Equations
            • CategoryTheory.WithTerminal.instCategoryWithTerminal = CategoryTheory.Category.mk
            source
            def CategoryTheory.WithTerminal.down {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : CategoryTheory.WithTerminal.of X ⟶ CategoryTheory.WithTerminal.of Y) :
            X ⟶ Y

            Helper function for typechecking.

            Equations
            Instances For
              source
              @[simp]
              theorem CategoryTheory.WithTerminal.down_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} :
              CategoryTheory.WithTerminal.down (CategoryTheory.CategoryStruct.id (CategoryTheory.WithTerminal.of X)) = CategoryTheory.CategoryStruct.id X
              source
              @[simp]
              theorem CategoryTheory.WithTerminal.down_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : CategoryTheory.WithTerminal.of X ⟶ CategoryTheory.WithTerminal.of Y) (g : CategoryTheory.WithTerminal.of Y ⟶ CategoryTheory.WithTerminal.of Z) :
              CategoryTheory.WithTerminal.down (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.WithTerminal.down f) (CategoryTheory.WithTerminal.down g)
              source
              theorem CategoryTheory.WithTerminal.false_of_from_star {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (f : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.of X) :
              False
              source
              def CategoryTheory.WithTerminal.incl {C : Type u} [CategoryTheory.Category.{v, u} C] :
              CategoryTheory.Functor C (CategoryTheory.WithTerminal C)

              The inclusion from C into WithTerminal C.

              Equations
              Instances For
                source
                instance CategoryTheory.WithTerminal.instFullWithTerminalInstCategoryWithTerminalIncl {C : Type u} [CategoryTheory.Category.{v, u} C] :
                CategoryTheory.Full CategoryTheory.WithTerminal.incl
                Equations
                • One or more equations did not get rendered due to their size.
                source
                instance CategoryTheory.WithTerminal.instFaithfulWithTerminalInstCategoryWithTerminalIncl {C : Type u} [CategoryTheory.Category.{v, u} C] :
                CategoryTheory.Faithful CategoryTheory.WithTerminal.incl
                Equations
                source
                def CategoryTheory.WithTerminal.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) :
                CategoryTheory.Functor (CategoryTheory.WithTerminal C) (CategoryTheory.WithTerminal D)

                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
                  source
                  instance CategoryTheory.WithTerminal.instUniqueHomWithTerminalToQuiverToCategoryStructInstCategoryWithTerminalStar {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.WithTerminal C} :
                  Unique (X ⟶ CategoryTheory.WithTerminal.star)
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  def CategoryTheory.WithTerminal.starTerminal {C : Type u} [CategoryTheory.Category.{v, u} C] :
                  CategoryTheory.Limits.IsTerminal CategoryTheory.WithTerminal.star

                  WithTerminal.star is terminal.

                  Equations
                  Instances For
                    source
                    @[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.toPrefunctor.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f) (M y) = M x) (X : CategoryTheory.WithTerminal C) :
                    (CategoryTheory.WithTerminal.lift F M hM).toPrefunctor.obj X = match X with | CategoryTheory.WithTerminal.of x => F.toPrefunctor.obj x | CategoryTheory.WithTerminal.star => Z
                    source
                    @[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.toPrefunctor.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f) (M y) = M x) {X : CategoryTheory.WithTerminal C} {Y : CategoryTheory.WithTerminal C} (f : X ⟶ Y) :
                    (CategoryTheory.WithTerminal.lift F M hM).toPrefunctor.map f = match X, Y, f with | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.of y, f => F.toPrefunctor.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
                    source
                    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.toPrefunctor.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f) (M y) = M x) :
                    CategoryTheory.Functor (CategoryTheory.WithTerminal C) D

                    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
                      source
                      @[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.toPrefunctor.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f) (M y) = M x) (X : C) :
                      (CategoryTheory.WithTerminal.inclLift F M hM).hom.app X = CategoryTheory.CategoryStruct.id (match CategoryTheory.WithTerminal.incl.toPrefunctor.obj X with | CategoryTheory.WithTerminal.of x => F.toPrefunctor.obj x | CategoryTheory.WithTerminal.star => Z)
                      source
                      @[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.toPrefunctor.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f) (M y) = M x) (X : C) :
                      (CategoryTheory.WithTerminal.inclLift F M hM).inv.app X = CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)
                      source
                      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.toPrefunctor.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f) (M y) = M x) :
                      CategoryTheory.Functor.comp CategoryTheory.WithTerminal.incl (CategoryTheory.WithTerminal.lift F M hM) ≅ F

                      The isomorphism between incl ⋙ lift F _ _ with F.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        @[simp]
                        theorem CategoryTheory.WithTerminal.liftStar_inv {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.toPrefunctor.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f) (M y) = M x) :
                        (CategoryTheory.WithTerminal.liftStar F M hM).inv = CategoryTheory.CategoryStruct.id Z
                        source
                        @[simp]
                        theorem CategoryTheory.WithTerminal.liftStar_hom {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.toPrefunctor.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f) (M y) = M x) :
                        (CategoryTheory.WithTerminal.liftStar F M hM).hom = CategoryTheory.CategoryStruct.id Z
                        source
                        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.toPrefunctor.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f) (M y) = M x) :
                        (CategoryTheory.WithTerminal.lift F M hM).toPrefunctor.obj CategoryTheory.WithTerminal.star ≅ Z

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

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          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.toPrefunctor.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f) (M y) = M x) (x : C) :
                          CategoryTheory.CategoryStruct.comp ((CategoryTheory.WithTerminal.lift F M hM).toPrefunctor.map (CategoryTheory.Limits.IsTerminal.from CategoryTheory.WithTerminal.starTerminal (CategoryTheory.WithTerminal.incl.toPrefunctor.obj x))) (CategoryTheory.WithTerminal.liftStar F M hM).hom = CategoryTheory.CategoryStruct.comp ((CategoryTheory.WithTerminal.inclLift F M hM).hom.app x) (M x)
                          source
                          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.toPrefunctor.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.toPrefunctor.map f) (M y) = M x) (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (h : CategoryTheory.Functor.comp CategoryTheory.WithTerminal.incl G ≅ F) (hG : G.toPrefunctor.obj CategoryTheory.WithTerminal.star ≅ Z) (hh : ∀ (x : C), CategoryTheory.CategoryStruct.comp (G.toPrefunctor.map (CategoryTheory.Limits.IsTerminal.from CategoryTheory.WithTerminal.starTerminal (CategoryTheory.WithTerminal.incl.toPrefunctor.obj x))) hG.hom = CategoryTheory.CategoryStruct.comp (h.hom.app x) (M x)) :
                          G ≅ CategoryTheory.WithTerminal.lift F M hM

                          The uniqueness of lift.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            @[simp]
                            theorem CategoryTheory.WithTerminal.liftToTerminal_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) (hZ : CategoryTheory.Limits.IsTerminal Z) (X : CategoryTheory.WithTerminal C) :
                            (CategoryTheory.WithTerminal.liftToTerminal F hZ).toPrefunctor.obj X = match X with | CategoryTheory.WithTerminal.of x => F.toPrefunctor.obj x | CategoryTheory.WithTerminal.star => Z
                            source
                            @[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).toPrefunctor.map f = match X, Y, f with | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.of y, f => F.toPrefunctor.map (CategoryTheory.WithTerminal.down f) | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => CategoryTheory.Limits.IsTerminal.from hZ (F.toPrefunctor.obj x) | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id Z
                            source
                            def CategoryTheory.WithTerminal.liftToTerminal {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) :
                            CategoryTheory.Functor (CategoryTheory.WithTerminal C) D

                            A variant of lift with Z a terminal object.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              @[simp]
                              theorem CategoryTheory.WithTerminal.inclLiftToTerminal_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) (X : C) :
                              (CategoryTheory.WithTerminal.inclLiftToTerminal F hZ).inv.app X = CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)
                              source
                              @[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.toPrefunctor.obj X with | CategoryTheory.WithTerminal.of x => F.toPrefunctor.obj x | CategoryTheory.WithTerminal.star => Z)
                              source
                              def CategoryTheory.WithTerminal.inclLiftToTerminal {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) :
                              CategoryTheory.Functor.comp CategoryTheory.WithTerminal.incl (CategoryTheory.WithTerminal.liftToTerminal F hZ) ≅ F

                              A variant of incl_lift with Z a terminal object.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                @[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.Functor.comp CategoryTheory.WithTerminal.incl G ≅ F) (hG : G.toPrefunctor.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
                                source
                                @[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.Functor.comp CategoryTheory.WithTerminal.incl G ≅ F) (hG : G.toPrefunctor.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
                                source
                                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.Functor.comp CategoryTheory.WithTerminal.incl G ≅ F) (hG : G.toPrefunctor.obj CategoryTheory.WithTerminal.star ≅ Z) :
                                G ≅ CategoryTheory.WithTerminal.liftToTerminal F hZ

                                A variant of lift_unique with Z a terminal object.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  def CategoryTheory.WithTerminal.homFrom {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) :
                                  CategoryTheory.WithTerminal.incl.toPrefunctor.obj X ⟶ CategoryTheory.WithTerminal.star

                                  Constructs a morphism to star from of X.

                                  Equations
                                  Instances For
                                    source
                                    instance CategoryTheory.WithTerminal.isIso_of_from_star {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.WithTerminal C} (f : CategoryTheory.WithTerminal.star ⟶ X) :
                                    CategoryTheory.IsIso f
                                    Equations
                                    source
                                    def CategoryTheory.WithInitial.Hom {C : Type u} [CategoryTheory.Category.{v, u} C] :
                                    CategoryTheory.WithInitial C → CategoryTheory.WithInitial C → Type v

                                    Morphisms for WithInitial C.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      source
                                      def CategoryTheory.WithInitial.id {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.WithInitial C) :
                                      CategoryTheory.WithInitial.Hom X X

                                      Identity morphisms for WithInitial C.

                                      Equations
                                      Instances For
                                        source
                                        def CategoryTheory.WithInitial.comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.WithInitial C} {Y : CategoryTheory.WithInitial C} {Z : CategoryTheory.WithInitial C} :
                                        CategoryTheory.WithInitial.Hom X Y → CategoryTheory.WithInitial.Hom Y Z → CategoryTheory.WithInitial.Hom X Z

                                        Composition of morphisms for WithInitial C.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          source
                                          instance CategoryTheory.WithInitial.instCategoryWithInitial {C : Type u} [CategoryTheory.Category.{v, u} C] :
                                          CategoryTheory.Category.{v, u} (CategoryTheory.WithInitial C)
                                          Equations
                                          • CategoryTheory.WithInitial.instCategoryWithInitial = CategoryTheory.Category.mk
                                          source
                                          def CategoryTheory.WithInitial.down {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : CategoryTheory.WithInitial.of X ⟶ CategoryTheory.WithInitial.of Y) :
                                          X ⟶ Y

                                          Helper function for typechecking.

                                          Equations
                                          Instances For
                                            source
                                            @[simp]
                                            theorem CategoryTheory.WithInitial.down_id {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} :
                                            CategoryTheory.WithInitial.down (CategoryTheory.CategoryStruct.id (CategoryTheory.WithInitial.of X)) = CategoryTheory.CategoryStruct.id X
                                            source
                                            @[simp]
                                            theorem CategoryTheory.WithInitial.down_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : CategoryTheory.WithInitial.of X ⟶ CategoryTheory.WithInitial.of Y) (g : CategoryTheory.WithInitial.of Y ⟶ CategoryTheory.WithInitial.of Z) :
                                            CategoryTheory.WithInitial.down (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.WithInitial.down f) (CategoryTheory.WithInitial.down g)
                                            source
                                            theorem CategoryTheory.WithInitial.false_of_to_star {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (f : CategoryTheory.WithInitial.of X ⟶ CategoryTheory.WithInitial.star) :
                                            False
                                            source
                                            def CategoryTheory.WithInitial.incl {C : Type u} [CategoryTheory.Category.{v, u} C] :
                                            CategoryTheory.Functor C (CategoryTheory.WithInitial C)

                                            The inclusion of C into WithInitial C.

                                            Equations
                                            Instances For
                                              source
                                              instance CategoryTheory.WithInitial.instFullWithInitialInstCategoryWithInitialIncl {C : Type u} [CategoryTheory.Category.{v, u} C] :
                                              CategoryTheory.Full CategoryTheory.WithInitial.incl
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              source
                                              instance CategoryTheory.WithInitial.instFaithfulWithInitialInstCategoryWithInitialIncl {C : Type u} [CategoryTheory.Category.{v, u} C] :
                                              CategoryTheory.Faithful CategoryTheory.WithInitial.incl
                                              Equations
                                              source
                                              def CategoryTheory.WithInitial.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) :
                                              CategoryTheory.Functor (CategoryTheory.WithInitial C) (CategoryTheory.WithInitial D)

                                              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
                                                source
                                                instance CategoryTheory.WithInitial.instUniqueHomWithInitialToQuiverToCategoryStructInstCategoryWithInitialStar {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.WithInitial C} :
                                                Unique (CategoryTheory.WithInitial.star ⟶ X)
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                source
                                                def CategoryTheory.WithInitial.starInitial {C : Type u} [CategoryTheory.Category.{v, u} C] :
                                                CategoryTheory.Limits.IsInitial CategoryTheory.WithInitial.star

                                                WithInitial.star is initial.

                                                Equations
                                                Instances For
                                                  source
                                                  @[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.toPrefunctor.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.toPrefunctor.map f) = M y) {X : CategoryTheory.WithInitial C} {Y : CategoryTheory.WithInitial C} (f : X ⟶ Y) :
                                                  (CategoryTheory.WithInitial.lift F M hM).toPrefunctor.map f = match X, Y, f with | CategoryTheory.WithInitial.of x, CategoryTheory.WithInitial.of y, f => F.toPrefunctor.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.toPrefunctor.obj x | CategoryTheory.WithInitial.star => Z) CategoryTheory.WithInitial.star)
                                                  source
                                                  @[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.toPrefunctor.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.toPrefunctor.map f) = M y) (X : CategoryTheory.WithInitial C) :
                                                  (CategoryTheory.WithInitial.lift F M hM).toPrefunctor.obj X = match X with | CategoryTheory.WithInitial.of x => F.toPrefunctor.obj x | CategoryTheory.WithInitial.star => Z
                                                  source
                                                  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.toPrefunctor.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.toPrefunctor.map f) = M y) :
                                                  CategoryTheory.Functor (CategoryTheory.WithInitial C) D

                                                  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
                                                    source
                                                    @[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.toPrefunctor.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.toPrefunctor.map f) = M y) (X : C) :
                                                    (CategoryTheory.WithInitial.inclLift F M hM).inv.app X = CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)
                                                    source
                                                    @[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.toPrefunctor.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.toPrefunctor.map f) = M y) (X : C) :
                                                    (CategoryTheory.WithInitial.inclLift F M hM).hom.app X = CategoryTheory.CategoryStruct.id (match CategoryTheory.WithInitial.incl.toPrefunctor.obj X with | CategoryTheory.WithInitial.of x => F.toPrefunctor.obj x | CategoryTheory.WithInitial.star => Z)
                                                    source
                                                    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.toPrefunctor.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.toPrefunctor.map f) = M y) :
                                                    CategoryTheory.Functor.comp CategoryTheory.WithInitial.incl (CategoryTheory.WithInitial.lift F M hM) ≅ F

                                                    The isomorphism between incl ⋙ lift F _ _ with F.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      source
                                                      @[simp]
                                                      theorem CategoryTheory.WithInitial.liftStar_inv {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.toPrefunctor.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.toPrefunctor.map f) = M y) :
                                                      (CategoryTheory.WithInitial.liftStar F M hM).inv = CategoryTheory.CategoryStruct.id Z
                                                      source
                                                      @[simp]
                                                      theorem CategoryTheory.WithInitial.liftStar_hom {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.toPrefunctor.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.toPrefunctor.map f) = M y) :
                                                      (CategoryTheory.WithInitial.liftStar F M hM).hom = CategoryTheory.CategoryStruct.id Z
                                                      source
                                                      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.toPrefunctor.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.toPrefunctor.map f) = M y) :
                                                      (CategoryTheory.WithInitial.lift F M hM).toPrefunctor.obj CategoryTheory.WithInitial.star ≅ Z

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

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        source
                                                        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.toPrefunctor.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.toPrefunctor.map f) = M y) (x : C) :
                                                        CategoryTheory.CategoryStruct.comp (CategoryTheory.WithInitial.liftStar F M hM).hom ((CategoryTheory.WithInitial.lift F M hM).toPrefunctor.map (CategoryTheory.Limits.IsInitial.to CategoryTheory.WithInitial.starInitial (CategoryTheory.WithInitial.incl.toPrefunctor.obj x))) = CategoryTheory.CategoryStruct.comp (M x) ((CategoryTheory.WithInitial.inclLift F M hM).hom.app x)
                                                        source
                                                        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.toPrefunctor.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.toPrefunctor.map f) = M y) (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (h : CategoryTheory.Functor.comp CategoryTheory.WithInitial.incl G ≅ F) (hG : G.toPrefunctor.obj CategoryTheory.WithInitial.star ≅ Z) (hh : ∀ (x : C), CategoryTheory.CategoryStruct.comp hG.symm.hom (G.toPrefunctor.map (CategoryTheory.Limits.IsInitial.to CategoryTheory.WithInitial.starInitial (CategoryTheory.WithInitial.incl.toPrefunctor.obj x))) = CategoryTheory.CategoryStruct.comp (M x) (h.symm.hom.app x)) :
                                                        G ≅ CategoryTheory.WithInitial.lift F M hM

                                                        The uniqueness of lift.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          source
                                                          @[simp]
                                                          theorem CategoryTheory.WithInitial.liftToInitial_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) (hZ : CategoryTheory.Limits.IsInitial Z) (X : CategoryTheory.WithInitial C) :
                                                          (CategoryTheory.WithInitial.liftToInitial F hZ).toPrefunctor.obj X = match X with | CategoryTheory.WithInitial.of x => F.toPrefunctor.obj x | CategoryTheory.WithInitial.star => Z
                                                          source
                                                          @[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).toPrefunctor.map f = match X, Y, f with | CategoryTheory.WithInitial.of x, CategoryTheory.WithInitial.of y, f => F.toPrefunctor.map (CategoryTheory.WithInitial.down f) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of x, x_1 => CategoryTheory.Limits.IsInitial.to hZ (F.toPrefunctor.obj x) | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => CategoryTheory.CategoryStruct.id Z
                                                          source
                                                          def CategoryTheory.WithInitial.liftToInitial {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) :
                                                          CategoryTheory.Functor (CategoryTheory.WithInitial C) D

                                                          A variant of lift with Z an initial object.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            source
                                                            @[simp]
                                                            theorem CategoryTheory.WithInitial.inclLiftToInitial_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) (X : C) :
                                                            (CategoryTheory.WithInitial.inclLiftToInitial F hZ).inv.app X = CategoryTheory.CategoryStruct.id (F.toPrefunctor.obj X)
                                                            source
                                                            @[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.toPrefunctor.obj X with | CategoryTheory.WithInitial.of x => F.toPrefunctor.obj x | CategoryTheory.WithInitial.star => Z)
                                                            source
                                                            def CategoryTheory.WithInitial.inclLiftToInitial {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) :
                                                            CategoryTheory.Functor.comp CategoryTheory.WithInitial.incl (CategoryTheory.WithInitial.liftToInitial F hZ) ≅ F

                                                            A variant of incl_lift with Z an initial object.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              source
                                                              @[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.Functor.comp CategoryTheory.WithInitial.incl G ≅ F) (hG : G.toPrefunctor.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
                                                              source
                                                              @[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.Functor.comp CategoryTheory.WithInitial.incl G ≅ F) (hG : G.toPrefunctor.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
                                                              source
                                                              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.Functor.comp CategoryTheory.WithInitial.incl G ≅ F) (hG : G.toPrefunctor.obj CategoryTheory.WithInitial.star ≅ Z) :
                                                              G ≅ CategoryTheory.WithInitial.liftToInitial F hZ

                                                              A variant of lift_unique with Z an initial object.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                source
                                                                def CategoryTheory.WithInitial.homTo {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) :
                                                                CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.incl.toPrefunctor.obj X

                                                                Constructs a morphism from star to of X.

                                                                Equations
                                                                Instances For
                                                                  source
                                                                  instance CategoryTheory.WithInitial.isIso_of_to_star {C : Type u} [CategoryTheory.Category.{v, u} C] {X : CategoryTheory.WithInitial C} (f : X ⟶ CategoryTheory.WithInitial.star) :
                                                                  CategoryTheory.IsIso f
                                                                  Equations