with_initial
and with_terminal
#
Given a category C
, this file constructs two objects:
with_terminal C
, the category built fromC
by formally adjoining a terminal object.with_initial C
, the category built fromC
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:
lift
, which liftsF : C ⥤ D
to a functor fromwith_terminal C
resp.with_initial C
in the case where an objectZ : D
is provided satisfying some additional conditions.incl_lift
shows that the composition oflift
withincl
is isomorphic to the functor which was lifted.lift_unique
provides the uniqueness property oflift
.
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.
- of : Π {C : Type u} [_inst_1 : category_theory.category C], C → category_theory.with_terminal C
- star : Π {C : Type u} [_inst_1 : category_theory.category C], category_theory.with_terminal C
Formally adjoin a terminal object to a category.
Instances for category_theory.with_terminal
- category_theory.with_terminal.has_sizeof_inst
- category_theory.with_terminal.inhabited
- category_theory.with_terminal.category_theory.category
- of : Π {C : Type u} [_inst_1 : category_theory.category C], C → category_theory.with_initial C
- star : Π {C : Type u} [_inst_1 : category_theory.category C], category_theory.with_initial C
Formally adjoin an initial object to a category.
Instances for category_theory.with_initial
- category_theory.with_initial.has_sizeof_inst
- category_theory.with_initial.inhabited
- category_theory.with_initial.category_theory.category
Morphisms for with_terminal C
.
Equations
- category_theory.with_terminal.star.hom category_theory.with_terminal.star = punit
- category_theory.with_terminal.star.hom (category_theory.with_terminal.of X) = pempty
- (category_theory.with_terminal.of ᾰ).hom category_theory.with_terminal.star = punit
- (category_theory.with_terminal.of X).hom (category_theory.with_terminal.of Y) = (X ⟶ Y)
Identity morphisms for with_terminal C
.
Equations
- category_theory.with_terminal.star.id = punit.star
- (category_theory.with_terminal.of X).id = 𝟙 X
Composition of morphisms for with_terminal C
.
Equations
- category_theory.with_terminal.comp = λ (_x _x : category_theory.with_terminal.star.hom category_theory.with_terminal.star), punit.star
- category_theory.with_terminal.comp = λ (f : category_theory.with_terminal.star.hom category_theory.with_terminal.star) (g : category_theory.with_terminal.star.hom (category_theory.with_terminal.of Y)), pempty.elim g
- category_theory.with_terminal.comp = λ (f : category_theory.with_terminal.star.hom (category_theory.with_terminal.of X)) (g : (category_theory.with_terminal.of X).hom _x), pempty.elim f
- category_theory.with_terminal.comp = λ (f : (category_theory.with_terminal.of X).hom category_theory.with_terminal.star) (g : category_theory.with_terminal.star.hom category_theory.with_terminal.star), punit.star
- category_theory.with_terminal.comp = λ (f : (category_theory.with_terminal.of ᾰ).hom category_theory.with_terminal.star) (g : category_theory.with_terminal.star.hom (category_theory.with_terminal.of Y)), pempty.elim g
- category_theory.with_terminal.comp = λ (f : (category_theory.with_terminal.of X).hom (category_theory.with_terminal.of ᾰ)) (g : (category_theory.with_terminal.of ᾰ).hom category_theory.with_terminal.star), punit.star
- category_theory.with_terminal.comp = λ (f : (category_theory.with_terminal.of X).hom (category_theory.with_terminal.of Y)) (g : (category_theory.with_terminal.of Y).hom (category_theory.with_terminal.of Z)), f ≫ g
Equations
- category_theory.with_terminal.category_theory.category = {to_category_struct := {to_quiver := {hom := λ (X Y : category_theory.with_terminal C), X.hom Y}, id := λ (X : category_theory.with_terminal C), X.id, comp := λ (X Y Z : category_theory.with_terminal C) (f : X ⟶ Y) (g : Y ⟶ Z), category_theory.with_terminal.comp f g}, id_comp' := _, comp_id' := _, assoc' := _}
The inclusion from C
into with_terminal C
.
Equations
- category_theory.with_terminal.incl = {obj := category_theory.with_terminal.of _inst_1, map := λ (X Y : C) (f : X ⟶ Y), f, map_id' := _, map_comp' := _}
Instances for category_theory.with_terminal.incl
Equations
- category_theory.with_terminal.incl.category_theory.full = {preimage := λ (X Y : C) (f : category_theory.with_terminal.incl.obj X ⟶ category_theory.with_terminal.incl.obj Y), f, witness' := _}
Map with_terminal
with respect to a functor F : C ⥤ D
.
Equations
- category_theory.with_terminal.map F = {obj := λ (X : category_theory.with_terminal C), category_theory.with_terminal.map._match_1 F X, map := λ (X Y : category_theory.with_terminal C) (f : X ⟶ Y), category_theory.with_terminal.map._match_2 F X Y f, map_id' := _, map_comp' := _}
- category_theory.with_terminal.map._match_1 F category_theory.with_terminal.star = category_theory.with_terminal.star
- category_theory.with_terminal.map._match_1 F (category_theory.with_terminal.of x) = category_theory.with_terminal.of (F.obj x)
- category_theory.with_terminal.map._match_2 F category_theory.with_terminal.star category_theory.with_terminal.star punit.star = punit.star
- category_theory.with_terminal.map._match_2 F (category_theory.with_terminal.of x) category_theory.with_terminal.star punit.star = punit.star
- category_theory.with_terminal.map._match_2 F (category_theory.with_terminal.of x) (category_theory.with_terminal.of y) f = F.map f
Equations
- category_theory.with_terminal.quiver.hom.unique = {to_inhabited := {default := category_theory.with_terminal.quiver.hom.unique._match_1 X}, uniq := _}
- category_theory.with_terminal.quiver.hom.unique._match_1 category_theory.with_terminal.star = punit.star
- category_theory.with_terminal.quiver.hom.unique._match_1 (category_theory.with_terminal.of x) = punit.star
with_terminal.star
is terminal.
Lift a functor F : C ⥤ D
to with_term C ⥤ D
.
Equations
- category_theory.with_terminal.lift F M hM = {obj := λ (X : category_theory.with_terminal C), category_theory.with_terminal.lift._match_1 F X, map := λ (X Y : category_theory.with_terminal C) (f : X ⟶ Y), category_theory.with_terminal.lift._match_2 F M X Y f, map_id' := _, map_comp' := _}
- category_theory.with_terminal.lift._match_1 F category_theory.with_terminal.star = Z
- category_theory.with_terminal.lift._match_1 F (category_theory.with_terminal.of x) = F.obj x
- category_theory.with_terminal.lift._match_2 F M category_theory.with_terminal.star category_theory.with_terminal.star punit.star = 𝟙 Z
- category_theory.with_terminal.lift._match_2 F M (category_theory.with_terminal.of x) category_theory.with_terminal.star punit.star = M x
- category_theory.with_terminal.lift._match_2 F M (category_theory.with_terminal.of x) (category_theory.with_terminal.of y) f = F.map f
The isomorphism between incl ⋙ lift F _ _
with F
.
Equations
- category_theory.with_terminal.incl_lift F M hM = {hom := {app := λ (X : C), 𝟙 ((category_theory.with_terminal.incl ⋙ category_theory.with_terminal.lift F M hM).obj X), naturality' := _}, inv := {app := λ (X : C), 𝟙 (F.obj X), naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
The isomorphism between (lift F _ _).obj with_terminal.star
with Z
.
Equations
The uniqueness of lift
.
Equations
- category_theory.with_terminal.lift_unique F M hM G h hG hh = category_theory.nat_iso.of_components (λ (X : category_theory.with_terminal C), category_theory.with_terminal.lift_unique._match_1 F M hM G h hG X) _
- category_theory.with_terminal.lift_unique._match_1 F M hM G h hG category_theory.with_terminal.star = hG
- category_theory.with_terminal.lift_unique._match_1 F M hM G h hG (category_theory.with_terminal.of x) = h.app x
A variant of lift
with Z
a terminal object.
Equations
- category_theory.with_terminal.lift_to_terminal F hZ = category_theory.with_terminal.lift F (λ (x : C), hZ.from (F.obj x)) _
A variant of incl_lift
with Z
a terminal object.
Equations
- category_theory.with_terminal.incl_lift_to_terminal F hZ = category_theory.with_terminal.incl_lift F (λ (x : C), hZ.from (F.obj x)) _
A variant of lift_unique
with Z
a terminal object.
Equations
- category_theory.with_terminal.lift_to_terminal_unique F hZ G h hG = category_theory.with_terminal.lift_unique F (λ (z : C), hZ.from (F.obj z)) _ G h hG _
Constructs a morphism to star
from of X
.
Morphisms for with_initial C
.
Identity morphisms for with_initial C
.
Equations
- category_theory.with_initial.star.id = punit.star
- (category_theory.with_initial.of X).id = 𝟙 X
Composition of morphisms for with_initial C
.
Equations
- category_theory.with_initial.comp = λ (_x _x : category_theory.with_initial.star.hom category_theory.with_initial.star), punit.star
- category_theory.with_initial.comp = λ (f : category_theory.with_initial.star.hom category_theory.with_initial.star) (g : category_theory.with_initial.star.hom (category_theory.with_initial.of X)), punit.star
- category_theory.with_initial.comp = λ (f : category_theory.with_initial.star.hom (category_theory.with_initial.of X)) (g : (category_theory.with_initial.of X).hom category_theory.with_initial.star), pempty.elim g
- category_theory.with_initial.comp = λ (f : category_theory.with_initial.star.hom (category_theory.with_initial.of ᾰ)) (g : (category_theory.with_initial.of ᾰ).hom (category_theory.with_initial.of X)), punit.star
- category_theory.with_initial.comp = λ (f : (category_theory.with_initial.of Y).hom category_theory.with_initial.star) (g : category_theory.with_initial.star.hom _x), pempty.elim f
- category_theory.with_initial.comp = λ (f : (category_theory.with_initial.of ᾰ).hom (category_theory.with_initial.of X)) (g : (category_theory.with_initial.of X).hom category_theory.with_initial.star), pempty.elim g
- category_theory.with_initial.comp = λ (f : (category_theory.with_initial.of X).hom (category_theory.with_initial.of Y)) (g : (category_theory.with_initial.of Y).hom (category_theory.with_initial.of Z)), f ≫ g
Equations
- category_theory.with_initial.category_theory.category = {to_category_struct := {to_quiver := {hom := λ (X Y : category_theory.with_initial C), X.hom Y}, id := λ (X : category_theory.with_initial C), X.id, comp := λ (X Y Z : category_theory.with_initial C) (f : X ⟶ Y) (g : Y ⟶ Z), category_theory.with_initial.comp f g}, id_comp' := _, comp_id' := _, assoc' := _}
The inclusion of C
into with_initial C
.
Equations
- category_theory.with_initial.incl = {obj := category_theory.with_initial.of _inst_1, map := λ (X Y : C) (f : X ⟶ Y), f, map_id' := _, map_comp' := _}
Instances for category_theory.with_initial.incl
Equations
- category_theory.with_initial.incl.category_theory.full = {preimage := λ (X Y : C) (f : category_theory.with_initial.incl.obj X ⟶ category_theory.with_initial.incl.obj Y), f, witness' := _}
Map with_initial
with respect to a functor F : C ⥤ D
.
Equations
- category_theory.with_initial.map F = {obj := λ (X : category_theory.with_initial C), category_theory.with_initial.map._match_1 F X, map := λ (X Y : category_theory.with_initial C) (f : X ⟶ Y), category_theory.with_initial.map._match_2 F X Y f, map_id' := _, map_comp' := _}
- category_theory.with_initial.map._match_1 F category_theory.with_initial.star = category_theory.with_initial.star
- category_theory.with_initial.map._match_1 F (category_theory.with_initial.of x) = category_theory.with_initial.of (F.obj x)
- category_theory.with_initial.map._match_2 F category_theory.with_initial.star category_theory.with_initial.star punit.star = punit.star
- category_theory.with_initial.map._match_2 F category_theory.with_initial.star (category_theory.with_initial.of x) punit.star = punit.star
- category_theory.with_initial.map._match_2 F (category_theory.with_initial.of x) (category_theory.with_initial.of y) f = F.map f
Equations
- category_theory.with_initial.quiver.hom.unique = {to_inhabited := {default := category_theory.with_initial.quiver.hom.unique._match_1 X}, uniq := _}
- category_theory.with_initial.quiver.hom.unique._match_1 category_theory.with_initial.star = punit.star
- category_theory.with_initial.quiver.hom.unique._match_1 (category_theory.with_initial.of x) = punit.star
with_initial.star
is initial.
Lift a functor F : C ⥤ D
to with_initial C ⥤ D
.
Equations
- category_theory.with_initial.lift F M hM = {obj := λ (X : category_theory.with_initial C), category_theory.with_initial.lift._match_1 F X, map := λ (X Y : category_theory.with_initial C) (f : X ⟶ Y), category_theory.with_initial.lift._match_2 F M X Y f, map_id' := _, map_comp' := _}
- category_theory.with_initial.lift._match_1 F category_theory.with_initial.star = Z
- category_theory.with_initial.lift._match_1 F (category_theory.with_initial.of x) = F.obj x
- category_theory.with_initial.lift._match_2 F M category_theory.with_initial.star category_theory.with_initial.star punit.star = 𝟙 (category_theory.with_initial.lift._match_1 F category_theory.with_initial.star)
- category_theory.with_initial.lift._match_2 F M category_theory.with_initial.star (category_theory.with_initial.of x) punit.star = M x
- category_theory.with_initial.lift._match_2 F M (category_theory.with_initial.of x) (category_theory.with_initial.of y) f = F.map f
The isomorphism between incl ⋙ lift F _ _
with F
.
Equations
- category_theory.with_initial.incl_lift F M hM = {hom := {app := λ (X : C), 𝟙 ((category_theory.with_initial.incl ⋙ category_theory.with_initial.lift F M hM).obj X), naturality' := _}, inv := {app := λ (X : C), 𝟙 (F.obj X), naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
The isomorphism between (lift F _ _).obj with_term.star
with Z
.
Equations
The uniqueness of lift
.
Equations
- category_theory.with_initial.lift_unique F M hM G h hG hh = category_theory.nat_iso.of_components (λ (X : category_theory.with_initial C), category_theory.with_initial.lift_unique._match_1 F M hM G h hG X) _
- category_theory.with_initial.lift_unique._match_1 F M hM G h hG category_theory.with_initial.star = hG
- category_theory.with_initial.lift_unique._match_1 F M hM G h hG (category_theory.with_initial.of x) = h.app x
A variant of lift
with Z
an initial object.
Equations
- category_theory.with_initial.lift_to_initial F hZ = category_theory.with_initial.lift F (λ (x : C), hZ.to (F.obj x)) _
A variant of incl_lift
with Z
an initial object.
Equations
- category_theory.with_initial.incl_lift_to_initial F hZ = category_theory.with_initial.incl_lift F (λ (x : C), hZ.to (F.obj x)) _
A variant of lift_unique
with Z
an initial object.
Equations
- category_theory.with_initial.lift_to_initial_unique F hZ G h hG = category_theory.with_initial.lift_unique F (λ (z : C), hZ.to (F.obj z)) _ G h hG _
Constructs a morphism from star
to of X
.