Existence of limits and colimits

In CategoryTheory.Limits.IsLimit we defined IsLimit c, the data showing that a cone c is a limit cone.

The two main structures defined in this file are:

• LimitCone F, which consists of a choice of cone for F and the fact it is a limit cone, and
• HasLimit F, asserting the mere existence of some limit cone for F.

HasLimit 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 HasLimit 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 HasLimit 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.pt ⟶ limit F, the universal morphism from any other c : Cone F, etc.

Key to using the HasLimit 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 HasLimitsOfShape J C and HasLimits 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 IsLimit, and then a result in terms of HasLimit derived from this. At this point, however, this is far from uniformly achieved in mathlib --- often statements are only written in terms of HasLimit.

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

• Stacks: Limits and colimits

structure CategoryTheory.Limits.LimitCone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) : Type (max (max u u₁) v)

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

• cone : Cone F

  The cone itself

• isLimit : IsLimit self.cone

  The proof that is the limit cone

class CategoryTheory.Limits.HasLimit {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) : Prop

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

• mk' :: (
• exists_limit : Nonempty (LimitCone F)

  There is some limit cone for F

• )

theorem CategoryTheory.Limits.HasLimit.mk {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} (d : LimitCone F) : HasLimit F

noncomputable def CategoryTheory.Limits.getLimitCone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasLimit F] : LimitCone F

Use the axiom of choice to extract explicit LimitCone F from HasLimit F.

class CategoryTheory.Limits.HasLimitsOfShape (J : Type u₁) [Category.{v₁, u₁} J] (C : Type u) [Category.{v, u} C] : Prop

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

• has_limit (F : Functor J C) : HasLimit F

  All functors F : J ⥤ C from J have limits

class CategoryTheory.Limits.HasLimitsOfSize (C : Type u) [Category.{v, u} C] : Prop

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

• has_limits_of_shape (J : Type u₁) [Category.{v₁, u₁} J] : HasLimitsOfShape J C

  All functors F : J ⥤ C from all small J have limits

@[reducible, inline]

abbrev CategoryTheory.Limits.HasLimits (C : Type u) [Category.{v, u} C] : Prop

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

theorem CategoryTheory.Limits.HasLimits.has_limits_of_shape {C : Type u} [Category.{v, u} C] [HasLimits C] (J : Type v) [Category.{v, v} J] : HasLimitsOfShape J C

@[instance 100]

instance CategoryTheory.Limits.hasLimitOfHasLimitsOfShape {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] [HasLimitsOfShape J C] (F : Functor J C) : HasLimit F

@[instance 100]

instance CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] [HasLimitsOfSize.{v₁, u₁, v, u} C] : HasLimitsOfShape J C

noncomputable def CategoryTheory.Limits.limit.cone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasLimit F] : Cone F

An arbitrary choice of limit cone for a functor.

noncomputable def CategoryTheory.Limits.limit {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasLimit F] : C

An arbitrary choice of limit object of a functor.

noncomputable def CategoryTheory.Limits.limit.π {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasLimit F] (j : J) : limit F ⟶ F.obj j

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

theorem CategoryTheory.Limits.limit.π_comp_eqToHom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasLimit F] {j j' : J} (hj : j = j') : CategoryStruct.comp (π F j) (eqToHom ⋯) = π F j'

theorem CategoryTheory.Limits.limit.π_comp_eqToHom_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasLimit F] {j j' : J} (hj : j = j') {Z : C} (h : F.obj j' ⟶ Z) : CategoryStruct.comp (π F j) (CategoryStruct.comp (eqToHom ⋯) h) = CategoryStruct.comp (π F j') h

@[simp]

theorem CategoryTheory.Limits.limit.cone_x {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] : (cone F).pt = limit F

@[simp]

theorem CategoryTheory.Limits.limit.cone_π {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] : (cone F).π.app = π F

@[simp]

theorem CategoryTheory.Limits.limit.w {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasLimit F] {j j' : J} (f : j ⟶ j') : CategoryStruct.comp (π F j) (F.map f) = π F j'

@[simp]

theorem CategoryTheory.Limits.limit.w_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasLimit F] {j j' : J} (f : j ⟶ j') {Z : C} (h : F.obj j' ⟶ Z) : CategoryStruct.comp (π F j) (CategoryStruct.comp (F.map f) h) = CategoryStruct.comp (π F j') h

noncomputable def CategoryTheory.Limits.limit.isLimit {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasLimit F] : IsLimit (cone F)

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

noncomputable def CategoryTheory.Limits.limit.lift {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasLimit F] (c : Cone F) : c.pt ⟶ limit F

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

@[simp]

theorem CategoryTheory.Limits.limit.isLimit_lift {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] (c : Cone F) : (isLimit F).lift c = lift F c

@[simp]

theorem CategoryTheory.Limits.limit.lift_π {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] (c : Cone F) (j : J) : CategoryStruct.comp (lift F c) (π F j) = c.π.app j

@[simp]

theorem CategoryTheory.Limits.limit.lift_π_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] (c : Cone F) (j : J) {Z : C} (h : F.obj j ⟶ Z) : CategoryStruct.comp (lift F c) (CategoryStruct.comp (π F j) h) = CategoryStruct.comp (c.π.app j) h

noncomputable def CategoryTheory.Limits.limMap {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasLimit F] [HasLimit G] (α : F ⟶ G) : limit F ⟶ limit 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.

@[simp]

theorem CategoryTheory.Limits.limMap_π {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasLimit F] [HasLimit G] (α : F ⟶ G) (j : J) : CategoryStruct.comp (limMap α) (limit.π G j) = CategoryStruct.comp (limit.π F j) (α.app j)

@[simp]

theorem CategoryTheory.Limits.limMap_π_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasLimit F] [HasLimit G] (α : F ⟶ G) (j : J) {Z : C} (h : G.obj j ⟶ Z) : CategoryStruct.comp (limMap α) (CategoryStruct.comp (limit.π G j) h) = CategoryStruct.comp (limit.π F j) (CategoryStruct.comp (α.app j) h)

noncomputable def CategoryTheory.Limits.limit.coneMorphism {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] (c : Cone F) : c ⟶ cone F

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

@[simp]

theorem CategoryTheory.Limits.limit.coneMorphism_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] (c : Cone F) : (coneMorphism c).hom = lift F c

theorem CategoryTheory.Limits.limit.coneMorphism_π {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] (c : Cone F) (j : J) : CategoryStruct.comp (coneMorphism c).hom (π F j) = c.π.app j

@[simp]

theorem CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] {c : Cone F} (hc : IsLimit c) (j : J) : CategoryStruct.comp (hc.conePointUniqueUpToIso (isLimit F)).hom (π F j) = c.π.app j

@[simp]

theorem CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] {c : Cone F} (hc : IsLimit c) (j : J) {Z : C} (h : F.obj j ⟶ Z) : CategoryStruct.comp (hc.conePointUniqueUpToIso (isLimit F)).hom (CategoryStruct.comp (π F j) h) = CategoryStruct.comp (c.π.app j) h

@[simp]

