mathlib3 documentation

category_theory.limits.has_limits

Existence of limits and colimits #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In category_theory.limits.is_limit we defined is_limit c, the data showing that a cone c is a limit cone.

The two main structures defined in this file are:

has_limit is a propositional typeclass (it's important that it is a proposition merely asserting the existence of a limit, as otherwise we would have non-defeq problems from incompatible instances).

While has_limit only asserts the existence of a limit cone, we happily use the axiom of choice in mathlib, so there are convenience functions all depending on has_limit F:

Key to using the has_limit interface is that there is an @[ext] lemma stating that to check f = g, for f g : Z ⟶ limit F, it suffices to check f ≫ limit.π F j = g ≫ limit.π F j for every j. This, combined with @[simp] lemmas, makes it possible to prove many easy facts about limits using automation (e.g. tidy).

There are abbreviations has_limits_of_shape J C and has_limits C asserting the existence of classes of limits. Later more are introduced, for finite limits, special shapes of limits, etc.

Ideally, many results about limits should be stated first in terms of is_limit, and then a result in terms of has_limit derived from this. At this point, however, this is far from uniformly achieved in mathlib --- often statements are only written in terms of has_limit.

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 #

@[nolint]
structure category_theory.limits.limit_cone {J : Type u₁} [category_theory.category J] {C : Type u} [category_theory.category C] (F : J C) :
Type (max u u₁ v)

limit_cone F contains a cone over F together with the information that it is a limit.

Instances for category_theory.limits.limit_cone
  • category_theory.limits.limit_cone.has_sizeof_inst
@[class]
structure category_theory.limits.has_limit {J : Type u₁} [category_theory.category J] {C : Type u} [category_theory.category C] (F : J C) :
Prop

has_limit F represents the mere existence of a limit for F.

Instances of this typeclass
@[class]

C has limits of shape J if there exists a limit for every functor F : J ⥤ C.

Instances of this typeclass
@[class]

C has all limits of size v₁ u₁ (has_limits_of_size.{v₁ u₁} C) if it has limits of every shape J : Type u₁ with [category.{v₁} J].

Instances of this typeclass
@[reducible]

C has all (small) limits if it has limits of every shape that is as big as its hom-sets.

The projection from the limit object to a value of the functor.

Equations
Instances for category_theory.limits.limit.π

Functoriality of limits.

Usually this morphism should be accessed through lim.map, but may be needed separately when you have specified limits for the source and target functors, but not necessarily for all functors of shape J.

Equations
Instances for category_theory.limits.lim_map

The isomorphism (in Type) between morphisms from a specified object W to the limit object, and cones with cone point W.

Equations
noncomputable def category_theory.limits.limit.hom_iso' {J : Type u₁} [category_theory.category J] {C : Type u} [category_theory.category C] (F : J C) [category_theory.limits.has_limit F] (W : C) :
ulift (W category_theory.limits.limit F) {p // {j j' : J} (f : j j'), p j F.map f = p j'}

The isomorphism (in Type) between morphisms from a specified object W to the limit object, and an explicit componentwise description of cones with cone point W.

Equations

If a functor F has a limit, so does any naturally isomorphic functor.

If a functor G has the same collection of cones as a functor F which has a limit, then G also has a limit.

The limits of F : J ⥤ C and G : K ⥤ C are isomorphic, if there is an equivalence e : J ≌ K making the triangle commute up to natural isomorphism.

Equations

If a E ⋙ F has a limit, and E is an equivalence, we can construct a limit of F.

limit F is functorial in F, when C has all limits of shape J.

Equations
Instances for category_theory.limits.lim

The isomorphism between morphisms from W to the cone point of the limit cone for F and cones over F with cone point W is natural in F.

Equations

The constant functor and limit functor are adjoint to each other

Equations

has_limits_of_size_shrink.{v u} C tries to obtain has_limits_of_size.{v u} C from some other has_limits_of_size C.

@[nolint]
structure category_theory.limits.colimit_cocone {J : Type u₁} [category_theory.category J] {C : Type u} [category_theory.category C] (F : J C) :
Type (max u u₁ v)

colimit_cocone F contains a cocone over F together with the information that it is a colimit.

Instances for category_theory.limits.colimit_cocone
  • category_theory.limits.colimit_cocone.has_sizeof_inst
@[class]
structure category_theory.limits.has_colimit {J : Type u₁} [category_theory.category J] {C : Type u} [category_theory.category C] (F : J C) :
Prop

has_colimit F represents the mere existence of a colimit for F.

Instances of this typeclass
@[class]

C has colimits of shape J if there exists a colimit for every functor F : J ⥤ C.

Instances of this typeclass
@[class]

C has all colimits of size v₁ u₁ (has_colimits_of_size.{v₁ u₁} C) if it has colimits of every shape J : Type u₁ with [category.{v₁} J].

Instances of this typeclass
@[reducible]

C has all (small) colimits if it has colimits of every shape that is as big as its hom-sets.

The coprojection from a value of the functor to the colimit object.

Equations
Instances for category_theory.limits.colimit.ι
@[simp]

We have lots of lemmas describing how to simplify colimit.ι F j ≫ _, and combined with colimit.ext we rely on these lemmas for many calculations.

However, since category.assoc is a @[simp] lemma, often expressions are right associated, and it's hard to apply these lemmas about colimit.ι.

We thus use reassoc to define additional @[simp] lemmas, with an arbitrary extra morphism. (see tactic/reassoc_axiom.lean)

Functoriality of colimits.

Usually this morphism should be accessed through colim.map, but may be needed separately when you have specified colimits for the source and target functors, but not necessarily for all functors of shape J.

Equations
Instances for category_theory.limits.colim_map

The isomorphism (in Type) between morphisms from the colimit object to a specified object W, and cocones with cone point W.

Equations
noncomputable def category_theory.limits.colimit.hom_iso' {J : Type u₁} [category_theory.category J] {C : Type u} [category_theory.category C] (F : J C) [category_theory.limits.has_colimit F] (W : C) :
ulift (category_theory.limits.colimit F W) {p // {j j' : J} (f : j j'), F.map f p j' = p j}

The isomorphism (in Type) between morphisms from the colimit object to a specified object W, and an explicit componentwise description of cocones with cone point W.

Equations

If F has a colimit, so does any naturally isomorphic functor.

If a functor G has the same collection of cocones as a functor F which has a colimit, then G also has a colimit.

The colimits of F : J ⥤ C and G : K ⥤ C are isomorphic, if there is an equivalence e : J ≌ K making the triangle commute up to natural isomorphism.

Equations

If a E ⋙ F has a colimit, and E is an equivalence, we can construct a colimit of F.

The isomorphism between morphisms from the cone point of the colimit cocone for F to W and cocones over F with cone point W is natural in F.

Equations

has_colimits_of_size_shrink.{v u} C tries to obtain has_colimits_of_size.{v u} C from some other has_colimits_of_size C.

If t : cone F is a limit cone, then t.op : cocone F.op is a colimit cocone.

Equations

If t : cocone F is a colimit cocone, then t.op : cone F.op is a limit cone.

Equations

If t : cone F.op is a limit cone, then t.unop : cocone F is a colimit cocone.

Equations

If t : cocone F.op is a colimit cocone, then t.unop : cone F. is a limit cone.

Equations