# mathlibdocumentation

category_theory.limits.has_limits

# Existence of limits and colimits #

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:

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

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.limit_cone {J : Type v} {C : Type u} (F : J C) :
Type (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} (F : 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), . "apply_instance"

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 ?) [𝒥 : , . "apply_instance"

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}  :
@[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 } (w : ∀ (j : J), ) :
f = f'
@[simp]
theorem category_theory.limits.limit.lift_map {J : Type v} {C : Type u} {F G : J C} (α : F G) :
@[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} (w : 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) (w : 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.pre_π_assoc {J K : Type v} {C : Type u} (F : J C) (E : K J) (k : K) {X' : C} (f' : (E F).obj k X') :
k f' = f'
@[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_π_assoc {J : Type v} {C : Type u} (F : J C) {D : Type u'} (G : C D) (j : J) {X' : D} (f' : (F G).obj j X') :
j f' = f'
@[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.lim_map_eq_lim_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) :
def category_theory.limits.lim_yoneda {J : Type v} {C : Type u}  :

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
theorem category_theory.limits.has_limits_of_shape_of_equivalence {J : Type v} {C : Type u} {J' : Type v} (e : J J')  :

We can transport limits of shape J along an equivalence J ≌ J'.

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

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

@[class]
structure category_theory.limits.has_colimit {J : Type v} {C : Type u} (F : J C) :
Prop
• exists_colimit :

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

Instances
theorem category_theory.limits.has_colimit.mk {J : Type v} {C : Type u} {F : J C}  :
def category_theory.limits.get_colimit_cocone {J : Type v} {C : Type u} (F : J C)  :

Use the axiom of choice to extract explicit colimit_cocone F from has_colimit F.

Equations
@[class]
structure category_theory.limits.has_colimits_of_shape (J : Type v) (C : Type u)  :
Prop
• has_colimit : (∀ (F : J C), . "apply_instance"

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

Instances
@[class]
structure category_theory.limits.has_colimits (C : Type u)  :
Prop
• has_colimits_of_shape : (∀ (J : Type ?) [𝒥 : , . "apply_instance"

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

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

An arbitrary choice of colimit cocone of a functor.

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

An arbitrary choice of colimit object of a functor.

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

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

Equations
@[simp]
theorem category_theory.limits.colimit.cocone_ι {J : Type v} {C : Type u} {F : J C} (j : J) :
@[simp]
theorem category_theory.limits.colimit.cocone_X {J : Type v} {C : Type u} {F : J C}  :
@[simp]
theorem category_theory.limits.colimit.w {J : Type v} {C : Type u} (F : J C) {j j' : J} (f : j j') :
@[simp]
theorem category_theory.limits.colimit.w_assoc {J : Type v} {C : Type u} (F : J C) {j j' : J} (f : j j') {X' : C} (f' : X') :
F.map f =
def category_theory.limits.colimit.is_colimit {J : Type v} {C : Type u} (F : J C)  :

Evidence that the arbitrary choice of cocone is a colimit cocone.

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

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

Equations
@[simp]
theorem category_theory.limits.colimit.is_colimit_desc {J : Type v} {C : Type u} {F : J C}  :
@[simp]
theorem category_theory.limits.colimit.ι_desc_assoc {J : Type v} {C : Type u} {F : J C} (j : J) {X' : C} (f' : c.X X') :
= c.ι.app j f'
@[simp]
theorem category_theory.limits.colimit.ι_desc {J : Type v} {C : Type u} {F : J C} (j : J) :

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)

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

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
@[simp]
theorem category_theory.limits.ι_colim_map_assoc {J : Type v} {C : Type u} {F G : J C} (α : F G) (j : J) {X' : C} (f' : X') :
= α.app j
@[simp]
theorem category_theory.limits.ι_colim_map {J : Type v} {C : Type u} {F G : J C} (α : F G) (j : J) :
def category_theory.limits.colimit.cocone_morphism {J : Type v} {C : Type u} {F : J C}  :

The cocone morphism from the arbitrary choice of colimit cocone to any cocone.

Equations
@[simp]
theorem category_theory.limits.colimit.cocone_morphism_hom {J : Type v} {C : Type u} {F : J C}  :
theorem category_theory.limits.colimit.ι_cocone_morphism {J : Type v} {C : Type u} {F : J C} (j : J) :
@[simp]
theorem category_theory.limits.colimit.comp_cocone_point_unique_up_to_iso_hom {J : Type v} {C : Type u} {F : J C} (j : J) :
@[simp]
theorem category_theory.limits.colimit.comp_cocone_point_unique_up_to_iso_hom_assoc {J : Type v} {C : Type u} {F : J C} (j : J) {X' : C} (f' : c.X X') :
= c.ι.app j f'
@[simp]
theorem category_theory.limits.colimit.comp_cocone_point_unique_up_to_iso_inv {J : Type v} {C : Type u} {F : J C} (j : J) :
@[simp]
theorem category_theory.limits.colimit.comp_cocone_point_unique_up_to_iso_inv_assoc {J : Type v} {C : Type u} {F : J C} (j : J) {X' : C} (f' : c.X X') :
= c.ι.app j f'
def category_theory.limits.colimit.iso_colimit_cocone {J : Type v} {C : Type u} {F : J C}  :

Given any other colimit cocone for F, the chosen colimit F is isomorphic to the cocone point.

Equations
@[simp]
theorem category_theory.limits.colimit.iso_colimit_cocone_ι_hom_assoc {J : Type v} {C : Type u} {F : J C} (j : J) {X' : C} (f' : t.cocone.X X') :
= t.cocone.ι.app j f'
@[simp]
theorem category_theory.limits.colimit.iso_colimit_cocone_ι_hom {J : Type v} {C : Type u} {F : J C} (j : J) :
@[simp]
theorem category_theory.limits.colimit.iso_colimit_cocone_ι_inv_assoc {J : Type v} {C : Type u} {F : J C} (j : J) {X' : C} (f' : X') :
=
@[simp]
theorem category_theory.limits.colimit.iso_colimit_cocone_ι_inv {J : Type v} {C : Type u} {F : J C} (j : J) :
@[ext]
theorem category_theory.limits.colimit.hom_ext {J : Type v} {C : Type u} {F : J C} {X : C} {f f' : X} (w : ∀ (j : J), ) :
f = f'
@[simp]
theorem category_theory.limits.colimit.desc_cocone {J : Type v} {C : Type u} {F : J C}  :
def category_theory.limits.colimit.hom_iso {J : Type v} {C : Type u} (F : J C) (W : C) :

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

Equations
@[simp]
theorem category_theory.limits.colimit.hom_iso_hom {J : Type v} {C : Type u} (F : J C) {W : C} (f : W) :
def category_theory.limits.colimit.hom_iso' {J : Type v} {C : Type u} (F : J C) (W : C) :
{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
theorem category_theory.limits.colimit.desc_extend {J : Type v} {C : Type u} (F : J C) {X : C} (f : c.X X) :
theorem category_theory.limits.has_colimit_of_iso {J : Type v} {C : Type u} {F G : J C} (α : G F) :

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

theorem category_theory.limits.has_colimit.of_cocones_iso {C : Type u} {J K : Type v} (F : J C) (G : K C) (h : F.cocones G.cocones)  :

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

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

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

Equations
@[simp]
theorem category_theory.limits.has_colimit.iso_of_nat_iso_ι_hom_assoc {J : Type v} {C : Type u} {F G : J C} (w : F G) (j : J) {X' : C} (f' : X') :
@[simp]
theorem category_theory.limits.has_colimit.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_colimit.iso_of_nat_iso_hom_desc {J : Type v} {C : Type u} {F G : J C} (w : F G) :
@[simp]
theorem category_theory.limits.has_colimit.iso_of_nat_iso_hom_desc_assoc {J : Type v} {C : Type u} {F G : J C} (w : F G) {X' : C} (f' : t.X X') :
def category_theory.limits.has_colimit.iso_of_equivalence {J K : Type v} {C : Type u} {F : J C} {G : K C} (e : J K) (w : e.functor G F) :

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
@[simp]
theorem category_theory.limits.has_colimit.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) (j : J) :
= F.map (e.unit.app j) w.inv.app ((e.functor e.inverse).obj j) (e.functor.obj ((e.functor e.inverse).obj j))
@[simp]
theorem category_theory.limits.has_colimit.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) (k : K) :
= G.map (e.counit_inv.app k) w.hom.app (e.inverse.obj k)
def category_theory.limits.colimit.pre {J K : Type v} {C : Type u} (F : J C) (E : K J)  :

The canonical morphism from the colimit of E ⋙ F to the colimit of F.

Equations
@[simp]
theorem category_theory.limits.colimit.ι_pre {J K : Type v} {C : Type u} (F : J C) (E : K J) (k : K) :
@[simp]
theorem category_theory.limits.colimit.ι_pre_assoc {J K : Type v} {C : Type u} (F : J C) (E : K J) (k : K) {X' : C} (f' : X') :
= f'
@[simp]
theorem category_theory.limits.colimit.pre_desc {J K : Type v} {C : Type u} (F : J C) (E : K J)  :
@[simp]
theorem category_theory.limits.colimit.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_colimit (D E F)] :
theorem category_theory.limits.colimit.pre_eq {J K : Type v} {C : Type u} {F : J C} {E : K J} (s : category_theory.limits.colimit_cocone (E F))  :
• If we have particular colimit cocones available for E ⋙ F and for F, we obtain a formula for colimit.pre F E.
def category_theory.limits.colimit.post {J : Type v} {C : Type u} (F : J C) {D : Type u'} (G : C D)  :

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

Equations
@[simp]
theorem category_theory.limits.colimit.ι_post_assoc {J : Type v} {C : Type u} (F : J C) {D : Type u'} (G : C D) (j : J) {X' : D} (f' : X') :
= f'
@[simp]
theorem category_theory.limits.colimit.ι_post {J : Type v} {C : Type u} (F : J C) {D : Type u'} (G : C D) (j : J) :
@[simp]
theorem category_theory.limits.colimit.post_desc {J : Type v} {C : Type u} (F : J C) {D : Type u'} (G : C D)  :
@[simp]
theorem category_theory.limits.colimit.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_colimit ((F G) H)] :
=
theorem category_theory.limits.colimit.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_colimit ((E F) G)] :
@[instance]
def category_theory.limits.has_colimit_equivalence_comp {J K : Type v} {C : Type u} {F : J C} (e : K J)  :
theorem category_theory.limits.has_colimit_of_equivalence_comp {J K : Type v} {C : Type u} {F : J C} (e : K J)  :

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

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

colimit F is functorial in F, when C has all colimits of shape J.

Equations
@[simp]
theorem category_theory.limits.colim_obj {J : Type v} {C : Type u} (F : J C) :
@[simp]
theorem category_theory.limits.colimit.ι_map {J : Type v} {C : Type u} {F : J C} {G : J C} (α : F G) (j : J) :
@[simp]
theorem category_theory.limits.colimit.ι_map_assoc {J : Type v} {C : Type u} {F : J C} {G : J C} (α : F G) (j : J) {X' : C} (f' : X') :
= α.app j
@[simp]
theorem category_theory.limits.colimit.map_desc {J : Type v} {C : Type u} {F : J C} {G : J C} (α : F G)  :
theorem category_theory.limits.colimit.pre_map {J K : Type v} {C : Type u} {F : J C} {G : J C} (α : F G) (E : K J) :
theorem category_theory.limits.colimit.pre_map' {J K : Type v} {C : Type u} (F : J C) {E₁ E₂ : K J} (α : E₁ E₂) :
theorem category_theory.limits.colimit.pre_id {J : Type v} {C : Type u} (F : J C) :
theorem category_theory.limits.colimit.map_post {J : Type v} {C : Type u} {F : J C} {G : J C} (α : F G) {D : Type u'} (H : C D) :

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
theorem category_theory.limits.has_colimits_of_shape_of_equivalence {J : Type v} {C : Type u} {J' : Type v} (e : J J')  :

We can transport colimits of shape J along an equivalence J ≌ J'.

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

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

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

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

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

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

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

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

Equations
def category_theory.limits.is_limit_equiv_is_colimit_op {J : Type v} {C : Type u} {F : J C}  :

t : cone F is a limit cone if and only is t.op : cocone F.op is a colimit cocone.

Equations
def category_theory.limits.is_colimit_equiv_is_limit_op {J : Type v} {C : Type u} {F : J C}  :

t : cocone F is a colimit cocone if and only is t.op : cone F.op is a limit cone.

Equations