# mathlibdocumentation

category_theory.limits.limits

# 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 three main structures involved are

• `is_limit c`, for `c : cone F`, `F : J ⥤ C`, expressing that `c` is a limit cone,
• `limit_cone F`, which consists of a choice of cone for `F` and the fact it is a limit cone, and
• `has_limit F`, asserting the mere existence of some limit cone for `F`.

`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).

Typically there are two different ways one can use the limits library:

1. working with particular cones, and terms of type `is_limit`
2. working solely with `has_limit`.

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`:

• `limit F : C`, producing some limit object (of course all such are isomorphic)
• `limit.π F j : limit F ⟶ F.obj j`, the morphisms out of the limit,
• `limit.lift F c : c.X ⟶ limit F`, the universal morphism from any other `c : cone F`, etc.

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.is_limit {J : Type v} {C : Type u} {F : J C} :
Type (max 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.

@[instance]
def category_theory.limits.is_limit.subsingleton {J : Type v} {C : Type u} {F : J C}  :

def category_theory.limits.is_limit.map {J : Type v} {C : Type u} {F G : J C}  :
(F G)(s.X t.X)

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]
theorem category_theory.limits.is_limit.map_π {J : Type v} {C : Type u} {F G : J C} (α : F G) (j : J) :
d.π.app j = c.π.app j α.app j