theorem CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] {c : Cone F} (hc : IsLimit c) (j : J) : CategoryStruct.comp ((isLimit F).conePointUniqueUpToIso hc).inv (π F j) = c.π.app j

@[simp]

theorem CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] {c : Cone F} (hc : IsLimit c) (j : J) {Z : C} (h : F.obj j ⟶ Z) : CategoryStruct.comp ((isLimit F).conePointUniqueUpToIso hc).inv (CategoryStruct.comp (π F j) h) = CategoryStruct.comp (c.π.app j) h

theorem CategoryTheory.Limits.limit.existsUnique {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] (t : Cone F) : ∃! l : t.pt ⟶ limit F, ∀ (j : J), CategoryStruct.comp l (π F j) = t.π.app j

noncomputable def CategoryTheory.Limits.limit.isoLimitCone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] (t : LimitCone F) : limit F ≅ t.cone.pt

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

@[simp]

theorem CategoryTheory.Limits.limit.isoLimitCone_hom_π {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] (t : LimitCone F) (j : J) : CategoryStruct.comp (isoLimitCone t).hom (t.cone.π.app j) = π F j

@[simp]

theorem CategoryTheory.Limits.limit.isoLimitCone_hom_π_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] (t : LimitCone F) (j : J) {Z : C} (h : F.obj j ⟶ Z) : CategoryStruct.comp (isoLimitCone t).hom (CategoryStruct.comp (t.cone.π.app j) h) = CategoryStruct.comp (π F j) h

@[simp]

theorem CategoryTheory.Limits.limit.isoLimitCone_inv_π {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] (t : LimitCone F) (j : J) : CategoryStruct.comp (isoLimitCone t).inv (π F j) = t.cone.π.app j

@[simp]

theorem CategoryTheory.Limits.limit.isoLimitCone_inv_π_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] (t : LimitCone F) (j : J) {Z : C} (h : F.obj j ⟶ Z) : CategoryStruct.comp (isoLimitCone t).inv (CategoryStruct.comp (π F j) h) = CategoryStruct.comp (t.cone.π.app j) h

theorem CategoryTheory.Limits.limit.hom_ext {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] {X : C} {f f' : X ⟶ limit F} (w : ∀ (j : J), CategoryStruct.comp f (π F j) = CategoryStruct.comp f' (π F j)) : f = f'

theorem CategoryTheory.Limits.limit.hom_ext_iff {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] {X : C} {f f' : X ⟶ limit F} : f = f' ↔ ∀ (j : J), CategoryStruct.comp f (π F j) = CategoryStruct.comp f' (π F j)

instance CategoryTheory.Limits.isIso_limMap {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasLimit F] [HasLimit G] (α : F ⟶ G) [IsIso α] : IsIso (limMap α)

@[simp]

theorem CategoryTheory.Limits.limit.lift_map {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasLimit F] [HasLimit G] (c : Cone F) (α : F ⟶ G) : CategoryStruct.comp (lift F c) (limMap α) = lift G ((Cone.postcompose α).obj c)

@[simp]

theorem CategoryTheory.Limits.limit.lift_map_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasLimit F] [HasLimit G] (c : Cone F) (α : F ⟶ G) {Z : C} (h : limit G ⟶ Z) : CategoryStruct.comp (lift F c) (CategoryStruct.comp (limMap α) h) = CategoryStruct.comp (lift G ((Cone.postcompose α).obj c)) h

@[simp]

theorem CategoryTheory.Limits.limit.lift_cone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] : lift F (cone F) = CategoryStruct.id (limit F)

noncomputable def CategoryTheory.Limits.limit.homIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasLimit F] (W : C) : ULift.{u₁, v} (W ⟶ limit F) ≅ F.cones.obj (Opposite.op W)

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

@[simp]

theorem CategoryTheory.Limits.limit.homIso_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasLimit F] {W : C} (f : ULift.{u₁, v} (W ⟶ limit F)) : (homIso F W).hom f = CategoryStruct.comp ((Functor.const J).map f.down) (cone F).π

noncomputable def CategoryTheory.Limits.limit.homIso' {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasLimit F] (W : C) : ULift.{u₁, v} (W ⟶ limit F) ≅ { p : (j : J) → W ⟶ F.obj j // ∀ {j j' : J} (f : j ⟶ j'), CategoryStruct.comp (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.

theorem CategoryTheory.Limits.limit.lift_extend {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] (c : Cone F) {X : C} (f : X ⟶ c.pt) : lift F (c.extend f) = CategoryStruct.comp f (lift F c)

theorem CategoryTheory.Limits.hasLimit_of_iso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasLimit F] (α : F ≅ G) : HasLimit G

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

theorem CategoryTheory.Limits.hasLimit_iff_of_iso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} (α : F ≅ G) : HasLimit F ↔ HasLimit G

theorem CategoryTheory.Limits.HasLimit.ofConesIso {C : Type u} [Category.{v, u} C] {J K : Type u₁} [Category.{v₁, u₁} J] [Category.{v₂, u₁} K] (F : Functor J C) (G : Functor K C) (h : F.cones ≅ G.cones) [HasLimit F] : HasLimit G

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

noncomputable def CategoryTheory.Limits.HasLimit.isoOfNatIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasLimit F] [HasLimit G] (w : F ≅ G) : limit F ≅ limit G

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

@[simp]

theorem CategoryTheory.Limits.HasLimit.isoOfNatIso_hom_π {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasLimit F] [HasLimit G] (w : F ≅ G) (j : J) : CategoryStruct.comp (isoOfNatIso w).hom (limit.π G j) = CategoryStruct.comp (limit.π F j) (w.hom.app j)

@[simp]

theorem CategoryTheory.Limits.HasLimit.isoOfNatIso_hom_π_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasLimit F] [HasLimit G] (w : F ≅ G) (j : J) {Z : C} (h : G.obj j ⟶ Z) : CategoryStruct.comp (isoOfNatIso w).hom (CategoryStruct.comp (limit.π G j) h) = CategoryStruct.comp (limit.π F j) (CategoryStruct.comp (w.hom.app j) h)

@[simp]

theorem CategoryTheory.Limits.HasLimit.isoOfNatIso_inv_π {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasLimit F] [HasLimit G] (w : F ≅ G) (j : J) : CategoryStruct.comp (isoOfNatIso w).inv (limit.π F j) = CategoryStruct.comp (limit.π G j) (w.inv.app j)

@[simp]

theorem CategoryTheory.Limits.HasLimit.isoOfNatIso_inv_π_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasLimit F] [HasLimit G] (w : F ≅ G) (j : J) {Z : C} (h : F.obj j ⟶ Z) : CategoryStruct.comp (isoOfNatIso w).inv (CategoryStruct.comp (limit.π F j) h) = CategoryStruct.comp (limit.π G j) (CategoryStruct.comp (w.inv.app j) h)

@[simp]

theorem CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasLimit F] [HasLimit G] (t : Cone F) (w : F ≅ G) : CategoryStruct.comp (limit.lift F t) (isoOfNatIso w).hom = limit.lift G ((Cone.postcompose w.hom).obj t)

@[simp]

