mathlib documentation

category_theory.with_terminal

with_initial and with_terminal #

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.

inductive category_theory.with_terminal (C : Type u) [category_theory.category C] :
Type u

Formally adjoin a terminal object to a category.

inductive category_theory.with_initial (C : Type u) [category_theory.category C] :
Type u

Formally adjoin an initial object to a category.

@[simp]

Composition of morphisms for with_terminal C.

Equations

The inclusion from C into with_terminal C.

Equations

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

Equations
@[instance]
Equations
@[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
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) :

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

Equations
@[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
@[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) :
@[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) :
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) :

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

Equations
@[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)
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) :

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

Equations
@[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) :
@[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) :

The uniqueness of lift.

Equations
@[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
@[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
@[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
@[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
@[simp]
def category_theory.with_initial.comp {C : Type u} [category_theory.category C] {X Y Z : category_theory.with_initial C} :
X.hom YY.hom ZX.hom Z

Composition of morphisms for with_initial C.

Equations

The inclusion of C into with_initial C.

Equations

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

Equations
@[instance]
Equations
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) :

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

Equations
@[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
@[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
@[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) :
@[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) :
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) :

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

Equations
@[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) :
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) :

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

Equations
@[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)
@[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) :

The uniqueness of lift.

Equations

A variant of lift with Z an initial object.

Equations
@[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
@[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
@[simp]
@[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
@[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