@[simp]
theorem category_theory.limits.is_limit.map_π_assoc {J : Type v} {C : Type u} {F G : J C} (α : F G) (j : J) {X' : C} (f' : G.obj j X') :
d.π.app j f' = c.π.app j α.app j f'

theorem category_theory.limits.is_limit.lift_self {J : Type v} {C : Type u} {F : J C}  :
t.lift c = 𝟙 c.X

def category_theory.limits.is_limit.lift_cone_morphism {J : Type v} {C : Type u} {F : J C}  :
s t

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

Equations
@[simp]
theorem category_theory.limits.is_limit.lift_cone_morphism_hom {J : Type v} {C : Type u} {F : J C}  :

theorem category_theory.limits.is_limit.uniq_cone_morphism {J : Type v} {C : Type u} {F : J C} {s t : category_theory.limits.cone F} {f f' : s t} :
f = f'

@[simp]
theorem category_theory.limits.is_limit.mk_cone_morphism_lift {J : Type v} {C : Type u} {F : J C} (lift : Π (s : , s t) (uniq' : ∀ (s : (m : s t), m = lift s)  :
uniq').lift s = (lift s).hom

def category_theory.limits.is_limit.mk_cone_morphism {J : Type v} {C : Type u} {F : J C} (lift : Π (s : , s t) :
(∀ (s : (m : s t), m = lift s)

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

Equations
@[simp]
theorem category_theory.limits.is_limit.unique_up_to_iso_inv {J : Type v} {C : Type u} {F : J C} {s t : category_theory.limits.cone F}  :

def category_theory.limits.is_limit.unique_up_to_iso {J : Type v} {C : Type u} {F : J C} {s t : category_theory.limits.cone F} :

Limit cones on `F` are unique up to isomorphism.

Equations
@[simp]
theorem category_theory.limits.is_limit.unique_up_to_iso_hom {J : Type v} {C : Type u} {F : J C} {s t : category_theory.limits.cone F}  :

def category_theory.limits.is_limit.hom_is_iso {J : Type v} {C : Type u} {F : J C} {s t : category_theory.limits.cone F} (f : s t) :

Any cone morphism between limit cones is an isomorphism.

Equations

Limits of `F` are unique up to isomorphism.

Equations
@[simp]
theorem category_theory.limits.is_limit.cone_point_unique_up_to_iso_hom_comp_assoc {J : Type v} {C : Type u} {F : J C} {s t : category_theory.limits.cone F} (j : J) {X' : C} (f' : F.obj j X') :
t.π.app j f' = s.π.app j f'

@[simp]
theorem category_theory.limits.is_limit.cone_point_unique_up_to_iso_hom_comp {J : Type v} {C : Type u} {F : J C} {s t : category_theory.limits.cone F} (j : J) :
t.π.app j = s.π.app j

@[simp]
theorem category_theory.limits.is_limit.cone_point_unique_up_to_iso_inv_comp {J : Type v} {C : Type u} {F : J C} {s t : category_theory.limits.cone F} (j : J) :
s.π.app j = t.π.app j

@[simp]
theorem category_theory.limits.is_limit.cone_point_unique_up_to_iso_inv_comp_assoc {J : Type v} {C : Type u} {F : J C} {s t : category_theory.limits.cone F} (j : J) {X' : C} (f' : F.obj j X') :
s.π.app j f' = t.π.app j f'

@[simp]
theorem category_theory.limits.is_limit.lift_comp_cone_point_unique_up_to_iso_hom_assoc {J : Type v} {C : Type u} {F : J C} {r s t : category_theory.limits.cone F} {X' : C} (f' : t.X X') :
P.lift r f' = Q.lift r f'

@[simp]

@[simp]
theorem category_theory.limits.is_limit.lift_comp_cone_point_unique_up_to_iso_inv_assoc {J : Type v} {C : Type u} {F : J C} {r s t : category_theory.limits.cone F} {X' : C} (f' : s.X X') :
Q.lift r f' = P.lift r f'

@[simp]

def category_theory.limits.is_limit.of_iso_limit {J : Type v} {C : Type u} {F : J C} {r t : category_theory.limits.cone F} :

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

Equations
@[simp]
theorem category_theory.limits.is_limit.of_iso_limit_lift {J : Type v} {C : Type u} {F : J C} {r t : category_theory.limits.cone F} (i : r t)  :
(P.of_iso_limit i).lift s = P.lift s i.hom.hom

def category_theory.limits.is_limit.equiv_iso_limit {J : Type v} {C : Type u} {F : J C} {r t : category_theory.limits.cone F} :

Isomorphism of cones preserves whether or not they are limiting cones.

Equations
@[simp]
theorem category_theory.limits.is_limit.equiv_iso_limit_apply {J : Type v} {C : Type u} {F : J C} {r t : category_theory.limits.cone F} (i : r t)  :

@[simp]
theorem category_theory.limits.is_limit.equiv_iso_limit_symm_apply {J : Type v} {C : Type u} {F : J C} {r t : category_theory.limits.cone F} (i : r t)  :

def category_theory.limits.is_limit.of_point_iso {J : Type v} {C : Type u} {F : J C} {r t : category_theory.limits.cone F} [i : category_theory.is_iso (P.lift t)] :

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 v} {C : Type u} {F : J C} {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 v} {C : Type u} {F : J C} {W : C} {f f' : W t.X} :
(∀ (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.

def category_theory.limits.is_limit.of_right_adjoint {J K : Type v} {C : Type u} {F : J C} {D : Type u'} {G : K D}  :

Given a right adjoint functor between categories of cones, the image of a limit cone is a limit cone.

Equations
def category_theory.limits.is_limit.of_cone_equiv {J K : Type v} {C : Type u} {F : J C} {D : Type u'} {G : K D}  :

Given two functors which have equivalent categories of cones, we can transport a limiting cone across the equivalence.

Equations
@[simp]
theorem category_theory.limits.is_limit.of_cone_equiv_apply_desc {J K : Type v} {C : Type u} {F : J C} {D : Type u'} {G : K D} (P : category_theory.limits.is_limit (h.functor.obj c))  :

@[simp]
theorem category_theory.limits.is_limit.of_cone_equiv_symm_apply_desc {J K : Type v} {C : Type u} {F : J C} {D : Type u'} {G : K D}  :

def category_theory.limits.is_limit.postcompose_hom_equiv {J : Type v} {C : Type u} {F G : J C} (α : F G)  :

A cone postcomposed with a natural isomorphism is a limit cone if and only if the original cone is.

Equations
def category_theory.limits.is_limit.postcompose_inv_equiv {J : Type v} {C : Type u} {F G : J C} (α : F G)  :

A cone postcomposed with the inverse of a natural isomorphism is a limit cone if and only if the original cone is.

Equations
def category_theory.limits.is_limit.cone_points_iso_of_nat_iso {J : Type v} {C : Type u} {F G : J C}  :
(F G)(s.X t.X)

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

Equations
@[simp]
theorem category_theory.limits.is_limit.cone_points_iso_of_nat_iso_hom {J : Type v} {C : Type u} {F G : J C} (w : F G) :

@[simp]
theorem category_theory.limits.is_limit.cone_points_iso_of_nat_iso_inv {J : Type v} {C : Type u} {F G : J C} (w : F G) :

theorem category_theory.limits.is_limit.cone_points_iso_of_nat_iso_hom_comp_assoc {J : Type v} {C : Type u} {F G : J C} (w : F G) (j : J) {X' : C} (f' : G.obj j X') :
w).hom t.π.app j f' = s.π.app j w.hom.app j f'

theorem category_theory.limits.is_limit.cone_points_iso_of_nat_iso_hom_comp {J : Type v} {C : Type u} {F G : J C} (w : F G) (j : J) :
w).hom t.π.app j = s.π.app j w.hom.app j

theorem category_theory.limits.is_limit.cone_points_iso_of_nat_iso_inv_comp {J : Type v} {C : Type u} {F G : J C} (w : F G) (j : J) :
w).inv s.π.app j = t.π.app j w.inv.app j

theorem category_theory.limits.is_limit.cone_points_iso_of_nat_iso_inv_comp_assoc {J : Type v} {C : Type u} {F G : J C} (w : F G) (j : J) {X' : C} (f' : F.obj j X') :
w).inv s.π.app j f' = t.π.app j w.inv.app j f'

theorem category_theory.limits.is_limit.lift_comp_cone_points_iso_of_nat_iso_hom {J : Type v} {C : Type u} {F G : J C} {r s : category_theory.limits.cone F} (w : F G) :
P.lift r w).hom =

theorem category_theory.limits.is_limit.lift_comp_cone_points_iso_of_nat_iso_hom_assoc {J : Type v} {C : Type u} {F G : J C} {r s : category_theory.limits.cone F} (w : F G) {X' : C} (f' : t.X X') :
P.lift r w).hom f' =

def category_theory.limits.is_limit.whisker_equivalence {J K : Type v} {C : Type u} {F : J C} (e : K J) :

If `s : cone F` is a limit cone, so is `s` whiskered by an equivalence `e`.

Equations
@[simp]
theorem category_theory.limits.is_limit.cone_points_iso_of_equivalence_hom {J K : Type v} {C : Type u} {F : J C} {G : K C} (e : J K) (w : e.functor G F) :
w).hom =

@[simp]
theorem category_theory.limits.is_limit.cone_points_iso_of_equivalence_inv {J K : Type v} {C : Type u} {F : J C} {G : K C} (e : J K) (w : e.functor G F) :
w).inv =

def category_theory.limits.is_limit.cone_points_iso_of_equivalence {J K : Type v} {C : Type u} {F : J C} {G : K C} (e : J K) :
(e.functor G F)(s.X t.X)

We can prove two cone points `(s : cone F).X` and `(t.cone F).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
def category_theory.limits.is_limit.hom_iso {J : Type v} {C : Type u} {F : J C} (W : C) :
(W t.X)

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

Equations
@[simp]
theorem category_theory.limits.is_limit.hom_iso_hom {J : Type v} {C : Type u} {F : J C} {W : C} (f : W t.X) :
(h.hom_iso W).hom f = (t.extend f).π

def category_theory.limits.is_limit.nat_iso {J : Type v} {C : Type u} {F : J C}  :

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 v} {C : Type u} {F : J C} (W : C) :
(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
def category_theory.limits.is_limit.of_faithful {J : Type v} {C : Type u} {F : J C} {D : Type u'} (G : C D) (ht : category_theory.limits.is_limit (G.map_cone t)) (lift : Π (s : , s.X t.X) :
(∀ (s : , G.map (lift s) = ht.lift (G.map_cone s))

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
def category_theory.limits.is_limit.map_cone_equiv {J : Type v} {C : Type u} {D : Type u'} {K : J C} {F G : C D} (h : F G)  :

If `F` and `G` are naturally isomorphic, then `F.map_cone c` being a limit implies `G.map_cone c` is also a limit.

Equations
def category_theory.limits.is_limit.iso_unique_cone_morphism {J : Type v} {C : Type u} {F : J C}  :
Π (s : , unique (s t)

A cone is a limit cone exactly if there is a unique cone morphism from any other cone.

Equations
def category_theory.limits.is_limit.of_nat_iso.cone_of_hom {J : Type v} {C : Type u} {F : J C} {X : C} (h : F.cones) {Y : C} :
(Y X)

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

Equations
def category_theory.limits.is_limit.of_nat_iso.hom_of_cone {J : Type v} {C : Type u} {F : J C} {X : C} (h : F.cones)  :
s.X X

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

Equations
@[simp]
theorem category_theory.limits.is_limit.of_nat_iso.cone_of_hom_of_cone {J : Type v} {C : Type u} {F : J C} {X : C} (h : F.cones)  :

@[simp]
theorem category_theory.limits.is_limit.of_nat_iso.hom_of_cone_of_hom {J : Type v} {C : Type u} {F : J C} {X : C} (h : F.cones) {Y : C} (f : Y X) :

def category_theory.limits.is_limit.of_nat_iso.limit_cone {J : Type v} {C : Type u} {F : J C} {X : C} :

If `F.cones` is represented by `X`, the cone corresponding to the identity morphism on `X` will be a limit cone.

Equations
theorem category_theory.limits.is_limit.of_nat_iso.cone_of_hom_fac {J : Type v} {C : Type u} {F : J C} {X : C} (h : F.cones) {Y : C} (f : Y X) :

If `F.cones` is represented by `X`, the cone corresponding to a morphism `f : Y ⟶ X` is the limit cone extended by `f`.

theorem category_theory.limits.is_limit.of_nat_iso.cone_fac {J : Type v} {C : Type u} {F : J C} {X : C} (h : F.cones)  :

If `F.cones` is represented by `X`, any cone is the extension of the limit cone by the corresponding morphism.

def category_theory.limits.is_limit.of_nat_iso {J : Type v} {C : Type u} {F : J C} {X : C} (h : F.cones) :

If `F.cones` is representable, then the cone corresponding to the identity morphism on the representing object is a limit cone.

Equations
@[nolint]
structure category_theory.limits.is_colimit {J : Type v} {C : Type u} {F : J C} :
Type (max 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.

@[instance]
def category_theory.limits.is_colimit.subsingleton {J : Type v} {C : Type u} {F : J C}  :

def category_theory.limits.is_colimit.map {J : Type v} {C : Type u} {F G : J C}  :
(F G)(s.X t.X)

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 v} {C : Type u} {F G : J C} (α : F G) (j : J) {X' : C} (f' : d.X X') :
c.ι.app j hc.map d α f' = α.app j d.ι.app j f'

@[simp]
theorem category_theory.limits.is_colimit.ι_map {J : Type v} {C : Type u} {F G : J C} (α : F G) (j : J) :
c.ι.app j hc.map d α = α.app j d.ι.app j

@[simp]
theorem category_theory.limits.is_colimit.desc_self {J : Type v} {C : Type u} {F : J C}  :
h.desc t = 𝟙 t.X

def category_theory.limits.is_colimit.desc_cocone_morphism {J : Type v} {C : Type u} {F : J C}  :
t s

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

Equations
@[simp]
theorem category_theory.limits.is_colimit.desc_cocone_morphism_hom {J : Type v} {C : Type u} {F : J C}  :

theorem category_theory.limits.is_colimit.uniq_cocone_morphism {J : Type v} {C : Type u} {F : J C} {s t : category_theory.limits.cocone F} {f f' : t s} :
f = f'

def category_theory.limits.is_colimit.mk_cocone_morphism {J : Type v} {C : Type u} {F : J C} (desc : Π (s : , t s) :
(∀ (s : (m : t s), m = desc s)

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

Equations
@[simp]
theorem category_theory.limits.is_colimit.mk_cocone_morphism_desc {J : Type v} {C : Type u} {F : J C} (desc : Π (s : , t s) (uniq' : ∀ (s : (m : t s), m = desc s)  :
.desc s = (desc s).hom

@[simp]
theorem category_theory.limits.is_colimit.unique_up_to_iso_hom {J : Type v} {C : Type u} {F : J C} {s t : category_theory.limits.cocone F}  :

def category_theory.limits.is_colimit.unique_up_to_iso {J : Type v} {C : Type u} {F : J C} {s t : category_theory.limits.cocone F} :

Colimit cocones on `F` are unique up to isomorphism.

Equations
@[simp]
theorem category_theory.limits.is_colimit.unique_up_to_iso_inv {J : Type v} {C : Type u} {F : J C} {s t : category_theory.limits.cocone F}  :

def category_theory.limits.is_colimit.hom_is_iso {J : Type v} {C : Type u} {F : J C} {s t : category_theory.limits.cocone F} (f : s t) :

Any cocone morphism between colimit cocones is an isomorphism.

Equations

Colimits of `F` are unique up to isomorphism.

Equations
@[simp]
theorem category_theory.limits.is_colimit.comp_cocone_point_unique_up_to_iso_hom_assoc {J : Type v} {C : Type u} {F : J C} {s t : category_theory.limits.cocone F} (j : J) {X' : C} (f' : t.X X') :
s.ι.app j f' = t.ι.app j f'

@[simp]
theorem category_theory.limits.is_colimit.comp_cocone_point_unique_up_to_iso_hom {J : Type v} {C : Type u} {F : J C} {s t : category_theory.limits.cocone F} (j : J) :
s.ι.app j = t.ι.app j

@[simp]
theorem category_theory.limits.is_colimit.comp_cocone_point_unique_up_to_iso_inv {J : Type v} {C : Type u} {F : J C} {s t : category_theory.limits.cocone F} (j : J) :
t.ι.app j = s.ι.app j

@[simp]
theorem category_theory.limits.is_colimit.comp_cocone_point_unique_up_to_iso_inv_assoc {J : Type v} {C : Type u} {F : J C} {s t : category_theory.limits.cocone F} (j : J) {X' : C} (f' : s.X X') :
t.ι.app j f' = s.ι.app j f'

@[simp]

@[simp]
theorem category_theory.limits.is_colimit.cocone_point_unique_up_to_iso_hom_desc_assoc {J : Type v} {C : Type u} {F : J C} {r s t : category_theory.limits.cocone F} {X' : C} (f' : r.X X') :
Q.desc r f' = P.desc r f'

@[simp]
theorem category_theory.limits.is_colimit.cocone_point_unique_up_to_iso_inv_desc_assoc {J : Type v} {C : Type u} {F : J C} {r s t : category_theory.limits.cocone F} {X' : C} (f' : r.X X') :
P.desc r f' = Q.desc r f'

@[simp]

def category_theory.limits.is_colimit.of_iso_colimit {J : Type v} {C : Type u} {F : J C} {r t : category_theory.limits.cocone F} :

Transport evidence that a cocone is a colimit cocone across an isomorphism of cocones.

Equations
@[simp]
theorem category_theory.limits.is_colimit.of_iso_colimit_desc {J : Type v} {C : Type u} {F : J C} {r t : category_theory.limits.cocone F} (i : r t)  :

def category_theory.limits.is_colimit.equiv_iso_colimit {J : Type v} {C : Type u} {F : J C} {r t : category_theory.limits.cocone F} :

Isomorphism of cocones preserves whether or not they are colimiting cocones.

Equations
@[simp]
theorem category_theory.limits.is_colimit.equiv_iso_colimit_apply {J : Type v} {C : Type u} {F : J C} {r t : category_theory.limits.cocone F} (i : r t)  :

@[simp]
theorem category_theory.limits.is_colimit.equiv_iso_colimit_symm_apply {J : Type v} {C : Type u} {F : J C} {r t : category_theory.limits.cocone F} (i : r t)  :

def category_theory.limits.is_colimit.of_point_iso {J : Type v} {C : Type u} {F : J C} {r t : category_theory.limits.cocone F} [i : category_theory.is_iso (P.desc t)] :

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 v} {C : Type u} {F : J C} {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 v} {C : Type u} {F : J C} {W : C} {f f' : t.X 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.

def category_theory.limits.is_colimit.of_left_adjoint {J K : Type v} {C : Type u} {F : J C} {D : Type u'} {G : K D}  :

Given a left adjoint functor between categories of cocones, the image of a colimit cocone is a colimit cocone.

Equations
def category_theory.limits.is_colimit.of_cocone_equiv {J K : Type v} {C : Type u} {F : J C} {D : Type u'} {G : K D}  :

Given two functors which have equivalent categories of cocones, we can transport a colimiting cocone across the equivalence.

Equations
@[simp]
theorem category_theory.limits.is_colimit.of_cocone_equiv_apply_desc {J K : Type v} {C : Type u} {F : J C} {D : Type u'} {G : K D} (P : category_theory.limits.is_colimit (h.functor.obj c))  :

@[simp]
theorem category_theory.limits.is_colimit.of_cocone_equiv_symm_apply_desc {J K : Type v} {C : Type u} {F : J C} {D : Type u'} {G : K D}  :

def category_theory.limits.is_colimit.precompose_hom_equiv {J : Type v} {C : Type u} {F G : J C} (α : F G)  :

A cocone precomposed with a natural isomorphism is a colimit cocone if and only if the original cocone is.

Equations
def category_theory.limits.is_colimit.precompose_inv_equiv {J : Type v} {C : Type u} {F G : J C} (α : F G)  :

A cocone precomposed with the inverse of a natural isomorphism is a colimit cocone if and only if the original cocone is.

Equations
def category_theory.limits.is_colimit.cocone_points_iso_of_nat_iso {J : Type v} {C : Type u} {F G : J C}  :
(F G)(s.X t.X)

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

Equations
@[simp]
theorem category_theory.limits.is_colimit.cocone_points_iso_of_nat_iso_inv {J : Type v} {C : Type u} {F G : J C} (w : F G) :
w).inv = Q.map s w.inv

@[simp]
theorem category_theory.limits.is_colimit.cocone_points_iso_of_nat_iso_hom {J : Type v} {C : Type u} {F G : J C} (w : F G) :
w).hom = P.map t w.hom

theorem category_theory.limits.is_colimit.comp_cocone_points_iso_of_nat_iso_hom {J : Type v} {C : Type u} {F G : J C} (w : F G) (j : J) :
s.ι.app j w).hom = w.hom.app j t.ι.app j

theorem category_theory.limits.is_colimit.comp_cocone_points_iso_of_nat_iso_hom_assoc {J : Type v} {C : Type u} {F G : J C} (w : F G) (j : J) {X' : C} (f' : t.X X') :
s.ι.app j w).hom f' = w.hom.app j t.ι.app j f'

theorem category_theory.limits.is_colimit.comp_cocone_points_iso_of_nat_iso_inv_assoc {J : Type v} {C : Type u} {F G : J C} (w : F G) (j : J) {X' : C} (f' : s.X X') :
t.ι.app j w).inv f' = w.inv.app j s.ι.app j f'

theorem category_theory.limits.is_colimit.comp_cocone_points_iso_of_nat_iso_inv {J : Type v} {C : Type u} {F G : J C} (w : F G) (j : J) :
t.ι.app j w).inv = w.inv.app j s.ι.app j

theorem category_theory.limits.is_colimit.cocone_points_iso_of_nat_iso_hom_desc_assoc {J : Type v} {C : Type u} {F G : J C} {r t : category_theory.limits.cocone G} (w : F G) {X' : C} (f' : r.X X') :
w).hom Q.desc r f' = P.map r w.hom f'

theorem category_theory.limits.is_colimit.cocone_points_iso_of_nat_iso_hom_desc {J : Type v} {C : Type u} {F G : J C} {r t : category_theory.limits.cocone G} (w : F G) :
w).hom Q.desc r = P.map r w.hom

def category_theory.limits.is_colimit.whisker_equivalence {J K : Type v} {C : Type u} {F : J C} (e : K J) :

If `s : cone F` is a limit cone, so is `s` whiskered by an equivalence `e`.

Equations
@[simp]
theorem category_theory.limits.is_colimit.cocone_points_iso_of_equivalence_hom {J K : Type v} {C : Type u} {F : J C} {G : K C} (e : J K) (w : e.functor G F) :

@[simp]
theorem category_theory.limits.is_colimit.cocone_points_iso_of_equivalence_inv {J K : Type v} {C : Type u} {F : J C} {G : K C} (e : J K) (w : e.functor G F) :

def category_theory.limits.is_colimit.cocone_points_iso_of_equivalence {J K : Type v} {C : Type u} {F : J C} {G : K C} (e : J K) :
(e.functor G F)(s.X t.X)

We can prove two cocone points `(s : cocone F).X` and `(t.cocone F).X` are isomorphic if

• both cocones are colimit ccoones
• 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
def category_theory.limits.is_colimit.hom_iso {J : Type v} {C : Type u} {F : J C} (W : C) :
(t.X W)

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

Equations
@[simp]
theorem category_theory.limits.is_colimit.hom_iso_hom {J : Type v} {C : Type u} {F : J C} {W : C} (f : t.X W) :
(h.hom_iso W).hom f = (t.extend f).ι

def category_theory.limits.is_colimit.nat_iso {J : Type v} {C : Type u} {F : J C}  :

The colimit of `F` represents the functor taking `W` to the set of cocones on `F` with vertex `W`.

Equations
def category_theory.limits.is_colimit.hom_iso' {J : Type v} {C : Type u} {F : J C} (W : C) :
(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
def category_theory.limits.is_colimit.of_faithful {J : Type v} {C : Type u} {F : J C} {D : Type u'} (G : C D) (ht : category_theory.limits.is_colimit (G.map_cocone t)) (desc : Π (s : , t.X s.X) :
(∀ (s : , G.map (desc s) = ht.desc (G.map_cocone s))

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
def category_theory.limits.is_colimit.iso_unique_cocone_morphism {J : Type v} {C : Type u} {F : J C}  :
Π (s : , unique (t s)

A cocone is a colimit cocone exactly if there is a unique cocone morphism from any other cocone.

Equations
def category_theory.limits.is_colimit.of_nat_iso.cocone_of_hom {J : Type v} {C : Type u} {F : J C} {X : C} (h : F.cocones) {Y : C} :
(X Y)

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

Equations
def category_theory.limits.is_colimit.of_nat_iso.hom_of_cocone {J : Type v} {C : Type u} {F : J C} {X : C} (h : F.cocones)  :
X s.X

If `F.cocones` is corepresented by `X`, each cocone `s` gives a morphism `X ⟶ s.X`.

Equations
@[simp]
theorem category_theory.limits.is_colimit.of_nat_iso.cocone_of_hom_of_cocone {J : Type v} {C : Type u} {F : J C} {X : C} (h : F.cocones)  :

@[simp]
theorem category_theory.limits.is_colimit.of_nat_iso.hom_of_cocone_of_hom {J : Type v} {C : Type u} {F : J C} {X : C} (h : F.cocones) {Y : C} (f : X Y) :

def category_theory.limits.is_colimit.of_nat_iso.colimit_cocone {J : Type v} {C : Type u} {F : J C} {X : C} :

If `F.cocones` is corepresented by `X`, the cocone corresponding to the identity morphism on `X` will be a colimit cocone.

Equations
theorem category_theory.limits.is_colimit.of_nat_iso.cocone_of_hom_fac {J : Type v} {C : Type u} {F : J C} {X : C} (h : F.cocones) {Y : C} (f : X Y) :

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

theorem category_theory.limits.is_colimit.of_nat_iso.cocone_fac {J : Type v} {C : Type u} {F : J C} {X : C} (h : F.cocones)  :

If `F.cocones` is corepresented by `X`, any cocone is the extension of the colimit cocone by the corresponding morphism.

def category_theory.limits.is_colimit.of_nat_iso {J : Type v} {C : Type u} {F : J C} {X : C} (h : F.cocones) :

If `F.cocones` is corepresentable, then the cocone corresponding to the identity morphism on the representing object is a colimit cocone.

Equations
@[nolint]
structure category_theory.limits.limit_cone {J : Type v} {C : Type u}  :
J CType (max u v)
• cone :
• is_limit :

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

@[class]
structure category_theory.limits.has_limit {J : Type v} {C : Type u}  :
J C → Prop
• exists_limit :

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

Instances
theorem category_theory.limits.has_limit.mk {J : Type v} {C : Type u} {F : J C} :

def category_theory.limits.get_limit_cone {J : Type v} {C : Type u} (F : J C)  :

Use the axiom of choice to extract explicit `limit_cone F` from `has_limit F`.

Equations
@[class]
structure category_theory.limits.has_limits_of_shape (J : Type v) (C : Type u)  :
Prop
• has_limit : ∀ (F : J C),

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

Instances
@[class]
structure category_theory.limits.has_limits (C : Type u)  :
Prop
• has_limits_of_shape : ∀ (J : Type ?) [𝒥 : ,

`C` has all (small) limits if it has limits of every shape.

Instances
@[instance]
def category_theory.limits.has_limit_of_has_limits_of_shape {C : Type u} {J : Type v} (F : J C) :

@[instance]

def category_theory.limits.limit.cone {J : Type v} {C : Type u} (F : J C)  :

An arbitrary choice of limit cone for a functor.

Equations
def category_theory.limits.limit {J : Type v} {C : Type u} (F : J C)  :
C

An arbitrary choice of limit object of a functor.

Equations
def category_theory.limits.limit.π {J : Type v} {C : Type u} (F : J C) (j : J) :

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

Equations
@[simp]
theorem category_theory.limits.limit.cone_X {J : Type v} {C : Type u} {F : J C}  :

@[simp]
theorem category_theory.limits.limit.cone_π {J : Type v} {C : Type u} {F : J C} (j : J) :

@[simp]
theorem category_theory.limits.limit.w {J : Type v} {C : Type u} (F : J C) {j j' : J} (f : j j') :

@[simp]
theorem category_theory.limits.limit.w_assoc {J : Type v} {C : Type u} (F : J C) {j j' : J} (f : j j') {X' : C} (f' : F.obj j' X') :
F.map f f' =

def category_theory.limits.limit.is_limit {J : Type v} {C : Type u} (F : J C)  :

Evidence that the arbitrary choice of cone provied by `limit.cone F` is a limit cone.

Equations
def category_theory.limits.limit.lift {J : Type v} {C : Type u} (F : J C)  :

The morphism from the cone point of any other cone to the limit object.

Equations
@[simp]
theorem category_theory.limits.limit.is_limit_lift {J : Type v} {C : Type u} {F : J C}  :

@[simp]
theorem category_theory.limits.limit.lift_π {J : Type v} {C : Type u} {F : J C} (j : J) :

@[simp]
theorem category_theory.limits.limit.lift_π_assoc {J : Type v} {C : Type u} {F : J C} (j : J) {X' : C} (f' : F.obj j X') :
= c.π.app j f'

def category_theory.limits.lim_map {J : Type v} {C : Type u} {F G : J C}  :
(F G)

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
@[simp]
theorem category_theory.limits.lim_map_π_assoc {J : Type v} {C : Type u} {F G : J C} (α : F G) (j : J) {X' : C} (f' : G.obj j X') :
= α.app j f'

@[simp]
theorem category_theory.limits.lim_map_π {J : Type v} {C : Type u} {F G : J C} (α : F G) (j : J) :

def category_theory.limits.limit.cone_morphism {J : Type v} {C : Type u} {F : J C}  :

The cone morphism from any cone to the arbitrary choice of limit cone.

Equations
@[simp]
theorem category_theory.limits.limit.cone_morphism_hom {J : Type v} {C : Type u} {F : J C}  :

theorem category_theory.limits.limit.cone_morphism_π {J : Type v} {C : Type u} {F : J C} (j : J) :

@[simp]
theorem category_theory.limits.limit.cone_point_unique_up_to_iso_hom_comp_assoc {J : Type v} {C : Type u} {F : J C} (j : J) {X' : C} (f' : F.obj j X') :
= c.π.app j f'

@[simp]
theorem category_theory.limits.limit.cone_point_unique_up_to_iso_hom_comp {J : Type v} {C : Type u} {F : J C} (j : J) :

@[simp]
theorem category_theory.limits.limit.cone_point_unique_up_to_iso_inv_comp_assoc {J : Type v} {C : Type u} {F : J C} (j : J) {X' : C} (f' : F.obj j X') :
= c.π.app j f'

@[simp]
theorem category_theory.limits.limit.cone_point_unique_up_to_iso_inv_comp {J : Type v} {C : Type u} {F : J C} (j : J) :

def category_theory.limits.limit.iso_limit_cone {J : Type v} {C : Type u} {F : J C}  :

Given any other limit cone for `F`, the chosen `limit F` is isomorphic to the cone point.

Equations
@[simp]
theorem category_theory.limits.limit.iso_limit_cone_hom_π {J : Type v} {C : Type u} {F : J C} (j : J) :

@[simp]
theorem category_theory.limits.limit.iso_limit_cone_hom_π_assoc {J : Type v} {C : Type u} {F : J C} (j : J) {X' : C} (f' : F.obj j X') :
t.cone.π.app j f' =

@[simp]
theorem category_theory.limits.limit.iso_limit_cone_inv_π {J : Type v} {C : Type u} {F : J C} (j : J) :

@[simp]
theorem category_theory.limits.limit.iso_limit_cone_inv_π_assoc {J : Type v} {C : Type u} {F : J C} (j : J) {X' : C} (f' : F.obj j X') :
= t.cone.π.app j f'

@[ext]
theorem category_theory.limits.limit.hom_ext {J : Type v} {C : Type u} {F : J C} {X : C} {f f' : X } :
(∀ (j : J), = f = f'

@[simp]
theorem category_theory.limits.limit.lift_cone {J : Type v} {C : Type u} {F : J C}  :

def category_theory.limits.limit.hom_iso {J : Type v} {C : Type u} (F : J C) (W : C) :

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

Equations
@[simp]
theorem category_theory.limits.limit.hom_iso_hom {J : Type v} {C : Type u} (F : J C) {W : C} (f : W ) :

def category_theory.limits.limit.hom_iso' {J : Type v} {C : Type u} (F : J C) (W : C) :
{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
theorem category_theory.limits.limit.lift_extend {J : Type v} {C : Type u} {F : J C} {X : C} (f : X c.X) :

theorem category_theory.limits.has_limit_of_iso {J : Type v} {C : Type u} {F G : J C}  :
(F G)

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

theorem category_theory.limits.has_limit.of_cones_iso {C : Type u} {J K : Type v} (F : J C) (G : K C) (h : F.cones G.cones)  :

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

def category_theory.limits.has_limit.iso_of_nat_iso {J : Type v} {C : Type u} {F G : J C}  :
(F G)

The limits of `F : J ⥤ C` and `G : J ⥤ C` are isomorphic, if the functors are naturally isomorphic.

Equations
@[simp]
theorem category_theory.limits.has_limit.iso_of_nat_iso_hom_π {J : Type v} {C : Type u} {F G : J C} (w : F G) (j : J) :

@[simp]
theorem category_theory.limits.has_limit.iso_of_nat_iso_hom_π_assoc {J : Type v} {C : Type u} {F G : J C} (w : F G) (j : J) {X' : C} (f' : G.obj j X') :

@[simp]
theorem category_theory.limits.has_limit.lift_iso_of_nat_iso_hom {J : Type v} {C : Type u} {F G : J C} (w : F G) :

@[simp]
theorem category_theory.limits.has_limit.lift_iso_of_nat_iso_hom_assoc {J : Type v} {C : Type u} {F G : J C} (w : F G) {X' : C} (f' : X') :

def category_theory.limits.has_limit.iso_of_equivalence {J K : Type v} {C : Type u} {F : J C} {G : K C} (e : J K) :
(e.functor G F)

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
@[simp]
theorem category_theory.limits.has_limit.iso_of_equivalence_hom_π {J K : Type v} {C : Type u} {F : J C} {G : K C} (e : J K) (w : e.functor G F) (k : K) :
= w.inv.app (e.inverse.obj k) G.map (e.counit.app k)

@[simp]
theorem category_theory.limits.has_limit.iso_of_equivalence_inv_π {J K : Type v} {C : Type u} {F : J C} {G : K C} (e : J K) (w : e.functor G F) (j : J) :

def category_theory.limits.limit.pre {J K : Type v} {C : Type u} (F : J C) (E : K J)  :

The canonical morphism from the limit of `F` to the limit of `E ⋙ F`.

Equations
@[simp]
theorem category_theory.limits.limit.pre_π {J K : Type v} {C : Type u} (F : J C) (E : K J) (k : K) :

@[simp]
theorem category_theory.limits.limit.lift_pre {J K : Type v} {C : Type u} (F : J C) (E : K J)  :

@[simp]
theorem category_theory.limits.limit.pre_pre {J K : Type v} {C : Type u} (F : J C) (E : K J) {L : Type v} (D : L K) [category_theory.limits.has_limit (D E F)] :

theorem category_theory.limits.limit.pre_eq {J K : Type v} {C : Type u} {F : J C} {E : K J} (s : category_theory.limits.limit_cone (E F))  :

- If we have particular limit cones available for `E ⋙ F` and for `F`, we obtain a formula for `limit.pre F E`.

def category_theory.limits.limit.post {J : Type v} {C : Type u} (F : J C) {D : Type u'} (G : C D)  :

The canonical morphism from `G` applied to the limit of `F` to the limit of `F ⋙ G`.

Equations
@[simp]
theorem category_theory.limits.limit.post_π {J : Type v} {C : Type u} (F : J C) {D : Type u'} (G : C D) (j : J) :

@[simp]
theorem category_theory.limits.limit.lift_post {J : Type v} {C : Type u} (F : J C) {D : Type u'} (G : C D)  :
= (G.map_cone c)

@[simp]
theorem category_theory.limits.limit.post_post {J : Type v} {C : Type u} (F : J C) {D : Type u'} (G : C D) {E : Type u''} (H : D E) [category_theory.limits.has_limit ((F G) H)] :
=

theorem category_theory.limits.limit.pre_post {J K : Type v} {C : Type u} {D : Type u'} (E : K J) (F : J C) (G : C D) [category_theory.limits.has_limit ((E F) G)] :
=

@[instance]
def category_theory.limits.has_limit_equivalence_comp {J K : Type v} {C : Type u} {F : J C} (e : K J)  :

theorem category_theory.limits.has_limit_of_equivalence_comp {J K : Type v} {C : Type u} {F : J C} (e : K J)  :

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

def category_theory.limits.lim {J : Type v} {C : Type u}  :
(J C) C

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

Equations
@[simp]
theorem category_theory.limits.lim_obj {J : Type v} {C : Type u} (F : J C) :

@[simp]
theorem category_theory.limits.limit.map_π_assoc {J : Type v} {C : Type u} {F : J C} {G : J C} (α : F G) (j : J) {X' : C} (f' : G.obj j X') :
= α.app j f'

@[simp]
theorem category_theory.limits.limit.map_π {J : Type v} {C : Type u} {F : J C} {G : J C} (α : F G) (j : J) :

@[simp]
theorem category_theory.limits.limit.lift_map {J : Type v} {C : Type u} {F : J C} {G : J C} (α : F G)  :

theorem category_theory.limits.limit.map_pre {J K : Type v} {C : Type u} {F : J C} {G : J C} (α : F G) (E : K J) :

theorem category_theory.limits.limit.map_pre' {J K : Type v} {C : Type u} (F : J C) {E₁ E₂ : K J} (α : E₁ E₂) :

theorem category_theory.limits.limit.id_pre {J : Type v} {C : Type u} (F : J C) :

theorem category_theory.limits.limit.map_post {J : Type v} {C : Type u} {F : J C} {G : J C} (α : F G) {D : Type u'} (H : C D) :
H.map