theorem CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_hom_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasLimit F] [HasLimit G] (t : Cone F) (w : F ≅ G) {Z : C} (h : limit G ⟶ Z) : CategoryStruct.comp (limit.lift F t) (CategoryStruct.comp (isoOfNatIso w).hom h) = CategoryStruct.comp (limit.lift G ((Cone.postcompose w.hom).obj t)) h

@[simp]

theorem CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_inv {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasLimit F] [HasLimit G] (t : Cone G) (w : F ≅ G) : CategoryStruct.comp (limit.lift G t) (isoOfNatIso w).inv = limit.lift F ((Cone.postcompose w.inv).obj t)

@[simp]

theorem CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_inv_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasLimit F] [HasLimit G] (t : Cone G) (w : F ≅ G) {Z : C} (h : limit F ⟶ Z) : CategoryStruct.comp (limit.lift G t) (CategoryStruct.comp (isoOfNatIso w).inv h) = CategoryStruct.comp (limit.lift F ((Cone.postcompose w.inv).obj t)) h

noncomputable def CategoryTheory.Limits.HasLimit.isoOfEquivalence {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] {G : Functor K C} [HasLimit G] (e : J ≌ K) (w : e.functor.comp G ≅ F) : limit F ≅ limit G

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.

@[simp]

theorem CategoryTheory.Limits.HasLimit.isoOfEquivalence_hom_π {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] {G : Functor K C} [HasLimit G] (e : J ≌ K) (w : e.functor.comp G ≅ F) (k : K) : CategoryStruct.comp (isoOfEquivalence e w).hom (limit.π G k) = CategoryStruct.comp (limit.π F (e.inverse.obj k)) (CategoryStruct.comp (w.inv.app (e.inverse.obj k)) (G.map (e.counit.app k)))

@[simp]

theorem CategoryTheory.Limits.HasLimit.isoOfEquivalence_inv_π {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] {G : Functor K C} [HasLimit G] (e : J ≌ K) (w : e.functor.comp G ≅ F) (j : J) : CategoryStruct.comp (isoOfEquivalence e w).inv (limit.π F j) = CategoryStruct.comp (limit.π G (e.functor.obj j)) (w.hom.app j)

noncomputable def CategoryTheory.Limits.limit.pre {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasLimit F] (E : Functor K J) [HasLimit (E.comp F)] : limit F ⟶ limit (E.comp F)

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

@[simp]

theorem CategoryTheory.Limits.limit.pre_π {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasLimit F] (E : Functor K J) [HasLimit (E.comp F)] (k : K) : CategoryStruct.comp (pre F E) (π (E.comp F) k) = π F (E.obj k)

@[simp]

theorem CategoryTheory.Limits.limit.pre_π_assoc {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasLimit F] (E : Functor K J) [HasLimit (E.comp F)] (k : K) {Z : C} (h : F.obj (E.obj k) ⟶ Z) : CategoryStruct.comp (pre F E) (CategoryStruct.comp (π (E.comp F) k) h) = CategoryStruct.comp (π F (E.obj k)) h

@[simp]

theorem CategoryTheory.Limits.limit.lift_pre {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasLimit F] (E : Functor K J) [HasLimit (E.comp F)] (c : Cone F) : CategoryStruct.comp (lift F c) (pre F E) = lift (E.comp F) (Cone.whisker E c)

@[simp]

theorem CategoryTheory.Limits.limit.pre_pre {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasLimit F] (E : Functor K J) [HasLimit (E.comp F)] {L : Type u₃} [Category.{v₃, u₃} L] (D : Functor L K) [h : HasLimit (D.comp (E.comp F))] : CategoryStruct.comp (pre F E) (pre (E.comp F) D) = pre F (D.comp E)

theorem CategoryTheory.Limits.limit.pre_eq {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] {E : Functor K J} [HasLimit (E.comp F)] (s : LimitCone (E.comp F)) (t : LimitCone F) : pre F E = CategoryStruct.comp (isoLimitCone t).hom (CategoryStruct.comp (s.isLimit.lift (Cone.whisker E t.cone)) (isoLimitCone s).inv)

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

noncomputable def CategoryTheory.Limits.limit.post {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor J C) [HasLimit F] (G : Functor C D) [HasLimit (F.comp G)] : G.obj (limit F) ⟶ limit (F.comp G)

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

@[simp]

theorem CategoryTheory.Limits.limit.post_π {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor J C) [HasLimit F] (G : Functor C D) [HasLimit (F.comp G)] (j : J) : CategoryStruct.comp (post F G) (π (F.comp G) j) = G.map (π F j)

@[simp]

theorem CategoryTheory.Limits.limit.post_π_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor J C) [HasLimit F] (G : Functor C D) [HasLimit (F.comp G)] (j : J) {Z : D} (h : G.obj (F.obj j) ⟶ Z) : CategoryStruct.comp (post F G) (CategoryStruct.comp (π (F.comp G) j) h) = CategoryStruct.comp (G.map (π F j)) h

@[simp]

theorem CategoryTheory.Limits.limit.lift_post {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor J C) [HasLimit F] (G : Functor C D) [HasLimit (F.comp G)] (c : Cone F) : CategoryStruct.comp (G.map (lift F c)) (post F G) = lift (F.comp G) (G.mapCone c)

@[simp]

theorem CategoryTheory.Limits.limit.post_post {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor J C) [HasLimit F] (G : Functor C D) [HasLimit (F.comp G)] {E : Type u''} [Category.{v'', u''} E] (H : Functor D E) [h : HasLimit ((F.comp G).comp H)] : CategoryStruct.comp (H.map (post F G)) (post (F.comp G) H) = post F (G.comp H)

