mathlib3 documentation

category_theory.with_terminal

with_initial and with_terminal #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Given a category C, this file constructs two objects:

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

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

The inclusion from C intro with_terminal C resp. with_initial C is denoted with_terminal.incl resp. with_initial.incl.

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

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

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

source
@[protected, instance]
def category_theory.with_terminal.inhabited (C : Type u) [a : inhabited C] [category_theory.category C] :
inhabited (category_theory.with_terminal C)
source
inductive category_theory.with_terminal (C : Type u) [category_theory.category C] :
Type u

Formally adjoin a terminal object to a category.

Instances for category_theory.with_terminal
source
inductive category_theory.with_initial (C : Type u) [category_theory.category C] :
Type u

Formally adjoin an initial object to a category.

Instances for category_theory.with_initial
source
@[protected, instance]
def category_theory.with_initial.inhabited (C : Type u) [a : inhabited C] [category_theory.category C] :
inhabited (category_theory.with_initial C)
source
@[simp, nolint]
def category_theory.with_terminal.hom {C : Type u} [category_theory.category C] :
category_theory.with_terminal C → category_theory.with_terminal C → Type v

Morphisms for with_terminal C.

Equations
source
@[simp]
def category_theory.with_terminal.id {C : Type u} [category_theory.category C] (X : category_theory.with_terminal C) :
X.hom X

Identity morphisms for with_terminal C.

Equations
source
@[simp]
def category_theory.with_terminal.comp {C : Type u} [category_theory.category C] {X Y Z : category_theory.with_terminal C} :
X.hom Y → Y.hom Z → X.hom Z

Composition of morphisms for with_terminal C.

Equations
source
@[protected, instance]
def category_theory.with_terminal.category_theory.category {C : Type u} [category_theory.category C] :
category_theory.category (category_theory.with_terminal C)
Equations
source
def category_theory.with_terminal.incl {C : Type u} [category_theory.category C] :
C ⥤ category_theory.with_terminal C

The inclusion from C into with_terminal C.

Equations
Instances for category_theory.with_terminal.incl
source
@[protected, instance]
def category_theory.with_terminal.incl.category_theory.full {C : Type u} [category_theory.category C] :
category_theory.full category_theory.with_terminal.incl
Equations
source
@[protected, instance]
def category_theory.with_terminal.incl.category_theory.faithful {C : Type u} [category_theory.category C] :
category_theory.faithful category_theory.with_terminal.incl
source
def category_theory.with_terminal.map {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] (F : C ⥤ D) :
category_theory.with_terminal C ⥤ category_theory.with_terminal D

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

Equations
source
@[protected, instance]
def category_theory.with_terminal.quiver.hom.unique {C : Type u} [category_theory.category C] {X : category_theory.with_terminal C} :
unique (X ⟶ category_theory.with_terminal.star)
Equations
source
def category_theory.with_terminal.star_terminal {C : Type u} [category_theory.category C] :
category_theory.limits.is_terminal category_theory.with_terminal.star

with_terminal.star is terminal.

Equations
source
@[simp]
theorem category_theory.with_terminal.lift_obj {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x) (X : category_theory.with_terminal C) :
(category_theory.with_terminal.lift F M hM).obj X = category_theory.with_terminal.lift._match_1 F X
source
def category_theory.with_terminal.lift {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x) :
category_theory.with_terminal C ⥤ D

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

Equations
source
@[simp]
theorem category_theory.with_terminal.lift_map {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x) (X Y : category_theory.with_terminal C) (f : X ⟶ Y) :
(category_theory.with_terminal.lift F M hM).map f = category_theory.with_terminal.lift._match_2 F M X Y f
source
@[simp]
theorem category_theory.with_terminal.incl_lift_hom_app {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x) (X : C) :
(category_theory.with_terminal.incl_lift F M hM).hom.app X = 𝟙 ((category_theory.with_terminal.incl ⋙ category_theory.with_terminal.lift F M hM).obj X)
source
@[simp]
theorem category_theory.with_terminal.incl_lift_inv_app {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x) (X : C) :
(category_theory.with_terminal.incl_lift F M hM).inv.app X = 𝟙 (F.obj X)
source
def category_theory.with_terminal.incl_lift {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x) :
category_theory.with_terminal.incl ⋙ category_theory.with_terminal.lift F M hM ≅ F

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

Equations
source
@[simp]
theorem category_theory.with_terminal.lift_star_hom {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x) :
(category_theory.with_terminal.lift_star F M hM).hom = 𝟙 (category_theory.with_terminal.lift._match_1 F category_theory.with_terminal.star)
source
def category_theory.with_terminal.lift_star {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x) :
(category_theory.with_terminal.lift F M hM).obj category_theory.with_terminal.star ≅ Z

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

