Initial and terminal objects in a category. #
In this file we define the predicates IsTerminal
and IsInitial
as well as the class
InitialMonoClass
.
The classes HasTerminal
and HasInitial
and the associated notations for terminal and inital
objects are defined in Terminal.lean
.
References #
Construct a cone for the empty diagram given an object.
Equations
- One or more equations did not get rendered due to their size.
Construct a cocone for the empty diagram given an object.
Equations
- One or more equations did not get rendered due to their size.
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 iff for every X
there is a unique morphism X ⟶ Y
.
Equations
- One or more equations did not get rendered due to their size.
An object Y
is terminal if for every X
there is a unique morphism X ⟶ Y
(as an instance).
Equations
- CategoryTheory.Limits.IsTerminal.ofUnique Y = { lift := fun (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)) => default, fac := ⋯, uniq := ⋯ }
An object Y
is terminal if for every X
there is a unique morphism X ⟶ Y
(as explicit arguments).
If α
is a preorder with top, then ⊤
is a terminal object.
Equations
- CategoryTheory.Limits.isTerminalTop = CategoryTheory.Limits.IsTerminal.ofUnique ⊤
Transport a term of type IsTerminal
across an isomorphism.
Equations
- hY.ofIso i = CategoryTheory.Limits.IsLimit.ofIsoLimit hY { hom := { hom := i.hom, w := ⋯ }, inv := { hom := i.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
If X
and Y
are isomorphic, then X
is terminal iff Y
is.
Equations
- One or more equations did not get rendered due to their size.
An object X
is initial iff for every Y
there is a unique morphism X ⟶ Y
.
Equations
- One or more equations did not get rendered due to their size.
An object X
is initial if for every Y
there is a unique morphism X ⟶ Y
(as an instance).
Equations
- CategoryTheory.Limits.IsInitial.ofUnique X = { desc := fun (s : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.empty C)) => default, fac := ⋯, uniq := ⋯ }
An object X
is initial if for every Y
there is a unique morphism X ⟶ Y
(as explicit arguments).
If α
is a preorder with bot, then ⊥
is an initial object.
Equations
- CategoryTheory.Limits.isInitialBot = CategoryTheory.Limits.IsInitial.ofUnique ⊥
Transport a term of type is_initial
across an isomorphism.
Equations
- hX.ofIso i = CategoryTheory.Limits.IsColimit.ofIsoColimit hX { hom := { hom := i.hom, w := ⋯ }, inv := { hom := i.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
If X
and Y
are isomorphic, then X
is initial iff Y
is.
Equations
- One or more equations did not get rendered due to their size.
Give the morphism to a terminal object from any other.
Equations
- t.from Y = t.lift (CategoryTheory.Limits.asEmptyCone 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 (CategoryTheory.Limits.asEmptyCocone Y)
Any two morphisms from an initial object are equal.
Any morphism from a terminal object is split mono.
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.uniqueUpToIso 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.uniqueUpToIso hI' = { hom := hI.to I', inv := hI'.to I, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Being terminal is independent of the empty diagram, its universe, and the cone over it, as long as the cone points are isomorphic.
Equations
- One or more equations did not get rendered due to their size.
Replacing an empty cone in IsLimit
by another with the same cone point
is an equivalence.
Equations
- One or more equations did not get rendered due to their size.
Being initial is independent of the empty diagram, its universe, and the cocone over it, as long as the cocone points are isomorphic.
Equations
- One or more equations did not get rendered due to their size.
Replacing an empty cocone in IsColimit
by another with the same cocone point
is an equivalence.
Equations
- One or more equations did not get rendered due to their size.
An initial object is terminal in the opposite category.
Equations
- CategoryTheory.Limits.terminalOpOfInitial t = { lift := fun (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty Cᵒᵖ)) => (t.to (Opposite.unop s.pt)).op, fac := ⋯, uniq := ⋯ }
An initial object in the opposite category is terminal in the original category.
Equations
- CategoryTheory.Limits.terminalUnopOfInitial t = { lift := fun (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)) => (t.to (Opposite.op s.pt)).unop, fac := ⋯, uniq := ⋯ }
A terminal object is initial in the opposite category.
Equations
- One or more equations did not get rendered due to their size.
A terminal object in the opposite category is initial in the original category.
Equations
- CategoryTheory.Limits.initialUnopOfTerminal t = { desc := fun (s : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.empty C)) => (t.from (Opposite.op s.pt)).unop, fac := ⋯, uniq := ⋯ }
A category is an InitialMonoClass
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.
- isInitial_mono_from : ∀ {I : C} (X : C) (hI : CategoryTheory.Limits.IsInitial I), CategoryTheory.Mono (hI.to X)
The map from the (any as stated) initial object to any other object is a monomorphism
Instances
The map from the (any as stated) initial object to any other object is a monomorphism
To show a category is an InitialMonoClass
it suffices to give an initial object such that
every morphism out of it is a monomorphism.
To show a category is an InitialMonoClass
it suffices to show the unique morphism from an
initial object to a terminal object is a monomorphism.
From a functor F : J ⥤ C
, given an initial object of J
, construct a cone for J
.
In limitOfDiagramInitial
we show it is a limit cone.
Equations
- CategoryTheory.Limits.coneOfDiagramInitial tX F = { pt := F.obj X, π := { app := fun (j : J) => F.map (tX.to j), naturality := ⋯ } }
From a functor F : J ⥤ C
, given an initial object of J
, show the cone
coneOfDiagramInitial
is a limit.
Equations
- CategoryTheory.Limits.limitOfDiagramInitial tX F = { lift := fun (s : CategoryTheory.Limits.Cone F) => s.π.app X, fac := ⋯, uniq := ⋯ }
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 limitOfDiagramTerminal
we show it is a limit cone.
Equations
- CategoryTheory.Limits.coneOfDiagramTerminal hX F = { pt := F.obj X, π := { app := fun (x : J) => CategoryTheory.inv (F.map (hX.from x)), 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 coneOfDiagramTerminal
is a limit.
Equations
- CategoryTheory.Limits.limitOfDiagramTerminal hX F = { lift := fun (S : CategoryTheory.Limits.Cone F) => S.π.app X, fac := ⋯, uniq := ⋯ }
From a functor F : J ⥤ C
, given a terminal object of J
, construct a cocone for J
.
In colimitOfDiagramTerminal
we show it is a colimit cocone.
Equations
- CategoryTheory.Limits.coconeOfDiagramTerminal tX F = { pt := F.obj X, ι := { app := fun (j : J) => F.map (tX.from j), naturality := ⋯ } }
From a functor F : J ⥤ C
, given a terminal object of J
, show the cocone
coconeOfDiagramTerminal
is a colimit.
Equations
- CategoryTheory.Limits.colimitOfDiagramTerminal tX F = { desc := fun (s : CategoryTheory.Limits.Cocone F) => s.ι.app X, fac := ⋯, uniq := ⋯ }
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 colimitOfDiagramInitial
we show it is a colimit cocone.
Equations
- CategoryTheory.Limits.coconeOfDiagramInitial hX F = { pt := F.obj X, ι := { app := fun (x : J) => CategoryTheory.inv (F.map (hX.to x)), 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 coconeOfDiagramInitial
is a colimit.
Equations
- CategoryTheory.Limits.colimitOfDiagramInitial hX F = { desc := fun (S : CategoryTheory.Limits.Cocone F) => S.ι.app X, fac := ⋯, uniq := ⋯ }
Any morphism between terminal objects is an isomorphism.
Any morphism between initial objects is an isomorphism.