# Limits and colimits #

We set up the general theory of limits and colimits in a category. In this introduction we only describe the setup for limits; it is repeated, with slightly different names, for colimits.

The main structures defined in this file is

• IsLimit c, for c : Cone F, F : J ⥤ C, expressing that c is a limit cone,

See also CategoryTheory.Limits.HasLimits which further builds:

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

## 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 #

structure CategoryTheory.Limits.IsLimit {J : Type u₁} [] {C : Type u₃} [] {F : } (t : ) :
Type (max (max u₁ u₃) v₃)

A cone t on F is a limit cone if each cone on F admits a unique cone morphism to t.

• lift : (s : ) → s.pt t.pt

There is a morphism from any cone point to t.pt

• fac : ∀ (s : ) (j : J), CategoryTheory.CategoryStruct.comp (self.lift s) (t.app j) = s.app j

The map makes the triangle with the two natural transformations commute

• uniq : ∀ (s : ) (m : s.pt t.pt), (∀ (j : J), CategoryTheory.CategoryStruct.comp m (t.app j) = s.app j)m = self.lift s

It is the unique such map to do this

Instances For
@[simp]
theorem CategoryTheory.Limits.IsLimit.fac {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (self : ) (s : ) (j : J) :
CategoryTheory.CategoryStruct.comp (self.lift s) (t.app j) = s.app j

The map makes the triangle with the two natural transformations commute

theorem CategoryTheory.Limits.IsLimit.uniq {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (self : ) (s : ) (m : s.pt t.pt) :
(∀ (j : J), CategoryTheory.CategoryStruct.comp m (t.app j) = s.app j)m = self.lift s

It is the unique such map to do this

@[simp]
theorem CategoryTheory.Limits.IsLimit.fac_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (self : ) (s : ) (j : J) {Z : C} (h : F.obj j Z) :
instance CategoryTheory.Limits.IsLimit.subsingleton {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } :
Equations
• =
def CategoryTheory.Limits.IsLimit.map {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (s : ) {t : } (α : F G) :
s.pt t.pt

Given a natural transformation α : F ⟶ G, we give a morphism from the cone point of any cone over F to the cone point of a limit cone over G.

Equations
• = P.lift ( s)
Instances For
@[simp]
theorem CategoryTheory.Limits.IsLimit.map_π_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (c : ) {d : } (hd : ) (α : F G) (j : J) {Z : C} (h : G.obj j Z) :
@[simp]
theorem CategoryTheory.Limits.IsLimit.map_π {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (c : ) {d : } (hd : ) (α : F G) (j : J) :
@[simp]
theorem CategoryTheory.Limits.IsLimit.lift_self {J : Type u₁} [] {C : Type u₃} [] {F : } {c : } :
t.lift c =
@[simp]
theorem CategoryTheory.Limits.IsLimit.liftConeMorphism_hom {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (s : ) :
(h.liftConeMorphism s).hom = h.lift s
def CategoryTheory.Limits.IsLimit.liftConeMorphism {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (s : ) :
s t

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

Equations
• h.liftConeMorphism s = { hom := h.lift s, w := }
Instances For
theorem CategoryTheory.Limits.IsLimit.uniq_cone_morphism {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {t : } {f : s t} {f' : s t} :
f = f'
theorem CategoryTheory.Limits.IsLimit.existsUnique {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (s : ) :
∃! l : s.pt t.pt, ∀ (j : J), CategoryTheory.CategoryStruct.comp l (t.app j) = s.app j

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

def CategoryTheory.Limits.IsLimit.ofExistsUnique {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (ht : ∀ (s : ), ∃! l : s.pt t.pt, ∀ (j : J), CategoryTheory.CategoryStruct.comp l (t.app j) = s.app j) :

Noncomputably make a limit cone from the existence of unique factorizations.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.IsLimit.mkConeMorphism_lift {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (lift : (s : ) → s t) (uniq : ∀ (s : ) (m : s t), m = lift s) (s : ) :
.lift s = (lift s).hom
def CategoryTheory.Limits.IsLimit.mkConeMorphism {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (lift : (s : ) → s t) (uniq : ∀ (s : ) (m : s t), m = lift s) :

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

Equations
• = { lift := fun (s : ) => (lift s).hom, fac := , uniq := }
Instances For
@[simp]
theorem CategoryTheory.Limits.IsLimit.uniqueUpToIso_hom {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {t : } :
(P.uniqueUpToIso Q).hom = Q.liftConeMorphism s
@[simp]
theorem CategoryTheory.Limits.IsLimit.uniqueUpToIso_inv {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {t : } :
(P.uniqueUpToIso Q).inv = P.liftConeMorphism t
def CategoryTheory.Limits.IsLimit.uniqueUpToIso {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {t : } :
s t

Limit cones on F are unique up to isomorphism.

Equations
• P.uniqueUpToIso Q = { hom := Q.liftConeMorphism s, inv := P.liftConeMorphism t, hom_inv_id := , inv_hom_id := }
Instances For
theorem CategoryTheory.Limits.IsLimit.hom_isIso {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {t : } (f : s t) :

Any cone morphism between limit cones is an isomorphism.

def CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {t : } :
s.pt t.pt

Limits of F are unique up to isomorphism.

Equations
• P.conePointUniqueUpToIso Q = .mapIso (P.uniqueUpToIso Q)
Instances For
@[simp]
theorem CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {t : } (j : J) {Z : C} (h : F.obj j Z) :
@[simp]
theorem CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {t : } (j : J) :
CategoryTheory.CategoryStruct.comp (P.conePointUniqueUpToIso Q).hom (t.app j) = s.app j
@[simp]
theorem CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {t : } (j : J) {Z : C} (h : F.obj j Z) :
@[simp]
theorem CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {t : } (j : J) :
CategoryTheory.CategoryStruct.comp (P.conePointUniqueUpToIso Q).inv (s.app j) = t.app j
@[simp]
theorem CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_hom_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {r : } {s : } {t : } {Z : C} (h : t.pt Z) :
@[simp]
theorem CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_hom {J : Type u₁} [] {C : Type u₃} [] {F : } {r : } {s : } {t : } :
CategoryTheory.CategoryStruct.comp (P.lift r) (P.conePointUniqueUpToIso Q).hom = Q.lift r
@[simp]
theorem CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_inv_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {r : } {s : } {t : } {Z : C} (h : s.pt Z) :
@[simp]
theorem CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_inv {J : Type u₁} [] {C : Type u₃} [] {F : } {r : } {s : } {t : } :
CategoryTheory.CategoryStruct.comp (Q.lift r) (P.conePointUniqueUpToIso Q).inv = P.lift r
def CategoryTheory.Limits.IsLimit.ofIsoLimit {J : Type u₁} [] {C : Type u₃} [] {F : } {r : } {t : } (i : r t) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.IsLimit.ofIsoLimit_lift {J : Type u₁} [] {C : Type u₃} [] {F : } {r : } {t : } (i : r t) (s : ) :
(P.ofIsoLimit i).lift s = CategoryTheory.CategoryStruct.comp (P.lift s) i.hom.hom
def CategoryTheory.Limits.IsLimit.equivIsoLimit {J : Type u₁} [] {C : Type u₃} [] {F : } {r : } {t : } (i : r t) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.IsLimit.equivIsoLimit_apply {J : Type u₁} [] {C : Type u₃} [] {F : } {r : } {t : } (i : r t) :
= P.ofIsoLimit i
@[simp]
theorem CategoryTheory.Limits.IsLimit.equivIsoLimit_symm_apply {J : Type u₁} [] {C : Type u₃} [] {F : } {r : } {t : } (i : r t) :
= P.ofIsoLimit i.symm
def CategoryTheory.Limits.IsLimit.ofPointIso {J : Type u₁} [] {C : Type u₃} [] {F : } {r : } {t : } [i : CategoryTheory.IsIso (P.lift t)] :

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

Equations
Instances For
theorem CategoryTheory.Limits.IsLimit.hom_lift {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } {W : C} (m : W t.pt) :
m = h.lift { pt := W, π := { app := fun (b : J) => CategoryTheory.CategoryStruct.comp m (t.app b), naturality := } }
theorem CategoryTheory.Limits.IsLimit.hom_ext {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } {W : C} {f : W t.pt} {f' : W t.pt} (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp f (t.app j) = CategoryTheory.CategoryStruct.comp f' (t.app j)) :
f = f'

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

def CategoryTheory.Limits.IsLimit.ofRightAdjoint {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {D : Type u₄} [] {G : } {right : } (adj : left right) {c : } :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.IsLimit.ofConeEquiv {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {D : Type u₄} [] {G : } {c : } :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.IsLimit.ofConeEquiv_apply_desc {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {D : Type u₄} [] {G : } {c : } (P : CategoryTheory.Limits.IsLimit (h.functor.obj c)) (s : ) :
.lift s = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (h.unitIso.hom.app s).hom (h.inverse.map (P.liftConeMorphism (h.functor.obj s))).hom) (h.unitIso.inv.app c).hom
@[simp]
theorem CategoryTheory.Limits.IsLimit.ofConeEquiv_symm_apply_desc {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {D : Type u₄} [] {G : } {c : } (s : ) :
( P).lift s = CategoryTheory.CategoryStruct.comp (h.counitIso.inv.app s).hom (h.functor.map (P.liftConeMorphism (h.inverse.obj s))).hom
def CategoryTheory.Limits.IsLimit.postcomposeHomEquiv {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : F G) (c : ) :

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

Equations
Instances For
def CategoryTheory.Limits.IsLimit.postcomposeInvEquiv {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : F G) (c : ) :

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

Equations
Instances For
def CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : F G) (c : ) (d : ) (w : .obj c d) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_inv {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {s : } {t : } (w : F G) :
(P.conePointsIsoOfNatIso Q w).inv =
@[simp]
theorem CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_hom {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {s : } {t : } (w : F G) :
(P.conePointsIsoOfNatIso Q w).hom =
def CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {s : } {t : } (w : F G) :
s.pt t.pt

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

Equations
• P.conePointsIsoOfNatIso Q w = { hom := , inv := , hom_inv_id := , inv_hom_id := }
Instances For
theorem CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_hom_comp_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {s : } {t : } (w : F G) (j : J) {Z : C} (h : G.obj j Z) :
theorem CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_hom_comp {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {s : } {t : } (w : F G) (j : J) :
CategoryTheory.CategoryStruct.comp (P.conePointsIsoOfNatIso Q w).hom (t.app j) = CategoryTheory.CategoryStruct.comp (s.app j) (w.hom.app j)
theorem CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_inv_comp_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {s : } {t : } (w : F G) (j : J) {Z : C} (h : F.obj j Z) :
theorem CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_inv_comp {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {s : } {t : } (w : F G) (j : J) :
CategoryTheory.CategoryStruct.comp (P.conePointsIsoOfNatIso Q w).inv (s.app j) = CategoryTheory.CategoryStruct.comp (t.app j) (w.inv.app j)
theorem CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_hom_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {r : } {s : } {t : } (w : F G) {Z : C} (h : t.pt Z) :
CategoryTheory.CategoryStruct.comp (P.lift r) (CategoryTheory.CategoryStruct.comp (P.conePointsIsoOfNatIso Q w).hom h) =
theorem CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_hom {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {r : } {s : } {t : } (w : F G) :
CategoryTheory.CategoryStruct.comp (P.lift r) (P.conePointsIsoOfNatIso Q w).hom =
theorem CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_inv_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {r : } {s : } {t : } (w : F G) {Z : C} (h : t.pt Z) :
CategoryTheory.CategoryStruct.comp (Q.lift r) (CategoryTheory.CategoryStruct.comp (P.conePointsIsoOfNatIso Q w).inv h) =
theorem CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_inv {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {r : } {s : } {t : } (w : F G) :
CategoryTheory.CategoryStruct.comp (Q.lift r) (P.conePointsIsoOfNatIso Q w).inv =
def CategoryTheory.Limits.IsLimit.whiskerEquivalence {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {s : } (e : K J) :

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

Equations
• P.whiskerEquivalence e =
Instances For
def CategoryTheory.Limits.IsLimit.ofWhiskerEquivalence {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {s : } (e : K J) (P : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.IsLimit.whiskerEquivalenceEquiv {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {s : } (e : K J) :

Given an equivalence of diagrams e, s is a limit cone iff s.whisker e.functor is.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.IsLimit.extendIso {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {X : C} (i : X s.pt) (hs : ) :

A limit cone extended by an isomorphism is a limit cone.

Equations
• = hs.ofIsoLimit
Instances For
def CategoryTheory.Limits.IsLimit.ofExtendIso {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {X : C} (i : X s.pt) (hs : CategoryTheory.Limits.IsLimit (s.extend i)) :

A cone is a limit cone if its extension by an isomorphism is.

Equations
• = hs.ofIsoLimit
Instances For
def CategoryTheory.Limits.IsLimit.extendIsoEquiv {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {X : C} (i : X s.pt) :

A cone is a limit cone iff its extension by an isomorphism is.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence_inv {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {s : } {G : } {t : } (e : J K) (w : e.functor.comp G F) :
(P.conePointsIsoOfEquivalence Q e w).inv = P.lift (.functor.obj t)
@[simp]
theorem CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence_hom {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {s : } {G : } {t : } (e : J K) (w : e.functor.comp G F) :
(P.conePointsIsoOfEquivalence Q e w).hom = Q.lift ((CategoryTheory.Limits.Cones.equivalenceOfReindexing e.symm ((CategoryTheory.isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G)).functor.obj s)
def CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {s : } {G : } {t : } (e : J K) (w : e.functor.comp G F) :
s.pt t.pt

We can prove two cone points (s : Cone F).pt and (t : Cone G).pt are isomorphic if

• both cones are limit cones
• their indexing categories are equivalent via some e : J ≌ K,
• the triangle of functors commutes up to a natural isomorphism: e.functor ⋙ G ≅ F.

This is the most general form of uniqueness of cone points, allowing relabelling of both the indexing category (up to equivalence) and the functor (up to natural isomorphism).

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.IsLimit.homIso {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (W : C) :
ULift.{u₁, v₃} (W t.pt) .obj W F

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.IsLimit.homIso_hom {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } {W : C} (f : ULift.{u₁, v₃} (W t.pt)) :
(h.homIso W).hom f = (t.extend f.down)
def CategoryTheory.Limits.IsLimit.natIso {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } :
(CategoryTheory.yoneda.obj t.pt).comp CategoryTheory.uliftFunctor.{u₁, v₃} F.cones

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

Equations
Instances For
def CategoryTheory.Limits.IsLimit.homIso' {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (W : C) :
ULift.{u₁, v₃} (W t.pt) { p : (j : J) → W F.obj j // ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp (p j) (F.map f) = p j' }

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.IsLimit.ofFaithful {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } {D : Type u₄} [] (G : ) [G.Faithful] (ht : CategoryTheory.Limits.IsLimit (G.mapCone t)) (lift : (s : ) → s.pt t.pt) (h : ∀ (s : ), G.map (lift s) = ht.lift (G.mapCone s)) :

If G : C → D is a faithful functor which sends t to a limit cone, then it suffices to check that the induced maps for the image of t can be lifted to maps of C.

Equations
• = { lift := lift, fac := , uniq := }
Instances For
def CategoryTheory.Limits.IsLimit.mapConeEquiv {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {K : } {F : } {G : } (h : F G) {c : } (t : CategoryTheory.Limits.IsLimit (F.mapCone c)) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.IsLimit.isoUniqueConeMorphism {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } :
(s : ) → Unique (s t)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom {J : Type u₁} [] {C : Type u₃} [] {F : } {X : C} (h : (CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{u₁, v₃} F.cones) {Y : C} (f : Y X) :

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

Equations
• = { pt := Y, π := h.hom.app (Opposite.op Y) { down := f } }
Instances For
def CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone {J : Type u₁} [] {C : Type u₃} [] {F : } {X : C} (h : (CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{u₁, v₃} F.cones) (s : ) :
s.pt X

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom_homOfCone {J : Type u₁} [] {C : Type u₃} [] {F : } {X : C} (h : (CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{u₁, v₃} F.cones) (s : ) :
@[simp]
theorem CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone_coneOfHom {J : Type u₁} [] {C : Type u₃} [] {F : } {X : C} (h : (CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{u₁, v₃} F.cones) {Y : C} (f : Y X) :
def CategoryTheory.Limits.IsLimit.OfNatIso.limitCone {J : Type u₁} [] {C : Type u₃} [] {F : } {X : C} (h : (CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{u₁, v₃} F.cones) :

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

Equations
Instances For
theorem CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom_fac {J : Type u₁} [] {C : Type u₃} [] {F : } {X : C} (h : (CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{u₁, v₃} F.cones) {Y : C} (f : Y X) :

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

theorem CategoryTheory.Limits.IsLimit.OfNatIso.cone_fac {J : Type u₁} [] {C : Type u₃} [] {F : } {X : C} (h : (CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{u₁, v₃} F.cones) (s : ) :

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

def CategoryTheory.Limits.IsLimit.ofNatIso {J : Type u₁} [] {C : Type u₃} [] {F : } {X : C} (h : (CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{u₁, v₃} F.cones) :

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

Equations
• = { lift := , fac := , uniq := }
Instances For
structure CategoryTheory.Limits.IsColimit {J : Type u₁} [] {C : Type u₃} [] {F : } (t : ) :
Type (max (max u₁ u₃) v₃)

A cocone t on F is a colimit cocone if each cocone on F admits a unique cocone morphism from t.

• desc : (s : ) → t.pt s.pt

t.pt maps to all other cocone covertices

• fac : ∀ (s : ) (j : J), CategoryTheory.CategoryStruct.comp (t.app j) (self.desc s) = s.app j

The map desc makes the diagram with the natural transformations commute

• uniq : ∀ (s : ) (m : t.pt s.pt), (∀ (j : J), CategoryTheory.CategoryStruct.comp (t.app j) m = s.app j)m = self.desc s

desc is the unique such map

Instances For
@[simp]
theorem CategoryTheory.Limits.IsColimit.fac {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (self : ) (s : ) (j : J) :
CategoryTheory.CategoryStruct.comp (t.app j) (self.desc s) = s.app j

The map desc makes the diagram with the natural transformations commute

theorem CategoryTheory.Limits.IsColimit.uniq {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (self : ) (s : ) (m : t.pt s.pt) :
(∀ (j : J), CategoryTheory.CategoryStruct.comp (t.app j) m = s.app j)m = self.desc s

desc is the unique such map

@[simp]
theorem CategoryTheory.Limits.IsColimit.fac_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (self : ) (s : ) (j : J) {Z : C} (h : s.pt Z) :
instance CategoryTheory.Limits.IsColimit.subsingleton {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } :
Equations
• =
def CategoryTheory.Limits.IsColimit.map {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {s : } (t : ) (α : F G) :
s.pt t.pt

Given a natural transformation α : F ⟶ G, we give a morphism from the cocone point of a colimit cocone over F to the cocone point of any cocone over G.

Equations
• P.map t α = P.desc ( t)
Instances For
@[simp]
theorem CategoryTheory.Limits.IsColimit.ι_map_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {c : } (hc : ) (d : ) (α : F G) (j : J) {Z : C} (h : d.pt Z) :
@[simp]
theorem CategoryTheory.Limits.IsColimit.ι_map {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {c : } (hc : ) (d : ) (α : F G) (j : J) :
CategoryTheory.CategoryStruct.comp (c.app j) (hc.map d α) = CategoryTheory.CategoryStruct.comp (α.app j) (d.app j)
@[simp]
theorem CategoryTheory.Limits.IsColimit.desc_self {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } :
h.desc t =
@[simp]
theorem CategoryTheory.Limits.IsColimit.descCoconeMorphism_hom {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (s : ) :
(h.descCoconeMorphism s).hom = h.desc s
def CategoryTheory.Limits.IsColimit.descCoconeMorphism {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (s : ) :
t s

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

Equations
• h.descCoconeMorphism s = { hom := h.desc s, w := }
Instances For
theorem CategoryTheory.Limits.IsColimit.uniq_cocone_morphism {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {t : } {f : t s} {f' : t s} :
f = f'
theorem CategoryTheory.Limits.IsColimit.existsUnique {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (s : ) :
∃! d : t.pt s.pt, ∀ (j : J), CategoryTheory.CategoryStruct.comp (t.app j) d = s.app j

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

def CategoryTheory.Limits.IsColimit.ofExistsUnique {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (ht : ∀ (s : ), ∃! d : t.pt s.pt, ∀ (j : J), CategoryTheory.CategoryStruct.comp (t.app j) d = s.app j) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.IsColimit.mkCoconeMorphism_desc {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (desc : (s : ) → t s) (uniq' : ∀ (s : ) (m : t s), m = desc s) (s : ) :
.desc s = (desc s).hom
def CategoryTheory.Limits.IsColimit.mkCoconeMorphism {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (desc : (s : ) → t s) (uniq' : ∀ (s : ) (m : t s), m = desc s) :

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

Equations
• = { desc := fun (s : ) => (desc s).hom, fac := , uniq := }
Instances For
@[simp]
theorem CategoryTheory.Limits.IsColimit.uniqueUpToIso_hom {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {t : } :
(P.uniqueUpToIso Q).hom = P.descCoconeMorphism t
@[simp]
theorem CategoryTheory.Limits.IsColimit.uniqueUpToIso_inv {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {t : } :
(P.uniqueUpToIso Q).inv = Q.descCoconeMorphism s
def CategoryTheory.Limits.IsColimit.uniqueUpToIso {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {t : } :
s t

Colimit cocones on F are unique up to isomorphism.

Equations
• P.uniqueUpToIso Q = { hom := P.descCoconeMorphism t, inv := Q.descCoconeMorphism s, hom_inv_id := , inv_hom_id := }
Instances For
theorem CategoryTheory.Limits.IsColimit.hom_isIso {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {t : } (f : s t) :

Any cocone morphism between colimit cocones is an isomorphism.

def CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {t : } :
s.pt t.pt

Colimits of F are unique up to isomorphism.

Equations
• P.coconePointUniqueUpToIso Q = .mapIso (P.uniqueUpToIso Q)
Instances For
@[simp]
theorem CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {t : } (j : J) {Z : C} (h : t.pt Z) :
CategoryTheory.CategoryStruct.comp (s.app j) (CategoryTheory.CategoryStruct.comp (P.coconePointUniqueUpToIso Q).hom h) = CategoryTheory.CategoryStruct.comp (t.app j) h
@[simp]
theorem CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {t : } (j : J) :
CategoryTheory.CategoryStruct.comp (s.app j) (P.coconePointUniqueUpToIso Q).hom = t.app j
@[simp]
theorem CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {t : } (j : J) {Z : C} (h : s.pt Z) :
CategoryTheory.CategoryStruct.comp (t.app j) (CategoryTheory.CategoryStruct.comp (P.coconePointUniqueUpToIso Q).inv h) = CategoryTheory.CategoryStruct.comp (s.app j) h
@[simp]
theorem CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {t : } (j : J) :
CategoryTheory.CategoryStruct.comp (t.app j) (P.coconePointUniqueUpToIso Q).inv = s.app j
@[simp]
theorem CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_hom_desc_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {r : } {s : } {t : } {Z : C} (h : r.pt Z) :
@[simp]
theorem CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_hom_desc {J : Type u₁} [] {C : Type u₃} [] {F : } {r : } {s : } {t : } :
CategoryTheory.CategoryStruct.comp (P.coconePointUniqueUpToIso Q).hom (Q.desc r) = P.desc r
@[simp]
theorem CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_inv_desc_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {r : } {s : } {t : } {Z : C} (h : r.pt Z) :
@[simp]
theorem CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_inv_desc {J : Type u₁} [] {C : Type u₃} [] {F : } {r : } {s : } {t : } :
CategoryTheory.CategoryStruct.comp (P.coconePointUniqueUpToIso Q).inv (P.desc r) = Q.desc r
def CategoryTheory.Limits.IsColimit.ofIsoColimit {J : Type u₁} [] {C : Type u₃} [] {F : } {r : } {t : } (i : r t) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.IsColimit.ofIsoColimit_desc {J : Type u₁} [] {C : Type u₃} [] {F : } {r : } {t : } (i : r t) (s : ) :
(P.ofIsoColimit i).desc s = CategoryTheory.CategoryStruct.comp i.inv.hom (P.desc s)
def CategoryTheory.Limits.IsColimit.equivIsoColimit {J : Type u₁} [] {C : Type u₃} [] {F : } {r : } {t : } (i : r t) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.IsColimit.equivIsoColimit_apply {J : Type u₁} [] {C : Type u₃} [] {F : } {r : } {t : } (i : r t) :
= P.ofIsoColimit i
@[simp]
theorem CategoryTheory.Limits.IsColimit.equivIsoColimit_symm_apply {J : Type u₁} [] {C : Type u₃} [] {F : } {r : } {t : } (i : r t) :
= P.ofIsoColimit i.symm
def CategoryTheory.Limits.IsColimit.ofPointIso {J : Type u₁} [] {C : Type u₃} [] {F : } {r : } {t : } [i : CategoryTheory.IsIso (P.desc t)] :

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

Equations
Instances For
theorem CategoryTheory.Limits.IsColimit.hom_desc {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } {W : C} (m : t.pt W) :
m = h.desc { pt := W, ι := { app := fun (b : J) => CategoryTheory.CategoryStruct.comp (t.app b) m, naturality := } }
theorem CategoryTheory.Limits.IsColimit.hom_ext {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } {W : C} {f : t.pt W} {f' : t.pt W} (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (t.app j) f = CategoryTheory.CategoryStruct.comp (t.app j) f') :
f = f'

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

def CategoryTheory.Limits.IsColimit.ofLeftAdjoint {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {D : Type u₄} [] {G : } (adj : left right) {c : } :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.IsColimit.ofCoconeEquiv {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {D : Type u₄} [] {G : } {c : } :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.IsColimit.ofCoconeEquiv_apply_desc {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {D : Type u₄} [] {G : } {c : } (P : CategoryTheory.Limits.IsColimit (h.functor.obj c)) (s : ) :
.desc s = CategoryTheory.CategoryStruct.comp (h.unit.app c).hom (CategoryTheory.CategoryStruct.comp (h.inverse.map (P.descCoconeMorphism (h.functor.obj s))).hom (h.unitInv.app s).hom)
@[simp]
theorem CategoryTheory.Limits.IsColimit.ofCoconeEquiv_symm_apply_desc {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {D : Type u₄} [] {G : } {c : } (s : ) :
( P).desc s = CategoryTheory.CategoryStruct.comp (h.functor.map (P.descCoconeMorphism (h.inverse.obj s))).hom (h.counit.app s).hom
def CategoryTheory.Limits.IsColimit.precomposeHomEquiv {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : F G) (c : ) :

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

Equations
Instances For
def CategoryTheory.Limits.IsColimit.precomposeInvEquiv {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : F G) (c : ) :

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

Equations
Instances For
def CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } (α : F G) (c : ) (d : ) (w : .obj c d) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_inv {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {s : } {t : } (w : F G) :
(P.coconePointsIsoOfNatIso Q w).inv = Q.map s w.inv
@[simp]
theorem CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_hom {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {s : } {t : } (w : F G) :
(P.coconePointsIsoOfNatIso Q w).hom = P.map t w.hom
def CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {s : } {t : } (w : F G) :
s.pt t.pt

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

Equations
• P.coconePointsIsoOfNatIso Q w = { hom := P.map t w.hom, inv := Q.map s w.inv, hom_inv_id := , inv_hom_id := }
Instances For
theorem CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_hom_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {s : } {t : } (w : F G) (j : J) {Z : C} (h : t.pt Z) :
theorem CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_hom {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {s : } {t : } (w : F G) (j : J) :
CategoryTheory.CategoryStruct.comp (s.app j) (P.coconePointsIsoOfNatIso Q w).hom = CategoryTheory.CategoryStruct.comp (w.hom.app j) (t.app j)
theorem CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_inv_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {s : } {t : } (w : F G) (j : J) {Z : C} (h : s.pt Z) :
theorem CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_inv {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {s : } {t : } (w : F G) (j : J) :
CategoryTheory.CategoryStruct.comp (t.app j) (P.coconePointsIsoOfNatIso Q w).inv = CategoryTheory.CategoryStruct.comp (w.inv.app j) (s.app j)
theorem CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_hom_desc_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {s : } {r : } {t : } (w : F G) {Z : C} (h : r.pt Z) :
CategoryTheory.CategoryStruct.comp (P.coconePointsIsoOfNatIso Q w).hom (CategoryTheory.CategoryStruct.comp (Q.desc r) h) = CategoryTheory.CategoryStruct.comp (P.map r w.hom) h
theorem CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_hom_desc {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {s : } {r : } {t : } (w : F G) :
CategoryTheory.CategoryStruct.comp (P.coconePointsIsoOfNatIso Q w).hom (Q.desc r) = P.map r w.hom
theorem CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_inv_desc_assoc {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {s : } {r : } {t : } (w : F G) {Z : C} (h : r.pt Z) :
CategoryTheory.CategoryStruct.comp (P.coconePointsIsoOfNatIso Q w).inv (CategoryTheory.CategoryStruct.comp (P.desc r) h) = CategoryTheory.CategoryStruct.comp (Q.map r w.inv) h
theorem CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_inv_desc {J : Type u₁} [] {C : Type u₃} [] {F : } {G : } {s : } {r : } {t : } (w : F G) :
CategoryTheory.CategoryStruct.comp (P.coconePointsIsoOfNatIso Q w).inv (P.desc r) = Q.map r w.inv
def CategoryTheory.Limits.IsColimit.whiskerEquivalence {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {s : } (e : K J) :

If s : Cocone F is a colimit cocone, so is s whiskered by an equivalence e.

Equations
• P.whiskerEquivalence e =
Instances For
def CategoryTheory.Limits.IsColimit.ofWhiskerEquivalence {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {s : } (e : K J) (P : ) :

If s : Cocone F whiskered by an equivalence e is a colimit cocone, so is s.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.IsColimit.whiskerEquivalenceEquiv {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {s : } (e : K J) :

Given an equivalence of diagrams e, s is a colimit cocone iff s.whisker e.functor is.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.IsColimit.extendIso {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {X : C} (i : s.pt X) (hs : ) :

A colimit cocone extended by an isomorphism is a colimit cocone.

Equations
• = hs.ofIsoColimit
Instances For
def CategoryTheory.Limits.IsColimit.ofExtendIso {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {X : C} (i : s.pt X) (hs : CategoryTheory.Limits.IsColimit (s.extend i)) :

A cocone is a colimit cocone if its extension by an isomorphism is.

Equations
• = hs.ofIsoColimit
Instances For
def CategoryTheory.Limits.IsColimit.extendIsoEquiv {J : Type u₁} [] {C : Type u₃} [] {F : } {s : } {X : C} (i : s.pt X) :

A cocone is a colimit cocone iff its extension by an isomorphism is.

Equations
Instances For
@[simp]
theorem CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence_hom {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {s : } {G : } {t : } (e : J K) (w : e.functor.comp G F) :
(P.coconePointsIsoOfEquivalence Q e w).hom = P.desc (.functor.obj t)
@[simp]
theorem CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence_inv {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {s : } {G : } {t : } (e : J K) (w : e.functor.comp G F) :
(P.coconePointsIsoOfEquivalence Q e w).inv = Q.desc ((CategoryTheory.Limits.Cocones.equivalenceOfReindexing e.symm ((CategoryTheory.isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G)).functor.obj s)
def CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence {J : Type u₁} [] {K : Type u₂} [] {C : Type u₃} [] {F : } {s : } {G : } {t : } (e : J K) (w : e.functor.comp G F) :
s.pt t.pt

We can prove two cocone points (s : Cocone F).pt and (t : Cocone G).pt are isomorphic if

• both cocones are colimit cocones
• their indexing categories are equivalent via some e : J ≌ K,
• the triangle of functors commutes up to a natural isomorphism: e.functor ⋙ G ≅ F.

This is the most general form of uniqueness of cocone points, allowing relabelling of both the indexing category (up to equivalence) and the functor (up to natural isomorphism).

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.IsColimit.homEquiv {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (W : C) :
(t.pt W) (F .obj W)

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

Equations
• h.homEquiv W = { toFun := fun (f : t.pt W) => (t.extend f), invFun := fun (ι : F .obj W) => h.desc { pt := W, ι := ι }, left_inv := , right_inv := }
Instances For
@[simp]
theorem CategoryTheory.Limits.IsColimit.homEquiv_apply {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } {W : C} (f : t.pt W) :
(h.homEquiv W) f = (t.extend f)
def CategoryTheory.Limits.IsColimit.homIso {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (W : C) :
ULift.{u₁, v₃} (t.pt W) F .obj W

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

Equations
• h.homIso W = (Equiv.ulift.trans (h.homEquiv W)).toIso
Instances For
@[simp]
theorem CategoryTheory.Limits.IsColimit.homIso_hom {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } {W : C} (f : ULift.{u₁, v₃} (t.pt W)) :
(h.homIso W).hom f = (t.extend f.down)
def CategoryTheory.Limits.IsColimit.natIso {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } :
(CategoryTheory.coyoneda.obj (Opposite.op t.pt)).comp CategoryTheory.uliftFunctor.{u₁, v₃} F.cocones

The colimit of F represents the functor taking W to the set of cocones on F with cone point W.

Equations
Instances For
def CategoryTheory.Limits.IsColimit.homIso' {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } (W : C) :
ULift.{u₁, v₃} (t.pt W) { p : (j : J) → F.obj j W // ∀ {j j' : J} (f : j j'), CategoryTheory.CategoryStruct.comp (F.map f) (p j') = p j }

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.IsColimit.ofFaithful {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } {D : Type u₄} [] (G : ) [G.Faithful] (ht : CategoryTheory.Limits.IsColimit (G.mapCocone t)) (desc : (s : ) → t.pt s.pt) (h : ∀ (s : ), G.map (desc s) = ht.desc (G.mapCocone s)) :

If G : C → D is a faithful functor which sends t to a colimit cocone, then it suffices to check that the induced maps for the image of t can be lifted to maps of C.

Equations
• = { desc := desc, fac := , uniq := }
Instances For
def CategoryTheory.Limits.IsColimit.mapCoconeEquiv {J : Type u₁} [] {C : Type u₃} [] {D : Type u₄} [] {K : } {F : } {G : } (h : F G) {c : } (t : CategoryTheory.Limits.IsColimit (F.mapCocone c)) :

If F and G are naturally isomorphic, then F.mapCocone c being a colimit implies G.mapCocone c is also a colimit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.IsColimit.isoUniqueCoconeMorphism {J : Type u₁} [] {C : Type u₃} [] {F : } {t : } :
(s : ) → Unique (t s)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom {J : Type u₁} [] {C : Type u₃} [] {F : } {X : C} (h : (CategoryTheory.coyoneda.obj (Opposite.op X)).comp CategoryTheory.uliftFunctor.{u₁, v₃} F.cocones) {Y : C} (f : X Y) :

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

Equations
• = { pt := Y, ι := h.hom.app Y { down := f } }
Instances For
def CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone {J : Type u₁} [] {C : Type u₃} [] {F : } {X : C} (h : (CategoryTheory.coyoneda.obj (Opposite.op X)).comp CategoryTheory.uliftFunctor.{u₁, v₃} F.cocones) (s : ) :
X s.pt

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

Equations
• = (h.inv.app s.pt s).down
Instances For
@[simp]
theorem CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom_homOfCocone {J : Type u₁} [] {C : Type u₃} [] {F : } {X : C} (h : (CategoryTheory.coyoneda.obj (Opposite.op X)).comp CategoryTheory.uliftFunctor.{u₁, v₃} F.cocones) (s : ) :
@[simp]
theorem CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone_cooneOfHom {J : Type u₁} [] {C : Type u₃} [] {F : } {X : C} (h : (CategoryTheory.coyoneda.obj (Opposite.op X)).comp CategoryTheory.uliftFunctor.{u₁, v₃} F.cocones) {Y : C} (f : X Y) :
def CategoryTheory.Limits.IsColimit.OfNatIso.colimitCocone {J : Type u₁} [] {C : Type u₃} [] {F : } {X : C} (h : (CategoryTheory.coyoneda.obj (Opposite.op X)).comp CategoryTheory.uliftFunctor.{u₁, v₃} F.cocones) :

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

Equations
Instances For
theorem CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom_fac {J : Type u₁} [] {C : Type u₃} [] {F : } {X : C} (h : (CategoryTheory.coyoneda.obj (Opposite.op X)).comp CategoryTheory.uliftFunctor.{u₁, v₃} F.cocones) {Y : C} (f : X Y) :

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

theorem CategoryTheory.Limits.IsColimit.OfNatIso.cocone_fac {J : Type u₁} [] {C : Type u₃} [] {F : } {X : C} (h : (CategoryTheory.coyoneda.obj (Opposite.op X)).comp CategoryTheory.uliftFunctor.{u₁, v₃} F.cocones) (s : ) :

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

def CategoryTheory.Limits.IsColimit.ofNatIso {J : Type u₁} [] {C : Type u₃} [] {F : } {X : C} (h : (CategoryTheory.coyoneda.obj (Opposite.op X)).comp CategoryTheory.uliftFunctor.{u₁, v₃} F.cocones) :

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

Equations
• = { desc := , fac := , uniq := }
Instances For