Construct a cone for the empty diagram given an object.
Equations
- category_theory.limits.as_empty_cone X = {X := X, π := {app := category_theory.limits.as_empty_cone._aux_1 X, naturality' := _}}
Construct a cocone for the empty diagram given an object.
Equations
- category_theory.limits.as_empty_cocone X = {X := X, ι := {app := category_theory.limits.as_empty_cocone._aux_1 X, naturality' := _}}
X
is terminal if the cone it induces on the empty diagram is limiting.
X
is initial if the cocone it induces on the empty diagram is colimiting.
Give the morphism to a terminal object from any other.
Equations
- t.from Y = t.lift (category_theory.limits.as_empty_cone Y)
Any two morphisms to a terminal object are equal.
Give the morphism from an initial object to any other.
Equations
- t.to Y = t.desc (category_theory.limits.as_empty_cocone Y)
Any two morphisms from an initial object are equal.
Any morphism from a terminal object is mono.
Any morphism to an initial object is epi.
A category has a terminal object if it has a limit over the empty diagram.
Use has_terminal_of_unique
to construct instances.
A category has an initial object if it has a colimit over the empty diagram.
Use has_initial_of_unique
to construct instances.
An arbitrary choice of terminal object, if one exists.
You can use the notation ⊤_ C
.
This object is characterized by having a unique morphism from any object.
An arbitrary choice of initial object, if one exists.
You can use the notation ⊥_ C
.
This object is characterized by having a unique morphism to any object.
We can more explicitly show that a category has a terminal object by specifying the object, and showing there is a unique morphism to it from any other object.
We can more explicitly show that a category has an initial object by specifying the object, and showing there is a unique morphism from it to any other object.
The map from an object to the terminal object.
The map to an object from the initial object.
Equations
Equations
A terminal object is terminal.
Equations
- category_theory.limits.terminal_is_terminal = {lift := λ (s : category_theory.limits.cone (category_theory.functor.empty C)), category_theory.limits.terminal.from s.X, fac' := _, uniq' := _}
An initial object is initial.
Equations
- category_theory.limits.initial_is_initial = {desc := λ (s : category_theory.limits.cocone (category_theory.functor.empty C)), category_theory.limits.initial.to s.X, fac' := _, uniq' := _}
Any morphism from a terminal object is mono.
Any morphism to an initial object is epi.
An initial object is terminal in the opposite category.
Equations
- category_theory.limits.terminal_op_of_initial t = {lift := λ (s : category_theory.limits.cone (category_theory.functor.empty Cᵒᵖ)), (t.to (opposite.unop s.X)).op, fac' := _, uniq' := _}
An initial object in the opposite category is terminal in the original category.
Equations
- category_theory.limits.terminal_unop_of_initial t = {lift := λ (s : category_theory.limits.cone (category_theory.functor.empty C)), (t.to (opposite.op s.X)).unop, fac' := _, uniq' := _}
A terminal object is initial in the opposite category.
Equations
- category_theory.limits.initial_op_of_terminal t = {desc := λ (s : category_theory.limits.cocone (category_theory.functor.empty Cᵒᵖ)), (t.from (opposite.unop s.X)).op, fac' := _, uniq' := _}
A terminal object in the opposite category is initial in the original category.
Equations
- category_theory.limits.initial_unop_of_terminal t = {desc := λ (s : category_theory.limits.cocone (category_theory.functor.empty C)), (t.from (opposite.op s.X)).unop, fac' := _, uniq' := _}
From a functor F : J ⥤ C
, given an initial object of J
, construct a cone for J
.
In limit_of_diagram_initial
we show it is a limit cone.
From a functor F : J ⥤ C
, given an initial object of J
, show the cone
cone_of_diagram_initial
is a limit.
Equations
- category_theory.limits.limit_of_diagram_initial tX F = {lift := λ (s : category_theory.limits.cone F), s.π.app X, fac' := _, uniq' := _}
For a functor F : J ⥤ C
, if J
has an initial object then the image of it is isomorphic
to the limit of F
.
From a functor F : J ⥤ C
, given a terminal object of J
, construct a cocone for J
.
In colimit_of_diagram_terminal
we show it is a colimit cocone.
From a functor F : J ⥤ C
, given a terminal object of J
, show the cocone
cocone_of_diagram_terminal
is a colimit.
Equations
- category_theory.limits.colimit_of_diagram_terminal tX F = {desc := λ (s : category_theory.limits.cocone F), s.ι.app X, fac' := _, uniq' := _}
For a functor F : J ⥤ C
, if J
has a terminal object then the image of it is isomorphic
to the colimit of F
.
The comparison morphism from the image of a terminal object to the terminal object in the target category.
Equations
The comparison morphism from the initial object in the target category to the image of the initial object.