theorem CategoryTheory.Limits.limit.pre_post {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (E : Functor K J) (F : Functor J C) (G : Functor C D) [HasLimit F] [HasLimit (E.comp F)] [HasLimit (F.comp G)] [h : HasLimit ((E.comp F).comp G)] : CategoryStruct.comp (G.map (pre F E)) (post (E.comp F) G) = CategoryStruct.comp (post F G) (pre (F.comp G) E)

instance CategoryTheory.Limits.hasLimit_equivalence_comp {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] {F : Functor J C} (e : K ≌ J) [HasLimit F] : HasLimit (e.functor.comp F)

theorem CategoryTheory.Limits.hasLimit_of_equivalence_comp {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] {F : Functor J C} (e : K ≌ J) [HasLimit (e.functor.comp F)] : HasLimit F

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

theorem CategoryTheory.Limits.hasLimit_equivalence_comp_iff {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] {F : Functor J C} (e : K ≌ J) : HasLimit (e.functor.comp F) ↔ HasLimit F

theorem CategoryTheory.Limits.hasLimit_inverse_equivalence_comp_iff {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] {F : Functor J C} (e : J ≌ K) : HasLimit (e.inverse.comp F) ↔ HasLimit F

noncomputable def CategoryTheory.Limits.lim {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] [HasLimitsOfShape J C] : Functor (Functor J C) C

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

@[simp]

theorem CategoryTheory.Limits.lim_obj {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] [HasLimitsOfShape J C] (F : Functor J C) : lim.obj F = limit F

@[simp]

theorem CategoryTheory.Limits.lim_map {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] [HasLimitsOfShape J C] {X✝ Y✝ : Functor J C} (α : X✝ ⟶ Y✝) : lim.map α = limMap α

theorem CategoryTheory.Limits.limMap_eq {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimitsOfShape J C] {G : Functor J C} (α : F ⟶ G) : limMap α = lim.map α

theorem CategoryTheory.Limits.limit.map_pre {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimitsOfShape J C] {G : Functor J C} (α : F ⟶ G) [HasLimitsOfShape K C] (E : Functor K J) : CategoryStruct.comp (lim.map α) (pre G E) = CategoryStruct.comp (pre F E) (lim.map (E.whiskerLeft α))

theorem CategoryTheory.Limits.limit.map_pre' {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] [HasLimitsOfShape J C] [HasLimitsOfShape K C] (F : Functor J C) {E₁ E₂ : Functor K J} (α : E₁ ⟶ E₂) : pre F E₂ = CategoryStruct.comp (pre F E₁) (lim.map (Functor.whiskerRight α F))

theorem CategoryTheory.Limits.limit.id_pre {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] [HasLimitsOfShape J C] (F : Functor J C) : pre F (Functor.id J) = lim.map F.leftUnitor.inv

theorem CategoryTheory.Limits.limit.map_post {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimitsOfShape J C] {G : Functor J C} (α : F ⟶ G) {D : Type u'} [Category.{v', u'} D] [HasLimitsOfShape J D] (H : Functor C D) : CategoryStruct.comp (H.map (limMap α)) (post G H) = CategoryStruct.comp (post F H) (limMap (Functor.whiskerRight α H))

noncomputable def CategoryTheory.Limits.limYoneda {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] [HasLimitsOfShape J C] : lim.comp (yoneda.comp ((Functor.whiskeringRight Cᵒᵖ (Type v) (Type (max v u₁))).obj uliftFunctor.{u₁, v})) ≅ cones J C

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.

noncomputable def CategoryTheory.Limits.constLimAdj {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] [HasLimitsOfShape J C] : Functor.const J ⊣ lim

The constant functor and limit functor are adjoint to each other

instance CategoryTheory.Limits.instIsRightAdjointFunctorLim {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] [HasLimitsOfShape J C] : lim.IsRightAdjoint

instance CategoryTheory.Limits.limMap_mono' {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasLimitsOfShape J C] (α : F ⟶ G) [Mono α] : Mono (limMap α)

instance CategoryTheory.Limits.limMap_mono {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasLimit F] [HasLimit G] (α : F ⟶ G) [∀ (j : J), Mono (α.app j)] : Mono (limMap α)

noncomputable def CategoryTheory.Limits.coneOfAdj {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {L : Functor (Functor J C) C} (adj : Functor.const J ⊣ L) (F : Functor J C) : Cone F

The limit cone obtained from a right adjoint of the constant functor.

@[simp]

theorem CategoryTheory.Limits.coneOfAdj_π {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {L : Functor (Functor J C) C} (adj : Functor.const J ⊣ L) (F : Functor J C) : (coneOfAdj adj F).π = adj.counit.app F

@[simp]

theorem CategoryTheory.Limits.coneOfAdj_pt {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {L : Functor (Functor J C) C} (adj : Functor.const J ⊣ L) (F : Functor J C) : (coneOfAdj adj F).pt = L.obj F

def CategoryTheory.Limits.isLimitConeOfAdj {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {L : Functor (Functor J C) C} (adj : Functor.const J ⊣ L) (F : Functor J C) : IsLimit (coneOfAdj adj F)

The cones defined by coneOfAdj are limit cones.

@[simp]

theorem CategoryTheory.Limits.isLimitConeOfAdj_lift {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {L : Functor (Functor J C) C} (adj : Functor.const J ⊣ L) (F : Functor J C) (s : Cone F) : (isLimitConeOfAdj adj F).lift s = (adj.homEquiv s.pt F) s.π

theorem CategoryTheory.Limits.hasLimitsOfShape_of_equivalence {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {J' : Type u₂} [Category.{v₂, u₂} J'] (e : J ≌ J') [HasLimitsOfShape J C] : HasLimitsOfShape J' C

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

theorem CategoryTheory.Limits.HasLimitsOfShape.of_small (C : Type u) [Category.{v, u} C] [HasLimitsOfSize.{v₁, u₁, v, u} C] (J : Type u₂) [Category.{v₂, u₂} J] [Small.{u₁, u₂} J] [LocallySmall.{v₁, v₂, u₂} J] : HasLimitsOfShape J C

theorem CategoryTheory.Limits.HasLimitsOfShape.of_essentiallySmall (C : Type u) [Category.{v, u} C] [HasLimitsOfSize.{v₁, u₁, v, u} C] (J : Type u₂) [Category.{v₂, u₂} J] [EssentiallySmall.{u₁, v₂, u₂} J] [LocallySmall.{v₁, v₂, u₂} J] : HasLimitsOfShape J C

theorem CategoryTheory.Limits.hasLimitsOfSizeOfUnivLE (C : Type u) [Category.{v, u} C] [UnivLE.{v₂, v₁}] [UnivLE.{u₂, u₁}] [HasLimitsOfSize.{v₁, u₁, v, u} C] : HasLimitsOfSize.{v₂, u₂, v, u} C

A category that has larger limits also has smaller limits.

theorem CategoryTheory.Limits.hasLimitsOfSizeShrink (C : Type u) [Category.{v, u} C] [HasLimitsOfSize.{max v₁ v₂, max u₁ u₂, v, u} C] : HasLimitsOfSize.{v₁, u₁, v, u} C

hasLimitsOfSizeShrink.{v u} C tries to obtain HasLimitsOfSize.{v u} C from some other HasLimitsOfSize C.

@[instance 100]

instance CategoryTheory.Limits.hasSmallestLimitsOfHasLimits (C : Type u) [Category.{v, u} C] [HasLimits C] : HasLimitsOfSize.{0, 0, v, u} C

structure CategoryTheory.Limits.ColimitCocone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) : Type (max (max u u₁) v)

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

• cocone : Cocone F

  The cocone itself

• isColimit : IsColimit self.cocone

  The proof that it is the colimit cocone

class CategoryTheory.Limits.HasColimit {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) : Prop

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

• mk' :: (
• exists_colimit : Nonempty (ColimitCocone F)

  There exists a colimit for F

• )

theorem CategoryTheory.Limits.HasColimit.mk {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} (d : ColimitCocone F) : HasColimit F

noncomputable def CategoryTheory.Limits.getColimitCocone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] : ColimitCocone F

Use the axiom of choice to extract explicit ColimitCocone F from HasColimit F.

class CategoryTheory.Limits.HasColimitsOfShape (J : Type u₁) [Category.{v₁, u₁} J] (C : Type u) [Category.{v, u} C] : Prop

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

• has_colimit (F : Functor J C) : HasColimit F

  All F : J ⥤ C have colimits for a fixed J

class CategoryTheory.Limits.HasColimitsOfSize (C : Type u) [Category.{v, u} C] : Prop

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

• has_colimits_of_shape (J : Type u₁) [Category.{v₁, u₁} J] : HasColimitsOfShape J C

  All F : J ⥤ C have colimits for all small J

@[reducible, inline]

abbrev CategoryTheory.Limits.HasColimits (C : Type u) [Category.{v, u} C] : Prop

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

theorem CategoryTheory.Limits.HasColimits.hasColimitsOfShape {C : Type u} [Category.{v, u} C] [HasColimits C] (J : Type v) [Category.{v, v} J] : HasColimitsOfShape J C

@[instance 100]

instance CategoryTheory.Limits.hasColimitOfHasColimitsOfShape {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] [HasColimitsOfShape J C] (F : Functor J C) : HasColimit F

@[instance 100]

instance CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize {C : Type u} [Category.{v, u} C] {J : Type u₁} [Category.{v₁, u₁} J] [HasColimitsOfSize.{v₁, u₁, v, u} C] : HasColimitsOfShape J C

noncomputable def CategoryTheory.Limits.colimit.cocone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] : Cocone F

An arbitrary choice of colimit cocone of a functor.

noncomputable def CategoryTheory.Limits.colimit {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] : C

An arbitrary choice of colimit object of a functor.

noncomputable def CategoryTheory.Limits.colimit.ι {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] (j : J) : F.obj j ⟶ colimit F

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

theorem CategoryTheory.Limits.colimit.eqToHom_comp_ι {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] {j j' : J} (hj : j = j') : CategoryStruct.comp (eqToHom ⋯) (ι F j) = ι F j'

theorem CategoryTheory.Limits.colimit.eqToHom_comp_ι_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] {j j' : J} (hj : j = j') {Z : C} (h : colimit F ⟶ Z) : CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (ι F j) h) = CategoryStruct.comp (ι F j') h

@[simp]

theorem CategoryTheory.Limits.colimit.cocone_ι {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] (j : J) : (cocone F).ι.app j = ι F j

@[simp]

theorem CategoryTheory.Limits.colimit.cocone_x {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] : (cocone F).pt = colimit F

@[simp]

theorem CategoryTheory.Limits.colimit.w {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] {j j' : J} (f : j ⟶ j') : CategoryStruct.comp (F.map f) (ι F j') = ι F j

@[simp]

theorem CategoryTheory.Limits.colimit.w_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] {j j' : J} (f : j ⟶ j') {Z : C} (h : colimit F ⟶ Z) : CategoryStruct.comp (F.map f) (CategoryStruct.comp (ι F j') h) = CategoryStruct.comp (ι F j) h

noncomputable def CategoryTheory.Limits.colimit.isColimit {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] : IsColimit (cocone F)

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

noncomputable def CategoryTheory.Limits.colimit.desc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] (c : Cocone F) : colimit F ⟶ c.pt

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

@[simp]

theorem CategoryTheory.Limits.colimit.isColimit_desc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] (c : Cocone F) : (isColimit F).desc c = desc F c

@[simp]

theorem CategoryTheory.Limits.colimit.ι_desc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] (c : Cocone F) (j : J) : CategoryStruct.comp (ι F j) (desc F c) = c.ι.app 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 Mathlib/Tactic/CategoryTheory/Reassoc.lean)

@[simp]

theorem CategoryTheory.Limits.colimit.ι_desc_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] (c : Cocone F) (j : J) {Z : C} (h : c.pt ⟶ Z) : CategoryStruct.comp (ι F j) (CategoryStruct.comp (desc F c) h) = CategoryStruct.comp (c.ι.app j) h

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 Mathlib/Tactic/CategoryTheory/Reassoc.lean)

