# mathlib3documentation

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.

@[protected, instance]
inductive category_theory.with_terminal (C : Type u)  :
• of : Π {C : Type u} [_inst_1 : ,
• star : Π {C : Type u} [_inst_1 : ,

Formally adjoin a terminal object to a category.

Instances for category_theory.with_terminal
inductive category_theory.with_initial (C : Type u)  :
• of : Π {C : Type u} [_inst_1 : ,
• star : Π {C : Type u} [_inst_1 : ,

Formally adjoin an initial object to a category.

Instances for category_theory.with_initial
@[protected, instance]
@[simp, nolint]

Morphisms for with_terminal C.

Equations
@[simp]

Identity morphisms for with_terminal C.

Equations
@[simp]

Composition of morphisms for with_terminal C.

Equations
@[protected, instance]
Equations

The inclusion from C into with_terminal C.

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

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

Equations
@[protected, instance]
Equations

with_terminal.star is terminal.

Equations
@[simp]
theorem category_theory.with_terminal.lift_obj {C : Type u} {D : Type u_1} {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)  :
.obj X = category_theory.with_terminal.lift._match_1 F X
def category_theory.with_terminal.lift {C : Type u} {D : Type u_1} {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) :

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

Equations
@[simp]
theorem category_theory.with_terminal.lift_map {C : Type u} {D : Type u_1} {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) :
.map f = category_theory.with_terminal.lift._match_2 F M X Y f
@[simp]
theorem category_theory.with_terminal.incl_lift_hom_app {C : Type u} {D : Type u_1} {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) :
X =
@[simp]
theorem category_theory.with_terminal.incl_lift_inv_app {C : Type u} {D : Type u_1} {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) :
X = 𝟙 (F.obj X)
def category_theory.with_terminal.incl_lift {C : Type u} {D : Type u_1} {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) :

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

Equations
@[simp]
theorem category_theory.with_terminal.lift_star_hom {C : Type u} {D : Type u_1} {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._match_1 F category_theory.with_terminal.star)
def category_theory.with_terminal.lift_star {C : Type u} {D : Type u_1} {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) :

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

Equations
@[simp]
theorem category_theory.with_terminal.lift_star_inv {C : Type u} {D : Type u_1} {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) :
= 𝟙 Z
theorem category_theory.with_terminal.lift_map_lift_star {C : Type u} {D : Type u_1} {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) :
@[simp]
def category_theory.with_terminal.lift_unique {C : Type u} {D : Type u_1} {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 : D) (h : F) (hG : Z) (hh : (x : C), = h.hom.app x M x) :

The uniqueness of lift.

Equations
def category_theory.with_terminal.lift_to_terminal {C : Type u} {D : Type u_1} {Z : D} (F : C D)  :

A variant of lift with Z a terminal object.

Equations
@[simp]
theorem category_theory.with_terminal.lift_to_terminal_obj {C : Type u} {D : Type u_1} {Z : D} (F : C D)  :
= category_theory.with_terminal.lift._match_1 F X
@[simp]
theorem category_theory.with_terminal.lift_to_terminal_map {C : Type u} {D : Type u_1} {Z : D} (F : C D) (X Y : category_theory.with_terminal C) (f : X Y) :
= category_theory.with_terminal.lift._match_2 F (λ (x : C), hZ.from (F.obj x)) X Y f
@[simp]
theorem category_theory.with_terminal.incl_lift_to_terminal_inv_app {C : Type u} {D : Type u_1} {Z : D} (F : C D) (X : C) :
= 𝟙 (F.obj X)
@[simp]
theorem category_theory.with_terminal.incl_lift_to_terminal_hom_app {C : Type u} {D : Type u_1} {Z : D} (F : C D) (X : C) :
= 𝟙 (category_theory.with_terminal.lift._match_1 F
def category_theory.with_terminal.incl_lift_to_terminal {C : Type u} {D : Type u_1} {Z : D} (F : C D)  :

A variant of incl_lift with Z a terminal object.

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

A variant of lift_unique with Z a terminal object.

Equations
• = (λ (z : C), hZ.from (F.obj z)) _ G h hG _
@[simp]

Constructs a morphism to star from of X.

Equations
@[protected, instance]
@[simp, nolint]

Morphisms for with_initial C.

Equations
@[simp]

Identity morphisms for with_initial C.

Equations
@[simp]

Composition of morphisms for with_initial C.

Equations
@[protected, instance]
Equations

The inclusion of C into with_initial C.

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

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

Equations
@[protected, instance]
Equations

with_initial.star is initial.

Equations
def category_theory.with_initial.lift {C : Type u} {D : Type u_1} {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) :

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

Equations
@[simp]
theorem category_theory.with_initial.lift_map {C : Type u} {D : Type u_1} {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) :
.map f = category_theory.with_initial.lift._match_2 F M X Y f
@[simp]
theorem category_theory.with_initial.lift_obj {C : Type u} {D : Type u_1} {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)  :
.obj X = category_theory.with_initial.lift._match_1 F X
@[simp]
theorem category_theory.with_initial.incl_lift_hom_app {C : Type u} {D : Type u_1} {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) :
.app X =
@[simp]
theorem category_theory.with_initial.incl_lift_inv_app {C : Type u} {D : Type u_1} {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) :
.app X = 𝟙 (F.obj X)
def category_theory.with_initial.incl_lift {C : Type u} {D : Type u_1} {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) :

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

Equations
@[simp]
theorem category_theory.with_initial.lift_star_inv {C : Type u} {D : Type u_1} {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) :
= 𝟙 Z
def category_theory.with_initial.lift_star {C : Type u} {D : Type u_1} {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) :

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

Equations
@[simp]
theorem category_theory.with_initial.lift_star_hom {C : Type u} {D : Type u_1} {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._match_1 F category_theory.with_initial.star)
theorem category_theory.with_initial.lift_star_lift_map {C : Type u} {D : Type u_1} {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) :
@[simp]
def category_theory.with_initial.lift_unique {C : Type u} {D : Type u_1} {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 : D) (h : F) (hG : Z) (hh : (x : C), = M x h.symm.hom.app x) :

The uniqueness of lift.

Equations
def category_theory.with_initial.lift_to_initial {C : Type u} {D : Type u_1} {Z : D} (F : C D)  :

A variant of lift with Z an initial object.

Equations
• = (λ (x : C), hZ.to (F.obj x)) _
@[simp]
theorem category_theory.with_initial.lift_to_initial_obj {C : Type u} {D : Type u_1} {Z : D} (F : C D)  :
= category_theory.with_initial.lift._match_1 F X
@[simp]
theorem category_theory.with_initial.lift_to_initial_map {C : Type u} {D : Type u_1} {Z : D} (F : C D) (X Y : category_theory.with_initial C) (f : X Y) :
= category_theory.with_initial.lift._match_2 F (λ (x : C), hZ.to (F.obj x)) X Y f
@[simp]
theorem category_theory.with_initial.incl_lift_to_initial_hom_app {C : Type u} {D : Type u_1} {Z : D} (F : C D) (X : C) :
= 𝟙 (category_theory.with_initial.lift._match_1 F
@[simp]
theorem category_theory.with_initial.incl_lift_to_initial_inv_app {C : Type u} {D : Type u_1} {Z : D} (F : C D) (X : C) :
= 𝟙 (F.obj X)
def category_theory.with_initial.incl_lift_to_initial {C : Type u} {D : Type u_1} {Z : D} (F : C D)  :

A variant of incl_lift with Z an initial object.

Equations
• = (λ (x : C), hZ.to (F.obj x)) _
def category_theory.with_initial.lift_to_initial_unique {C : Type u} {D : Type u_1} {Z : D} (F : C D) (G : D) (h : F) (hG : Z) :

A variant of lift_unique with Z an initial object.

Equations
• = (λ (z : C), hZ.to (F.obj z)) _ G h hG _
@[simp]
theorem category_theory.with_initial.lift_to_initial_unique_inv_app {C : Type u} {D : Type u_1} {Z : D} (F : C D) (G : D) (h : F) (hG : Z)  :
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
@[simp]
theorem category_theory.with_initial.lift_to_initial_unique_hom_app {C : Type u} {D : Type u_1} {Z : D} (F : C D) (G : D) (h : F) (hG : Z)  :
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
@[simp]

Constructs a morphism from star to of X.

Equations
@[protected, instance]