Equations
source
@[simp]
theorem category_theory.with_terminal.lift_star_inv {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x) :
(category_theory.with_terminal.lift_star F M hM).inv = 𝟙 Z
source
theorem category_theory.with_terminal.lift_map_lift_star {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x) (x : C) :
(category_theory.with_terminal.lift F M hM).map (category_theory.with_terminal.star_terminal.from (category_theory.with_terminal.incl.obj x)) ≫ (category_theory.with_terminal.lift_star F M hM).hom = (category_theory.with_terminal.incl_lift F M hM).hom.app x ≫ M x
source
@[simp]
def category_theory.with_terminal.lift_unique {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), F.obj x ⟶ Z) (hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x) (G : category_theory.with_terminal C ⥤ D) (h : category_theory.with_terminal.incl ⋙ G ≅ F) (hG : G.obj category_theory.with_terminal.star ≅ Z) (hh : ∀ (x : C), G.map (category_theory.with_terminal.star_terminal.from (category_theory.with_terminal.incl.obj x)) ≫ hG.hom = h.hom.app x ≫ M x) :
G ≅ category_theory.with_terminal.lift F M hM

The uniqueness of lift.

Equations
source
def category_theory.with_terminal.lift_to_terminal {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (hZ : category_theory.limits.is_terminal Z) :
category_theory.with_terminal C ⥤ D

A variant of lift with Z a terminal object.

Equations
source
@[simp]
theorem category_theory.with_terminal.lift_to_terminal_obj {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (hZ : category_theory.limits.is_terminal Z) (X : category_theory.with_terminal C) :
(category_theory.with_terminal.lift_to_terminal F hZ).obj X = category_theory.with_terminal.lift._match_1 F X
source
@[simp]
theorem category_theory.with_terminal.lift_to_terminal_map {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (hZ : category_theory.limits.is_terminal Z) (X Y : category_theory.with_terminal C) (f : X ⟶ Y) :
(category_theory.with_terminal.lift_to_terminal F hZ).map f = category_theory.with_terminal.lift._match_2 F (λ (x : C), hZ.from (F.obj x)) X Y f
source
@[simp]
theorem category_theory.with_terminal.incl_lift_to_terminal_inv_app {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (hZ : category_theory.limits.is_terminal Z) (X : C) :
(category_theory.with_terminal.incl_lift_to_terminal F hZ).inv.app X = 𝟙 (F.obj X)
source
@[simp]
theorem category_theory.with_terminal.incl_lift_to_terminal_hom_app {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (hZ : category_theory.limits.is_terminal Z) (X : C) :
(category_theory.with_terminal.incl_lift_to_terminal F hZ).hom.app X = 𝟙 (category_theory.with_terminal.lift._match_1 F (category_theory.with_terminal.incl.obj X))
source
def category_theory.with_terminal.incl_lift_to_terminal {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (hZ : category_theory.limits.is_terminal Z) :
category_theory.with_terminal.incl ⋙ category_theory.with_terminal.lift_to_terminal F hZ ≅ F

A variant of incl_lift with Z a terminal object.

Equations
source
@[simp]
theorem category_theory.with_terminal.lift_to_terminal_unique_hom_app {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (hZ : category_theory.limits.is_terminal Z) (G : category_theory.with_terminal C ⥤ D) (h : category_theory.with_terminal.incl ⋙ G ≅ F) (hG : G.obj category_theory.with_terminal.star ≅ Z) (X : category_theory.with_terminal C) :
(category_theory.with_terminal.lift_to_terminal_unique F hZ G h hG).hom.app X = (category_theory.with_terminal.lift_unique._match_1 F (λ (z : C), hZ.from (F.obj z)) _ G h hG X).hom
source
@[simp]
theorem category_theory.with_terminal.lift_to_terminal_unique_inv_app {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (hZ : category_theory.limits.is_terminal Z) (G : category_theory.with_terminal C ⥤ D) (h : category_theory.with_terminal.incl ⋙ G ≅ F) (hG : G.obj category_theory.with_terminal.star ≅ Z) (X : category_theory.with_terminal C) :
(category_theory.with_terminal.lift_to_terminal_unique F hZ G h hG).inv.app X = (category_theory.with_terminal.lift_unique._match_1 F (λ (z : C), hZ.from (F.obj z)) _ G h hG X).inv
source
def category_theory.with_terminal.lift_to_terminal_unique {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (hZ : category_theory.limits.is_terminal Z) (G : category_theory.with_terminal C ⥤ D) (h : category_theory.with_terminal.incl ⋙ G ≅ F) (hG : G.obj category_theory.with_terminal.star ≅ Z) :
G ≅ category_theory.with_terminal.lift_to_terminal F hZ

A variant of lift_unique with Z a terminal object.

Equations
source
@[simp]
def category_theory.with_terminal.hom_from {C : Type u} [category_theory.category C] (X : C) :
category_theory.with_terminal.incl.obj X ⟶ category_theory.with_terminal.star

Constructs a morphism to star from of X.

Equations
source
@[protected, instance]
def category_theory.with_terminal.is_iso_of_from_star {C : Type u} [category_theory.category C] {X : category_theory.with_terminal C} (f : category_theory.with_terminal.star ⟶ X) :
category_theory.is_iso f
source
@[simp, nolint]
def category_theory.with_initial.hom {C : Type u} [category_theory.category C] :
category_theory.with_initial C → category_theory.with_initial C → Type v

Morphisms for with_initial C.

Equations
source
@[simp]
def category_theory.with_initial.id {C : Type u} [category_theory.category C] (X : category_theory.with_initial C) :
X.hom X

Identity morphisms for with_initial C.

Equations
source
@[simp]
def category_theory.with_initial.comp {C : Type u} [category_theory.category C] {X Y Z : category_theory.with_initial C} :
X.hom Y → Y.hom Z → X.hom Z

Composition of morphisms for with_initial C.

Equations
source
@[protected, instance]
def category_theory.with_initial.category_theory.category {C : Type u} [category_theory.category C] :
category_theory.category (category_theory.with_initial C)
Equations
source
def category_theory.with_initial.incl {C : Type u} [category_theory.category C] :
C ⥤ category_theory.with_initial C

The inclusion of C into with_initial C.

Equations
Instances for category_theory.with_initial.incl
source
@[protected, instance]
def category_theory.with_initial.incl.category_theory.full {C : Type u} [category_theory.category C] :
category_theory.full category_theory.with_initial.incl
Equations
source
@[protected, instance]
def category_theory.with_initial.incl.category_theory.faithful {C : Type u} [category_theory.category C] :
category_theory.faithful category_theory.with_initial.incl
source
def category_theory.with_initial.map {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] (F : C ⥤ D) :
category_theory.with_initial C ⥤ category_theory.with_initial D

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

Equations
source
@[protected, instance]
def category_theory.with_initial.quiver.hom.unique {C : Type u} [category_theory.category C] {X : category_theory.with_initial C} :
unique (category_theory.with_initial.star ⟶ X)
Equations
source
def category_theory.with_initial.star_initial {C : Type u} [category_theory.category C] :
category_theory.limits.is_initial category_theory.with_initial.star

with_initial.star is initial.

Equations
source
def category_theory.with_initial.lift {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y) :
category_theory.with_initial C ⥤ D

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

Equations
source
@[simp]
theorem category_theory.with_initial.lift_map {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y) (X Y : category_theory.with_initial C) (f : X ⟶ Y) :
(category_theory.with_initial.lift F M hM).map f = category_theory.with_initial.lift._match_2 F M X Y f
source
@[simp]
theorem category_theory.with_initial.lift_obj {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y) (X : category_theory.with_initial C) :
(category_theory.with_initial.lift F M hM).obj X = category_theory.with_initial.lift._match_1 F X
source
@[simp]
theorem category_theory.with_initial.incl_lift_hom_app {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y) (X : C) :
(category_theory.with_initial.incl_lift F M hM).hom.app X = 𝟙 ((category_theory.with_initial.incl ⋙ category_theory.with_initial.lift F M hM).obj X)
source
@[simp]
theorem category_theory.with_initial.incl_lift_inv_app {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y) (X : C) :
(category_theory.with_initial.incl_lift F M hM).inv.app X = 𝟙 (F.obj X)
source
def category_theory.with_initial.incl_lift {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y) :
category_theory.with_initial.incl ⋙ category_theory.with_initial.lift F M hM ≅ F

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

Equations
source
@[simp]
theorem category_theory.with_initial.lift_star_inv {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y) :
(category_theory.with_initial.lift_star F M hM).inv = 𝟙 Z
source
def category_theory.with_initial.lift_star {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y) :
(category_theory.with_initial.lift F M hM).obj category_theory.with_initial.star ≅ Z

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

Equations
source
@[simp]
theorem category_theory.with_initial.lift_star_hom {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y) :
(category_theory.with_initial.lift_star F M hM).hom = 𝟙 (category_theory.with_initial.lift._match_1 F category_theory.with_initial.star)
source
theorem category_theory.with_initial.lift_star_lift_map {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y) (x : C) :
(category_theory.with_initial.lift_star F M hM).hom ≫ (category_theory.with_initial.lift F M hM).map (category_theory.with_initial.star_initial.to (category_theory.with_initial.incl.obj x)) = M x ≫ (category_theory.with_initial.incl_lift F M hM).hom.app x
source
@[simp]
def category_theory.with_initial.lift_unique {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (M : Π (x : C), Z ⟶ F.obj x) (hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y) (G : category_theory.with_initial C ⥤ D) (h : category_theory.with_initial.incl ⋙ G ≅ F) (hG : G.obj category_theory.with_initial.star ≅ Z) (hh : ∀ (x : C), hG.symm.hom ≫ G.map (category_theory.with_initial.star_initial.to (category_theory.with_initial.incl.obj x)) = M x ≫ h.symm.hom.app x) :
G ≅ category_theory.with_initial.lift F M hM

The uniqueness of lift.

Equations
source
def category_theory.with_initial.lift_to_initial {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (hZ : category_theory.limits.is_initial Z) :
category_theory.with_initial C ⥤ D

A variant of lift with Z an initial object.

Equations
source
@[simp]
theorem category_theory.with_initial.lift_to_initial_obj {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (hZ : category_theory.limits.is_initial Z) (X : category_theory.with_initial C) :
(category_theory.with_initial.lift_to_initial F hZ).obj X = category_theory.with_initial.lift._match_1 F X
source
@[simp]
theorem category_theory.with_initial.lift_to_initial_map {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (hZ : category_theory.limits.is_initial Z) (X Y : category_theory.with_initial C) (f : X ⟶ Y) :
(category_theory.with_initial.lift_to_initial F hZ).map f = category_theory.with_initial.lift._match_2 F (λ (x : C), hZ.to (F.obj x)) X Y f
source
@[simp]
theorem category_theory.with_initial.incl_lift_to_initial_hom_app {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (hZ : category_theory.limits.is_initial Z) (X : C) :
(category_theory.with_initial.incl_lift_to_initial F hZ).hom.app X = 𝟙 (category_theory.with_initial.lift._match_1 F (category_theory.with_initial.incl.obj X))
source
@[simp]
theorem category_theory.with_initial.incl_lift_to_initial_inv_app {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (hZ : category_theory.limits.is_initial Z) (X : C) :
(category_theory.with_initial.incl_lift_to_initial F hZ).inv.app X = 𝟙 (F.obj X)
source
def category_theory.with_initial.incl_lift_to_initial {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (hZ : category_theory.limits.is_initial Z) :
category_theory.with_initial.incl ⋙ category_theory.with_initial.lift_to_initial F hZ ≅ F

A variant of incl_lift with Z an initial object.

Equations
source
def category_theory.with_initial.lift_to_initial_unique {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (hZ : category_theory.limits.is_initial Z) (G : category_theory.with_initial C ⥤ D) (h : category_theory.with_initial.incl ⋙ G ≅ F) (hG : G.obj category_theory.with_initial.star ≅ Z) :
G ≅ category_theory.with_initial.lift_to_initial F hZ

A variant of lift_unique with Z an initial object.

Equations
source
@[simp]
theorem category_theory.with_initial.lift_to_initial_unique_inv_app {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (hZ : category_theory.limits.is_initial Z) (G : category_theory.with_initial C ⥤ D) (h : category_theory.with_initial.incl ⋙ G ≅ F) (hG : G.obj category_theory.with_initial.star ≅ Z) (X : category_theory.with_initial C) :
(category_theory.with_initial.lift_to_initial_unique F hZ G h hG).inv.app X = (category_theory.with_initial.lift_unique._match_1 F (λ (z : C), hZ.to (F.obj z)) _ G h hG X).inv
source
@[simp]
theorem category_theory.with_initial.lift_to_initial_unique_hom_app {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {Z : D} (F : C ⥤ D) (hZ : category_theory.limits.is_initial Z) (G : category_theory.with_initial C ⥤ D) (h : category_theory.with_initial.incl ⋙ G ≅ F) (hG : G.obj category_theory.with_initial.star ≅ Z) (X : category_theory.with_initial C) :
(category_theory.with_initial.lift_to_initial_unique F hZ G h hG).hom.app X = (category_theory.with_initial.lift_unique._match_1 F (λ (z : C), hZ.to (F.obj z)) _ G h hG X).hom
source
@[simp]
def category_theory.with_initial.hom_to {C : Type u} [category_theory.category C] (X : C) :
category_theory.with_initial.star ⟶ category_theory.with_initial.incl.obj X

Constructs a morphism from star to of X.

Equations
source
@[protected, instance]
def category_theory.with_initial.is_iso_of_to_star {C : Type u} [category_theory.category C] {X : category_theory.with_initial C} (f : X ⟶ category_theory.with_initial.star) :
category_theory.is_iso f