Limits and colimits #
We set up the general theory of limits and colimits in a category. In this introduction we only describe the setup for limits; it is repeated, with slightly different names, for colimits.
The main structures defined in this file is
IsLimit c
, forc : Cone F
,F : J ⥤ C
, expressing thatc
is a limit cone,
See also CategoryTheory.Limits.HasLimits
which further builds:
LimitCone F
, which consists of a choice of cone forF
and the fact it is a limit cone, andHasLimit F
, asserting the mere existence of some limit cone forF
.
Implementation #
At present we simply say everything twice, in order to handle both limits and colimits.
It would be highly desirable to have some automation support,
e.g. a @[dualize]
attribute that behaves similarly to @[to_additive]
.
References #
- lift : (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ t.pt
There is a morphism from any cone point to
t.pt
- fac : ∀ (s_1 : CategoryTheory.Limits.Cone F) (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.IsLimit.lift s s_1) (t.π.app j) = s_1.π.app j
The map makes the triangle with the two natural transformations commute
- uniq : ∀ (s_1 : CategoryTheory.Limits.Cone F) (m : s_1.pt ⟶ t.pt), (∀ (j : J), CategoryTheory.CategoryStruct.comp m (t.π.app j) = s_1.π.app j) → m = CategoryTheory.Limits.IsLimit.lift s s_1
It is the unique such map to do this
A cone t
on F
is a limit cone if each cone on F
admits a unique
cone morphism to t
.
See https://stacks.math.columbia.edu/tag/002E.
Instances For
Given a natural transformation α : F ⟶ G
, we give a morphism from the cone point
of any cone over F
to the cone point of a limit cone over G
.
Instances For
The universal morphism from any other cone to a limit cone.
Instances For
Restating the definition of a limit cone in terms of the ∃! operator.
Noncomputably make a colimit cocone from the existence of unique factorizations.
Instances For
Alternative constructor for isLimit
,
providing a morphism of cones rather than a morphism between the cone points
and separately the factorisation condition.
Instances For
Limit cones on F
are unique up to isomorphism.
Instances For
Any cone morphism between limit cones is an isomorphism.
Limits of F
are unique up to isomorphism.
Instances For
Transport evidence that a cone is a limit cone across an isomorphism of cones.
Instances For
Isomorphism of cones preserves whether or not they are limiting cones.
Instances For
If the canonical morphism from a cone point to a limiting cone point is an iso, then the first cone was limiting also.
Instances For
Two morphisms into a limit are equal if their compositions with each cone morphism are equal.
Given a right adjoint functor between categories of cones, the image of a limit cone is a limit cone.
Instances For
Given two functors which have equivalent categories of cones, we can transport a limiting cone across the equivalence.
Instances For
A cone postcomposed with a natural isomorphism is a limit cone if and only if the original cone is.
Instances For
A cone postcomposed with the inverse of a natural isomorphism is a limit cone if and only if the original cone is.
Instances For
Constructing an equivalence IsLimit c ≃ IsLimit d
from a natural isomorphism
between the underlying functors, and then an isomorphism between c
transported along this and d
.
Instances For
The cone points of two limit cones for naturally isomorphic functors are themselves isomorphic.
Instances For
If s : Cone F
is a limit cone, so is s
whiskered by an equivalence e
.
Instances For
If s : Cone F
whiskered by an equivalence e
is a limit cone, so is s
.
Instances For
Given an equivalence of diagrams e
, s
is a limit cone iff s.whisker e.functor
is.
Instances For
We can prove two cone points (s : Cone F).pt
and (t : Cone G).pt
are isomorphic if
- both cones are limit cones
- their indexing categories are equivalent via some
e : J ≌ K
, - the triangle of functors commutes up to a natural isomorphism:
e.functor ⋙ G ≅ F
.
This is the most general form of uniqueness of cone points, allowing relabelling of both the indexing category (up to equivalence) and the functor (up to natural isomorphism).
Instances For
The universal property of a limit cone: a map W ⟶ X
is the same as
a cone on F
with cone point W
.
Instances For
The limit of F
represents the functor taking W
to
the set of cones on F
with cone point W
.
Instances For
Another, more explicit, formulation of the universal property of a limit cone.
See also homIso
.
Instances For
If G : C → D is a faithful functor which sends t to a limit cone, then it suffices to check that the induced maps for the image of t can be lifted to maps of C.
Instances For
If F
and G
are naturally isomorphic, then F.mapCone c
being a limit implies
G.mapCone c
is also a limit.
Instances For
A cone is a limit cone exactly if there is a unique cone morphism from any other cone.
Instances For
If F.cones
is represented by X
, each morphism f : Y ⟶ X
gives a cone with cone point
Y
.
Instances For
If F.cones
is represented by X
, each cone s
gives a morphism s.pt ⟶ X
.
Instances For
If F.cones
is represented by X
, the cone corresponding to the identity morphism on X
will be a limit cone.
Instances For
If F.cones
is represented by X
, the cone corresponding to a morphism f : Y ⟶ X
is
the limit cone extended by f
.
If F.cones
is represented by X
, any cone is the extension of the limit cone by the
corresponding morphism.
If F.cones
is representable, then the cone corresponding to the identity morphism on
the representing object is a limit cone.
Instances For
- desc : (s : CategoryTheory.Limits.Cocone F) → t.pt ⟶ s.pt
t.pt
maps to all other cocone covertices - fac : ∀ (s_1 : CategoryTheory.Limits.Cocone F) (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) (CategoryTheory.Limits.IsColimit.desc s s_1) = s_1.ι.app j
The map
desc
makes the diagram with the natural transformations commute - uniq : ∀ (s_1 : CategoryTheory.Limits.Cocone F) (m : t.pt ⟶ s_1.pt), (∀ (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) m = s_1.ι.app j) → m = CategoryTheory.Limits.IsColimit.desc s s_1
desc
is the unique such map
A cocone t
on F
is a colimit cocone if each cocone on F
admits a unique
cocone morphism from t
.
See https://stacks.math.columbia.edu/tag/002F.
Instances For
Given a natural transformation α : F ⟶ G
, we give a morphism from the cocone point
of a colimit cocone over F
to the cocone point of any cocone over G
.
Instances For
The universal morphism from a colimit cocone to any other cocone.
Instances For
Restating the definition of a colimit cocone in terms of the ∃! operator.
Noncomputably make a colimit cocone from the existence of unique factorizations.
Instances For
Alternative constructor for IsColimit
,
providing a morphism of cocones rather than a morphism between the cocone points
and separately the factorisation condition.
Instances For
Colimit cocones on F
are unique up to isomorphism.
Instances For
Any cocone morphism between colimit cocones is an isomorphism.
Colimits of F
are unique up to isomorphism.
Instances For
Transport evidence that a cocone is a colimit cocone across an isomorphism of cocones.
Instances For
Isomorphism of cocones preserves whether or not they are colimiting cocones.
Instances For
If the canonical morphism to a cocone point from a colimiting cocone point is an iso, then the first cocone was colimiting also.
Instances For
Two morphisms out of a colimit are equal if their compositions with each cocone morphism are equal.
Given a left adjoint functor between categories of cocones, the image of a colimit cocone is a colimit cocone.
Instances For
Given two functors which have equivalent categories of cocones, we can transport a colimiting cocone across the equivalence.
Instances For
A cocone precomposed with a natural isomorphism is a colimit cocone if and only if the original cocone is.
Instances For
A cocone precomposed with the inverse of a natural isomorphism is a colimit cocone if and only if the original cocone is.
Instances For
Constructing an equivalence is_colimit c ≃ is_colimit d
from a natural isomorphism
between the underlying functors, and then an isomorphism between c
transported along this and d
.
Instances For
The cocone points of two colimit cocones for naturally isomorphic functors are themselves isomorphic.
Instances For
If s : Cocone F
is a colimit cocone, so is s
whiskered by an equivalence e
.
Instances For
If s : Cocone F
whiskered by an equivalence e
is a colimit cocone, so is s
.
Instances For
Given an equivalence of diagrams e
, s
is a colimit cocone iff s.whisker e.functor
is.
Instances For
We can prove two cocone points (s : Cocone F).pt
and (t : Cocone G).pt
are isomorphic if
- both cocones are colimit cocones
- their indexing categories are equivalent via some
e : J ≌ K
, - the triangle of functors commutes up to a natural isomorphism:
e.functor ⋙ G ≅ F
.
This is the most general form of uniqueness of cocone points, allowing relabelling of both the indexing category (up to equivalence) and the functor (up to natural isomorphism).
Instances For
The universal property of a colimit cocone: a map X ⟶ W
is the same as
a cocone on F
with cone point W
.
Instances For
The colimit of F
represents the functor taking W
to
the set of cocones on F
with cone point W
.
Instances For
Another, more explicit, formulation of the universal property of a colimit cocone.
See also homIso
.
Instances For
If G : C → D is a faithful functor which sends t to a colimit cocone, then it suffices to check that the induced maps for the image of t can be lifted to maps of C.
Instances For
If F
and G
are naturally isomorphic, then F.mapCocone c
being a colimit implies
G.mapCocone c
is also a colimit.
Instances For
A cocone is a colimit cocone exactly if there is a unique cocone morphism from any other cocone.
Instances For
If F.cocones
is corepresented by X
, each morphism f : X ⟶ Y
gives a cocone with cone
point Y
.
Instances For
If F.cocones
is corepresented by X
, each cocone s
gives a morphism X ⟶ s.pt
.
Instances For
If F.cocones
is corepresented by X
, the cocone corresponding to the identity morphism on X
will be a colimit cocone.
Instances For
If F.cocones
is corepresented by X
, the cocone corresponding to a morphism f : Y ⟶ X
is
the colimit cocone extended by f
.
If F.cocones
is corepresented by X
, any cocone is the extension of the colimit cocone by the
corresponding morphism.
If F.cocones
is corepresentable, then the cocone corresponding to the identity morphism on
the representing object is a colimit cocone.