noncomputable def CategoryTheory.Limits.colimMap {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasColimit F] [HasColimit G] (α : F ⟶ G) : colimit F ⟶ colimit 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.

@[simp]

theorem CategoryTheory.Limits.ι_colimMap {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasColimit F] [HasColimit G] (α : F ⟶ G) (j : J) : CategoryStruct.comp (colimit.ι F j) (colimMap α) = CategoryStruct.comp (α.app j) (colimit.ι G j)

@[simp]

theorem CategoryTheory.Limits.ι_colimMap_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasColimit F] [HasColimit G] (α : F ⟶ G) (j : J) {Z : C} (h : colimit G ⟶ Z) : CategoryStruct.comp (colimit.ι F j) (CategoryStruct.comp (colimMap α) h) = CategoryStruct.comp (α.app j) (CategoryStruct.comp (colimit.ι G j) h)

noncomputable def CategoryTheory.Limits.colimit.coconeMorphism {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] (c : Cocone F) : cocone F ⟶ c

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

@[simp]

theorem CategoryTheory.Limits.colimit.coconeMorphism_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] (c : Cocone F) : (coconeMorphism c).hom = desc F c

theorem CategoryTheory.Limits.colimit.ι_coconeMorphism {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] (c : Cocone F) (j : J) : CategoryStruct.comp (ι F j) (coconeMorphism c).hom = c.ι.app j

@[simp]

theorem CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] {c : Cocone F} (hc : IsColimit c) (j : J) : CategoryStruct.comp (ι F j) ((isColimit F).coconePointUniqueUpToIso hc).hom = c.ι.app j

@[simp]

theorem CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] {c : Cocone F} (hc : IsColimit c) (j : J) {Z : C} (h : c.pt ⟶ Z) : CategoryStruct.comp (ι F j) (CategoryStruct.comp ((isColimit F).coconePointUniqueUpToIso hc).hom h) = CategoryStruct.comp (c.ι.app j) h

@[simp]

theorem CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] {c : Cocone F} (hc : IsColimit c) (j : J) : CategoryStruct.comp (ι F j) (hc.coconePointUniqueUpToIso (isColimit F)).inv = c.ι.app j

@[simp]

theorem CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] {c : Cocone F} (hc : IsColimit c) (j : J) {Z : C} (h : c.pt ⟶ Z) : CategoryStruct.comp (ι F j) (CategoryStruct.comp (hc.coconePointUniqueUpToIso (isColimit F)).inv h) = CategoryStruct.comp (c.ι.app j) h

theorem CategoryTheory.Limits.colimit.existsUnique {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] (t : Cocone F) : ∃! d : colimit F ⟶ t.pt, ∀ (j : J), CategoryStruct.comp (ι F j) d = t.ι.app j

noncomputable def CategoryTheory.Limits.colimit.isoColimitCocone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] (t : ColimitCocone F) : colimit F ≅ t.cocone.pt

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

@[simp]

theorem CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] (t : ColimitCocone F) (j : J) : CategoryStruct.comp (ι F j) (isoColimitCocone t).hom = t.cocone.ι.app j

@[simp]

theorem CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] (t : ColimitCocone F) (j : J) {Z : C} (h : t.cocone.pt ⟶ Z) : CategoryStruct.comp (ι F j) (CategoryStruct.comp (isoColimitCocone t).hom h) = CategoryStruct.comp (t.cocone.ι.app j) h

@[simp]

