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.
An object Y is terminal if for every X there is a unique morphism X ⟶ Y.
Equations
- category_theory.limits.is_terminal.of_unique Y = {lift := λ (s : category_theory.limits.cone (category_theory.functor.empty C)), default, fac' := _, uniq' := _}
If α is a preorder with top, then ⊤ is a terminal object.
Transport a term of type is_terminal across an isomorphism.
An object X is initial if for every Y there is a unique morphism X ⟶ Y.
Equations
- category_theory.limits.is_initial.of_unique X = {desc := λ (s : category_theory.limits.cocone (category_theory.functor.empty C)), default, fac' := _, uniq' := _}
If α is a preorder with bot, then ⊥ is an initial object.
Transport a term of type is_initial across an isomorphism.
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 split mono.
Equations
- t.split_mono_from f = {retraction := t.from Y, id' := _}
Any morphism to an initial object is split epi.
Any morphism from a terminal object is mono.
Any morphism to an initial object is epi.
If T and T' are terminal, they are isomorphic.
Equations
- hT.unique_up_to_iso hT' = {hom := hT'.from T, inv := hT.from T', hom_inv_id' := _, inv_hom_id' := _}
If I and I' are initial, they are isomorphic.
Equations
- hI.unique_up_to_iso hI' = {hom := hI.to I', inv := hI'.to I, hom_inv_id' := _, inv_hom_id' := _}
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.
Being terminal is independent of the empty diagram, its universe, and the cone over it, as long as the cone points are isomorphic.
Replacing an empty cone in is_limit by another with the same cone point
is an equivalence.
Equations
- category_theory.limits.is_limit_empty_cone_equiv C c₁ c₂ h = {to_fun := λ (hl : category_theory.limits.is_limit c₁), category_theory.limits.is_limit_change_empty_cone C hl c₂ h, inv_fun := λ (hl : category_theory.limits.is_limit c₂), category_theory.limits.is_limit_change_empty_cone C hl c₁ h.symm, left_inv := _, right_inv := _}
Being initial is independent of the empty diagram, its universe, and the cocone over it, as long as the cocone points are isomorphic.
Replacing an empty cocone in is_colimit by another with the same cocone point
is an equivalence.
Equations
- category_theory.limits.is_colimit_empty_cocone_equiv C c₁ c₂ h = {to_fun := λ (hl : category_theory.limits.is_colimit c₁), category_theory.limits.is_colimit_change_empty_cocone C hl c₂ h, inv_fun := λ (hl : category_theory.limits.is_colimit c₂), category_theory.limits.is_colimit_change_empty_cocone C hl c₁ h.symm, left_inv := _, right_inv := _}
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 split mono.
Any morphism to an initial object is split 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' := _}
- is_initial_mono_from : ∀ {I : C} (X : C) (hI : category_theory.limits.is_initial I), category_theory.mono (hI.to X)
A category is a initial_mono_class if the canonical morphism of an initial object is a
monomorphism. In practice, this is most useful when given an arbitrary morphism out of the chosen
initial object, see initial.mono_from.
Given a terminal object, this is equivalent to the assumption that the unique morphism from initial
to terminal is a monomorphism, which is the second of Freyd's axioms for an AT category.
TODO: This is a condition satisfied by categories with zero objects and morphisms.
To show a category is a initial_mono_class it suffices to give an initial object such that
every morphism out of it is a monomorphism.
To show a category is a initial_mono_class it suffices to show every morphism out of the
initial object is a monomorphism.
To show a category is a initial_mono_class it suffices to show the unique morphism from an
initial object to a terminal object is a monomorphism.
To show a category is a initial_mono_class it suffices to show the unique morphism from the
initial object to a terminal object is a monomorphism.
The comparison morphism from the image of a terminal object to the terminal object in the target
category.
This is an isomorphism iff G preserves terminal objects, see
category_theory.limits.preserves_terminal.of_iso_comparison.
Equations
The comparison morphism from the initial object in the target category to the image of the initial object.
Equations
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 cone for J,
provided that the morphisms in the diagram are isomorphisms.
In limit_of_diagram_terminal we show it is a limit cone.
Equations
- category_theory.limits.cone_of_diagram_terminal hX F = {X := F.obj X, π := {app := λ (i : J), category_theory.inv (F.map (hX.from i)), naturality' := _}}
From a functor F : J ⥤ C, given a terminal object of J and that the morphisms in the
diagram are isomorphisms, show the cone cone_of_diagram_terminal is a limit.
Equations
- category_theory.limits.limit_of_diagram_terminal hX F = {lift := λ (S : category_theory.limits.cone F), S.π.app X, fac' := _, uniq' := _}
For a functor F : J ⥤ C, if J has a terminal object and all the morphisms in the diagram
are isomorphisms, then the image of the terminal object 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.
From a functor F : J ⥤ C, given an initial object of J, construct a cocone for J,
provided that the morphisms in the diagram are isomorphisms.
In colimit_of_diagram_initial we show it is a colimit cocone.
Equations
- category_theory.limits.cocone_of_diagram_initial hX F = {X := F.obj X, ι := {app := λ (i : J), category_theory.inv (F.map (hX.to i)), naturality' := _}}
From a functor F : J ⥤ C, given an initial object of J and that the morphisms in the
diagram are isomorphisms, show the cone cocone_of_diagram_initial is a colimit.
Equations
- category_theory.limits.colimit_of_diagram_initial hX F = {desc := λ (S : category_theory.limits.cocone F), S.ι.app X, fac' := _, uniq' := _}
For a functor F : J ⥤ C, if J has an initial object and all the morphisms in the diagram
are isomorphisms, then the image of the initial object is isomorphic to the colimit of F.
If j is initial in the index category, then the map limit.π F j is an isomorphism.
If j is terminal in the index category, then the map colimit.ι F j is an isomorphism.