mathlib3 documentation

category_theory.limits.is_limit

Limits and colimits #

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

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

See also category_theory.limits.has_limits which further builds:

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.is_limit {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J C} (t : category_theory.limits.cone F) :
Type (max u₁ u₃ v₃)

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 category_theory.limits.is_limit
@[simp]
theorem category_theory.limits.is_limit.fac_assoc {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J C} {t : category_theory.limits.cone F} (self : category_theory.limits.is_limit t) (s : category_theory.limits.cone F) (j : J) {X' : C} (f' : F.obj j X') :
self.lift s t.π.app j f' = s.π.app j f'
theorem category_theory.limits.is_limit.uniq {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J C} {t : category_theory.limits.cone F} (self : category_theory.limits.is_limit t) (s : category_theory.limits.cone F) (m : s.X t.X) (w : (j : J), m t.π.app j = s.π.app j) :
m = self.lift s

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.

Equations
@[simp]

The universal morphism from any other cone to a limit cone.

Equations

Restating the definition of a limit cone in terms of the ∃! operator.

Noncomputably make a colimit cocone from the existence of unique factorizations.

Equations

Alternative constructor for is_limit, providing a morphism of cones rather than a morphism between the cone points and separately the factorisation condition.

Equations

Any cone morphism between limit cones is an isomorphism.

Transport evidence that a cone is a limit cone across an isomorphism of cones.

Equations

If the canonical morphism from a cone point to a limiting cone point is an iso, then the first cone was limiting also.

Equations
theorem category_theory.limits.is_limit.hom_lift {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J C} {t : category_theory.limits.cone F} (h : category_theory.limits.is_limit t) {W : C} (m : W t.X) :
m = h.lift {X := W, π := {app := λ (b : J), m t.π.app b, naturality' := _}}
theorem category_theory.limits.is_limit.hom_ext {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J C} {t : category_theory.limits.cone F} (h : category_theory.limits.is_limit t) {W : C} {f f' : W t.X} (w : (j : J), f t.π.app j = f' t.π.app j) :
f = f'

Two morphisms into a limit are equal if their compositions with each cone morphism are equal.

Constructing an equivalence is_limit c ≃ is_limit d from a natural isomorphism between the underlying functors, and then an isomorphism between c transported along this and d.

Equations

The cone points of two limit cones for naturally isomorphic functors are themselves isomorphic.

Equations

We can prove two cone points (s : cone F).X and (t.cone G).X 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).

Equations

The universal property of a limit cone: a map W ⟶ X is the same as a cone on F with vertex W.

Equations

The limit of F represents the functor taking W to the set of cones on F with vertex W.

Equations
def category_theory.limits.is_limit.hom_iso' {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J C} {t : category_theory.limits.cone F} (h : category_theory.limits.is_limit t) (W : C) :
ulift (W t.X) {p // {j j' : J} (f : j j'), p j F.map f = p j'}

Another, more explicit, formulation of the universal property of a limit cone. See also hom_iso.

Equations

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.

Equations

If F.cones is represented by X, each morphism f : Y ⟶ X gives a cone with cone point Y.

Equations

If F.cones is represented by X, each cone s gives a morphism s.X ⟶ X.

Equations

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.

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

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 category_theory.limits.is_colimit
@[simp]
theorem category_theory.limits.is_colimit.fac_assoc {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J C} {t : category_theory.limits.cocone F} (self : category_theory.limits.is_colimit t) (s : category_theory.limits.cocone F) (j : J) {X' : C} (f' : s.X X') :
t.ι.app j self.desc s f' = s.ι.app j f'

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.

Equations
@[simp]
theorem category_theory.limits.is_colimit.ι_map_assoc {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F G : J C} {c : category_theory.limits.cocone F} (hc : category_theory.limits.is_colimit c) (d : category_theory.limits.cocone G) (α : F G) (j : J) {X' : C} (f' : d.X X') :
c.ι.app j hc.map d α f' = α.app j d.ι.app j f'

The universal morphism from a colimit cocone to any other cocone.

Equations

Restating the definition of a colimit cocone in terms of the ∃! operator.

Noncomputably make a colimit cocone from the existence of unique factorizations.

Equations

Alternative constructor for is_colimit, providing a morphism of cocones rather than a morphism between the cocone points and separately the factorisation condition.

Equations

Any cocone morphism between colimit cocones is an isomorphism.

If the canonical morphism to a cocone point from a colimiting cocone point is an iso, then the first cocone was colimiting also.

Equations
theorem category_theory.limits.is_colimit.hom_desc {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J C} {t : category_theory.limits.cocone F} (h : category_theory.limits.is_colimit t) {W : C} (m : t.X W) :
m = h.desc {X := W, ι := {app := λ (b : J), t.ι.app b m, naturality' := _}}
theorem category_theory.limits.is_colimit.hom_ext {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J C} {t : category_theory.limits.cocone F} (h : category_theory.limits.is_colimit t) {W : C} {f f' : t.X W} (w : (j : J), t.ι.app j f = t.ι.app j f') :
f = f'

Two morphisms out of a colimit are equal if their compositions with each cocone morphism are equal.

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.

Equations

The cocone points of two colimit cocones for naturally isomorphic functors are themselves isomorphic.

Equations

We can prove two cocone points (s : cocone F).X and (t.cocone G).X 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).

Equations

The universal property of a colimit cocone: a map X ⟶ W is the same as a cocone on F with vertex W.

Equations
def category_theory.limits.is_colimit.hom_iso' {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J C} {t : category_theory.limits.cocone F} (h : category_theory.limits.is_colimit t) (W : C) :
ulift (t.X W) {p // {j j' : J} (f : j j'), F.map f p j' = p j}

Another, more explicit, formulation of the universal property of a colimit cocone. See also hom_iso.

Equations

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.

Equations

If F.cocones is corepresented by X, each morphism f : X ⟶ Y gives a cocone with cone point Y.

Equations

If F.cocones is corepresented by X, the cocone corresponding to a morphism f : Y ⟶ X is the colimit cocone extended by f.