theorem CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] (t : ColimitCocone F) (j : J) : CategoryStruct.comp (t.cocone.ι.app j) (isoColimitCocone t).inv = ι F j

@[simp]

theorem CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] (t : ColimitCocone F) (j : J) {Z : C} (h : colimit F ⟶ Z) : CategoryStruct.comp (t.cocone.ι.app j) (CategoryStruct.comp (isoColimitCocone t).inv h) = CategoryStruct.comp (ι F j) h

theorem CategoryTheory.Limits.colimit.hom_ext {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] {X : C} {f f' : colimit F ⟶ X} (w : ∀ (j : J), CategoryStruct.comp (ι F j) f = CategoryStruct.comp (ι F j) f') : f = f'

theorem CategoryTheory.Limits.colimit.hom_ext_iff {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] {X : C} {f f' : colimit F ⟶ X} : f = f' ↔ ∀ (j : J), CategoryStruct.comp (ι F j) f = CategoryStruct.comp (ι F j) f'

instance CategoryTheory.Limits.isIso_colimMap {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasColimit F] [HasColimit G] (α : F ⟶ G) [IsIso α] : IsIso (colimMap α)

@[simp]

theorem CategoryTheory.Limits.colimit.desc_cocone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] : desc F (cocone F) = CategoryStruct.id (colimit F)

noncomputable def CategoryTheory.Limits.colimit.homIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] (W : C) : ULift.{u₁, v} (colimit F ⟶ W) ≅ F.cocones.obj W

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

@[simp]

theorem CategoryTheory.Limits.colimit.homIso_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] {W : C} (f : ULift.{u₁, v} (colimit F ⟶ W)) : (homIso F W).hom f = CategoryStruct.comp (cocone F).ι ((Functor.const J).map f.down)

noncomputable def CategoryTheory.Limits.colimit.homIso' {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] (W : C) : ULift.{u₁, v} (colimit F ⟶ W) ≅ { p : (j : J) → F.obj j ⟶ W // ∀ {j j' : J} (f : j ⟶ j'), CategoryStruct.comp (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.

theorem CategoryTheory.Limits.colimit.desc_extend {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] (c : Cocone F) {X : C} (f : c.pt ⟶ X) : desc F (c.extend f) = CategoryStruct.comp (desc F c) f

theorem CategoryTheory.Limits.hasColimit_of_iso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasColimit F] (α : G ≅ F) : HasColimit G

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

theorem CategoryTheory.Limits.hasColimit_iff_of_iso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} (α : F ≅ G) : HasColimit F ↔ HasColimit G

theorem CategoryTheory.Limits.HasColimit.ofCoconesIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {K : Type u₁} [Category.{v₂, u₁} K] (F : Functor J C) (G : Functor K C) (h : F.cocones ≅ G.cocones) [HasColimit F] : HasColimit G

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

noncomputable def CategoryTheory.Limits.HasColimit.isoOfNatIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasColimit F] [HasColimit G] (w : F ≅ G) : colimit F ≅ colimit G

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

@[simp]

theorem CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasColimit F] [HasColimit G] (w : F ≅ G) (j : J) : CategoryStruct.comp (colimit.ι F j) (isoOfNatIso w).hom = CategoryStruct.comp (w.hom.app j) (colimit.ι G j)

@[simp]

theorem CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasColimit F] [HasColimit G] (w : F ≅ G) (j : J) {Z : C} (h : colimit G ⟶ Z) : CategoryStruct.comp (colimit.ι F j) (CategoryStruct.comp (isoOfNatIso w).hom h) = CategoryStruct.comp (w.hom.app j) (CategoryStruct.comp (colimit.ι G j) h)

@[simp]

theorem CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_inv {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasColimit F] [HasColimit G] (w : F ≅ G) (j : J) : CategoryStruct.comp (colimit.ι G j) (isoOfNatIso w).inv = CategoryStruct.comp (w.inv.app j) (colimit.ι F j)

@[simp]

theorem CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_inv_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasColimit F] [HasColimit G] (w : F ≅ G) (j : J) {Z : C} (h : colimit F ⟶ Z) : CategoryStruct.comp (colimit.ι G j) (CategoryStruct.comp (isoOfNatIso w).inv h) = CategoryStruct.comp (w.inv.app j) (CategoryStruct.comp (colimit.ι F j) h)

@[simp]

theorem CategoryTheory.Limits.HasColimit.isoOfNatIso_hom_desc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasColimit F] [HasColimit G] (t : Cocone G) (w : F ≅ G) : CategoryStruct.comp (isoOfNatIso w).hom (colimit.desc G t) = colimit.desc F ((Cocone.precompose w.hom).obj t)

@[simp]

theorem CategoryTheory.Limits.HasColimit.isoOfNatIso_hom_desc_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasColimit F] [HasColimit G] (t : Cocone G) (w : F ≅ G) {Z : C} (h : t.pt ⟶ Z) : CategoryStruct.comp (isoOfNatIso w).hom (CategoryStruct.comp (colimit.desc G t) h) = CategoryStruct.comp (colimit.desc F ((Cocone.precompose w.hom).obj t)) h

@[simp]

theorem CategoryTheory.Limits.HasColimit.isoOfNatIso_inv_desc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasColimit F] [HasColimit G] (t : Cocone F) (w : F ≅ G) : CategoryStruct.comp (isoOfNatIso w).inv (colimit.desc F t) = colimit.desc G ((Cocone.precompose w.inv).obj t)

@[simp]

theorem CategoryTheory.Limits.HasColimit.isoOfNatIso_inv_desc_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasColimit F] [HasColimit G] (t : Cocone F) (w : F ≅ G) {Z : C} (h : t.pt ⟶ Z) : CategoryStruct.comp (isoOfNatIso w).inv (CategoryStruct.comp (colimit.desc F t) h) = CategoryStruct.comp (colimit.desc G ((Cocone.precompose w.inv).obj t)) h

noncomputable def CategoryTheory.Limits.HasColimit.isoOfEquivalence {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] {G : Functor K C} [HasColimit G] (e : J ≌ K) (w : e.functor.comp G ≅ F) : colimit F ≅ colimit G

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.

@[simp]

theorem CategoryTheory.Limits.HasColimit.isoOfEquivalence_hom_π {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] {G : Functor K C} [HasColimit G] (e : J ≌ K) (w : e.functor.comp G ≅ F) (j : J) : CategoryStruct.comp (colimit.ι F j) (isoOfEquivalence e w).hom = CategoryStruct.comp (F.map (e.unit.app j)) (CategoryStruct.comp (w.inv.app ((e.functor.comp e.inverse).obj j)) (colimit.ι G (e.functor.obj ((e.functor.comp e.inverse).obj j))))

@[simp]

theorem CategoryTheory.Limits.HasColimit.isoOfEquivalence_inv_π {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] {G : Functor K C} [HasColimit G] (e : J ≌ K) (w : e.functor.comp G ≅ F) (k : K) : CategoryStruct.comp (colimit.ι G k) (isoOfEquivalence e w).inv = CategoryStruct.comp (G.map (e.counitInv.app k)) (CategoryStruct.comp (w.hom.app (e.inverse.obj k)) (colimit.ι F (e.inverse.obj k)))

noncomputable def CategoryTheory.Limits.colimit.pre {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] (E : Functor K J) [HasColimit (E.comp F)] : colimit (E.comp F) ⟶ colimit F

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

@[simp]

theorem CategoryTheory.Limits.colimit.ι_pre {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] (E : Functor K J) [HasColimit (E.comp F)] (k : K) : CategoryStruct.comp (ι (E.comp F) k) (pre F E) = ι F (E.obj k)

@[simp]

theorem CategoryTheory.Limits.colimit.ι_pre_assoc {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] (E : Functor K J) [HasColimit (E.comp F)] (k : K) {Z : C} (h : colimit F ⟶ Z) : CategoryStruct.comp (ι (E.comp F) k) (CategoryStruct.comp (pre F E) h) = CategoryStruct.comp (ι F (E.obj k)) h

@[simp]

theorem CategoryTheory.Limits.colimit.ι_inv_pre {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] (E : Functor K J) [HasColimit (E.comp F)] [IsIso (pre F E)] (k : K) : CategoryStruct.comp (ι F (E.obj k)) (inv (pre F E)) = ι (E.comp F) k

@[simp]

theorem CategoryTheory.Limits.colimit.ι_inv_pre_assoc {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] (E : Functor K J) [HasColimit (E.comp F)] [IsIso (pre F E)] (k : K) {Z : C} (h : colimit (E.comp F) ⟶ Z) : CategoryStruct.comp (ι F (E.obj k)) (CategoryStruct.comp (inv (pre F E)) h) = CategoryStruct.comp (ι (E.comp F) k) h

@[simp]

theorem CategoryTheory.Limits.colimit.pre_desc {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] (E : Functor K J) [HasColimit (E.comp F)] (c : Cocone F) : CategoryStruct.comp (pre F E) (desc F c) = desc (E.comp F) (Cocone.whisker E c)

@[simp]

theorem CategoryTheory.Limits.colimit.pre_desc_assoc {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] (E : Functor K J) [HasColimit (E.comp F)] (c : Cocone F) {Z : C} (h : c.pt ⟶ Z) : CategoryStruct.comp (pre F E) (CategoryStruct.comp (desc F c) h) = CategoryStruct.comp (desc (E.comp F) (Cocone.whisker E c)) h

@[simp]

theorem CategoryTheory.Limits.colimit.pre_pre {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit F] (E : Functor K J) [HasColimit (E.comp F)] {L : Type u₃} [Category.{v₃, u₃} L] (D : Functor L K) [h : HasColimit (D.comp (E.comp F))] : CategoryStruct.comp (pre (E.comp F) D) (pre F E) = pre F (D.comp E)

theorem CategoryTheory.Limits.colimit.pre_eq {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] {E : Functor K J} [HasColimit (E.comp F)] (s : ColimitCocone (E.comp F)) (t : ColimitCocone F) : pre F E = CategoryStruct.comp (isoColimitCocone s).hom (CategoryStruct.comp (s.isColimit.desc (Cocone.whisker E t.cocone)) (isoColimitCocone t).inv)

If we have particular colimit cocones available for E ⋙ F and for F, we obtain a formula for colimit.pre F E.

noncomputable def CategoryTheory.Limits.colimit.post {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) {D : Type u'} [Category.{v', u'} D] [HasColimit F] (G : Functor C D) [HasColimit (F.comp G)] : colimit (F.comp G) ⟶ G.obj (colimit F)

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

@[simp]

theorem CategoryTheory.Limits.colimit.ι_post {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) {D : Type u'} [Category.{v', u'} D] [HasColimit F] (G : Functor C D) [HasColimit (F.comp G)] (j : J) : CategoryStruct.comp (ι (F.comp G) j) (post F G) = G.map (ι F j)

@[simp]

theorem CategoryTheory.Limits.colimit.ι_post_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) {D : Type u'} [Category.{v', u'} D] [HasColimit F] (G : Functor C D) [HasColimit (F.comp G)] (j : J) {Z : D} (h : G.obj (colimit F) ⟶ Z) : CategoryStruct.comp (ι (F.comp G) j) (CategoryStruct.comp (post F G) h) = CategoryStruct.comp (G.map (ι F j)) h

@[simp]

theorem CategoryTheory.Limits.colimit.post_desc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) {D : Type u'} [Category.{v', u'} D] [HasColimit F] (G : Functor C D) [HasColimit (F.comp G)] (c : Cocone F) : CategoryStruct.comp (post F G) (G.map (desc F c)) = desc (F.comp G) (G.mapCocone c)

@[simp]

theorem CategoryTheory.Limits.colimit.post_post {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) {D : Type u'} [Category.{v', u'} D] [HasColimit F] (G : Functor C D) [HasColimit (F.comp G)] {E : Type u''} [Category.{v'', u''} E] (H : Functor D E) [h : HasColimit ((F.comp G).comp H)] : CategoryStruct.comp (post (F.comp G) H) (H.map (post F G)) = post F (G.comp H)

theorem CategoryTheory.Limits.colimit.pre_post {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (E : Functor K J) (F : Functor J C) (G : Functor C D) [HasColimit F] [HasColimit (E.comp F)] [HasColimit (F.comp G)] [h : HasColimit ((E.comp F).comp G)] : CategoryStruct.comp (post (E.comp F) G) (G.map (pre F E)) = CategoryStruct.comp (pre (F.comp G) E) (post F G)

instance CategoryTheory.Limits.hasColimit_equivalence_comp {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] {F : Functor J C} (e : K ≌ J) [HasColimit F] : HasColimit (e.functor.comp F)

theorem CategoryTheory.Limits.hasColimit_of_equivalence_comp {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] {F : Functor J C} (e : K ≌ J) [HasColimit (e.functor.comp F)] : HasColimit F

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

theorem CategoryTheory.Limits.hasColimit_equivalence_comp_iff {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] {F : Functor J C} (e : K ≌ J) : HasColimit (e.functor.comp F) ↔ HasColimit F

theorem CategoryTheory.Limits.hasColimit_inverse_equivalence_comp_iff {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] {F : Functor J C} (e : J ≌ K) : HasColimit (e.inverse.comp F) ↔ HasColimit F

noncomputable def CategoryTheory.Limits.colim {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] [HasColimitsOfShape J C] : Functor (Functor J C) C

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

@[simp]

theorem CategoryTheory.Limits.colim_map {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] [HasColimitsOfShape J C] {X✝ Y✝ : Functor J C} (α : X✝ ⟶ Y✝) : colim.map α = colimMap α

@[simp]

theorem CategoryTheory.Limits.colim_obj {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] [HasColimitsOfShape J C] (F : Functor J C) : colim.obj F = colimit F

theorem CategoryTheory.Limits.colimMap_eq {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimitsOfShape J C] {G : Functor J C} (α : F ⟶ G) : colimMap α = colim.map α

theorem CategoryTheory.Limits.colimit.ι_map {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimitsOfShape J C] {G : Functor J C} (α : F ⟶ G) (j : J) : CategoryStruct.comp (ι F j) (colim.map α) = CategoryStruct.comp (α.app j) (ι G j)

theorem CategoryTheory.Limits.colimit.ι_map_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimitsOfShape J C] {G : Functor J C} (α : F ⟶ G) (j : J) {Z : C} (h : colim.obj G ⟶ Z) : CategoryStruct.comp (ι F j) (CategoryStruct.comp (colim.map α) h) = CategoryStruct.comp (α.app j) (CategoryStruct.comp (ι G j) h)

@[simp]

theorem CategoryTheory.Limits.colimit.map_desc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimitsOfShape J C] {G : Functor J C} (α : F ⟶ G) (c : Cocone G) : CategoryStruct.comp (colimMap α) (desc G c) = desc F ((Cocone.precompose α).obj c)

@[simp]

theorem CategoryTheory.Limits.colimit.map_desc_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimitsOfShape J C] {G : Functor J C} (α : F ⟶ G) (c : Cocone G) {Z : C} (h : c.pt ⟶ Z) : CategoryStruct.comp (colimMap α) (CategoryStruct.comp (desc G c) h) = CategoryStruct.comp (desc F ((Cocone.precompose α).obj c)) h

theorem CategoryTheory.Limits.colimit.pre_map {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimitsOfShape J C] {G : Functor J C} (α : F ⟶ G) [HasColimitsOfShape K C] (E : Functor K J) : CategoryStruct.comp (pre F E) (colim.map α) = CategoryStruct.comp (colim.map (E.whiskerLeft α)) (pre G E)

theorem CategoryTheory.Limits.colimit.pre_map' {J : Type u₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u} [Category.{v, u} C] [HasColimitsOfShape J C] [HasColimitsOfShape K C] (F : Functor J C) {E₁ E₂ : Functor K J} (α : E₁ ⟶ E₂) : pre F E₁ = CategoryStruct.comp (colim.map (Functor.whiskerRight α F)) (pre F E₂)

theorem CategoryTheory.Limits.colimit.pre_id {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] [HasColimitsOfShape J C] (F : Functor J C) : pre F (Functor.id J) = colim.map F.leftUnitor.hom

theorem CategoryTheory.Limits.colimit.map_post {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimitsOfShape J C] {G : Functor J C} (α : F ⟶ G) {D : Type u'} [Category.{v', u'} D] [HasColimitsOfShape J D] (H : Functor C D) : CategoryStruct.comp (post F H) (H.map (colim.map α)) = CategoryStruct.comp (colim.map (Functor.whiskerRight α H)) (post G H)

noncomputable def CategoryTheory.Limits.colimCoyoneda {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] [HasColimitsOfShape J C] : colim.op.comp (coyoneda.comp ((Functor.whiskeringRight C (Type v) (Type (max v u₁))).obj uliftFunctor.{u₁, v})) ≅ cocones J C

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.

noncomputable def CategoryTheory.Limits.colimConstAdj {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] [HasColimitsOfShape J C] : colim ⊣ Functor.const J

The colimit functor and constant functor are adjoint to each other

instance CategoryTheory.Limits.instIsLeftAdjointFunctorColim {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] [HasColimitsOfShape J C] : colim.IsLeftAdjoint

instance CategoryTheory.Limits.colimMap_epi' {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasColimitsOfShape J C] (α : F ⟶ G) [Epi α] : Epi (colimMap α)

instance CategoryTheory.Limits.colimMap_epi {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasColimit F] [HasColimit G] (α : F ⟶ G) [∀ (j : J), Epi (α.app j)] : Epi (colimMap α)

theorem CategoryTheory.Limits.hasColimitsOfShape_of_equivalence {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {J' : Type u₂} [Category.{v₂, u₂} J'] (e : J ≌ J') [HasColimitsOfShape J C] : HasColimitsOfShape J' C

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

theorem CategoryTheory.Limits.HasColimitsOfShape.of_small (C : Type u) [Category.{v, u} C] [HasColimitsOfSize.{v₁, u₁, v, u} C] (J : Type u₂) [Category.{v₂, u₂} J] [Small.{u₁, u₂} J] [LocallySmall.{v₁, v₂, u₂} J] : HasColimitsOfShape J C

theorem CategoryTheory.Limits.HasColimitsOfShape.of_essentiallySmall (C : Type u) [Category.{v, u} C] [HasColimitsOfSize.{v₁, u₁, v, u} C] (J : Type u₂) [Category.{v₂, u₂} J] [EssentiallySmall.{u₁, v₂, u₂} J] [LocallySmall.{v₁, v₂, u₂} J] : HasColimitsOfShape J C

theorem CategoryTheory.Limits.hasColimitsOfSizeOfUnivLE (C : Type u) [Category.{v, u} C] [UnivLE.{v₂, v₁}] [UnivLE.{u₂, u₁}] [HasColimitsOfSize.{v₁, u₁, v, u} C] : HasColimitsOfSize.{v₂, u₂, v, u} C

A category that has larger colimits also has smaller colimits.

theorem CategoryTheory.Limits.hasColimitsOfSizeShrink (C : Type u) [Category.{v, u} C] [HasColimitsOfSize.{max v₁ v₂, max u₁ u₂, v, u} C] : HasColimitsOfSize.{v₁, u₁, v, u} C

hasColimitsOfSizeShrink.{v u} C tries to obtain HasColimitsOfSize.{v u} C from some other HasColimitsOfSize C.

@[instance 100]

instance CategoryTheory.Limits.hasSmallestColimitsOfHasColimits (C : Type u) [Category.{v, u} C] [HasColimits C] : HasColimitsOfSize.{0, 0, v, u} C

def CategoryTheory.Limits.IsLimit.op {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} {t : Cone F} (P : IsLimit t) : IsColimit t.op

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

def CategoryTheory.Limits.IsColimit.op {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} {t : Cocone F} (P : IsColimit t) : IsLimit t.op

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

def CategoryTheory.Limits.IsLimit.unop {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} {t : Cone F.op} (P : IsLimit t) : IsColimit t.unop

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

def CategoryTheory.Limits.IsColimit.unop {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} {t : Cocone F.op} (P : IsColimit t) : IsLimit t.unop

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

def CategoryTheory.Limits.isLimitOfOp {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} {t : Cone F} (P : IsColimit t.op) : IsLimit t

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

def CategoryTheory.Limits.isColimitOfOp {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} {t : Cocone F} (P : IsLimit t.op) : IsColimit t

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

def CategoryTheory.Limits.isLimitOfUnop {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} {t : Cone F.op} (P : IsColimit t.unop) : IsLimit t

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

def CategoryTheory.Limits.isColimitOfUnop {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} {t : Cocone F.op} (P : IsLimit t.unop) : IsColimit t

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

def CategoryTheory.Limits.isLimitEquivIsColimitOp {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} {t : Cone F} : IsLimit t ≃ IsColimit t.op

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

def CategoryTheory.Limits.isColimitEquivIsLimitOp {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} {t : Cocone F} : IsColimit t ≃ IsLimit t.op

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