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

• Stacks: Limits and colimits

structure CategoryTheory.Limits.IsLimit {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (t : Cone F) : 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.

See https://stacks.math.columbia.edu/tag/002E.

• lift (s : Cone F) : s.pt ⟶ t.pt

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

• fac (s : Cone F) (j : J) : CategoryStruct.comp (self.lift s) (t.π.app j) = s.π.app j

  The map makes the triangle with the two natural transformations commute

• uniq (s : Cone F) (m : s.pt ⟶ t.pt) : (∀ (j : J), 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₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cone F} (self : IsLimit t) (s : Cone F) (j : J) {Z : C} (h : F.obj j ⟶ Z) : CategoryStruct.comp (self.lift s) (CategoryStruct.comp (t.π.app j) h) = CategoryStruct.comp (s.π.app j) h

instance CategoryTheory.Limits.IsLimit.subsingleton {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cone F} : Subsingleton (IsLimit t)

def CategoryTheory.Limits.IsLimit.map {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} (s : Cone F) {t : Cone G} (P : IsLimit 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

• CategoryTheory.Limits.IsLimit.map s P α = P.lift ((CategoryTheory.Limits.Cones.postcompose α).obj s)

@[simp]

theorem CategoryTheory.Limits.IsLimit.map_π {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} (c : Cone F) {d : Cone G} (hd : IsLimit d) (α : F ⟶ G) (j : J) : CategoryStruct.comp (map c hd α) (d.π.app j) = CategoryStruct.comp (c.π.app j) (α.app j)

@[simp]

theorem CategoryTheory.Limits.IsLimit.map_π_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} (c : Cone F) {d : Cone G} (hd : IsLimit d) (α : F ⟶ G) (j : J) {Z : C} (h : G.obj j ⟶ Z) : CategoryStruct.comp (map c hd α) (CategoryStruct.comp (d.π.app j) h) = CategoryStruct.comp (c.π.app j) (CategoryStruct.comp (α.app j) h)

@[simp]

theorem CategoryTheory.Limits.IsLimit.lift_self {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {c : Cone F} (t : IsLimit c) : t.lift c = CategoryStruct.id c.pt

def CategoryTheory.Limits.IsLimit.liftConeMorphism {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cone F} (h : IsLimit t) (s : Cone F) : s ⟶ t

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

Equations

• h.liftConeMorphism s = { hom := h.lift s, w := ⋯ }

@[simp]

theorem CategoryTheory.Limits.IsLimit.liftConeMorphism_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cone F} (h : IsLimit t) (s : Cone F) : (h.liftConeMorphism s).hom = h.lift s

theorem CategoryTheory.Limits.IsLimit.uniq_cone_morphism {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s t : Cone F} (h : IsLimit t) {f f' : s ⟶ t} : f = f'

theorem CategoryTheory.Limits.IsLimit.existsUnique {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cone F} (h : IsLimit t) (s : Cone F) : ∃! l : s.pt ⟶ t.pt, ∀ (j : J), 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₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cone F} (ht : ∀ (s : Cone F), ∃! l : s.pt ⟶ t.pt, ∀ (j : J), CategoryStruct.comp l (t.π.app j) = s.π.app j) : IsLimit t

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.IsLimit.mkConeMorphism {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cone F} (lift : (s : Cone F) → s ⟶ t) (uniq : ∀ (s : Cone F) (m : s ⟶ t), m = lift s) : IsLimit t

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

Equations

• CategoryTheory.Limits.IsLimit.mkConeMorphism lift uniq = { lift := fun (s : CategoryTheory.Limits.Cone F) => (lift s).hom, fac := ⋯, uniq := ⋯ }

@[simp]

theorem CategoryTheory.Limits.IsLimit.mkConeMorphism_lift {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cone F} (lift : (s : Cone F) → s ⟶ t) (uniq : ∀ (s : Cone F) (m : s ⟶ t), m = lift s) (s : Cone F) : (mkConeMorphism lift uniq).lift s = (lift s).hom

def CategoryTheory.Limits.IsLimit.uniqueUpToIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s t : Cone F} (P : IsLimit s) (Q : IsLimit 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 := ⋯ }

@[simp]

theorem CategoryTheory.Limits.IsLimit.uniqueUpToIso_inv {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s t : Cone F} (P : IsLimit s) (Q : IsLimit t) : (P.uniqueUpToIso Q).inv = P.liftConeMorphism t

@[simp]

theorem CategoryTheory.Limits.IsLimit.uniqueUpToIso_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s t : Cone F} (P : IsLimit s) (Q : IsLimit t) : (P.uniqueUpToIso Q).hom = Q.liftConeMorphism s

theorem CategoryTheory.Limits.IsLimit.hom_isIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s t : Cone F} (P : IsLimit s) (Q : IsLimit t) (f : s ⟶ t) : IsIso f

Any cone morphism between limit cones is an isomorphism.

def CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s t : Cone F} (P : IsLimit s) (Q : IsLimit t) : s.pt ≅ t.pt

Limits of F are unique up to isomorphism.

Equations

• P.conePointUniqueUpToIso Q = (CategoryTheory.Limits.Cones.forget F).mapIso (P.uniqueUpToIso Q)

@[simp]

theorem CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s t : Cone F} (P : IsLimit s) (Q : IsLimit t) (j : J) : CategoryStruct.comp (P.conePointUniqueUpToIso Q).hom (t.π.app j) = s.π.app j

@[simp]

theorem CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s t : Cone F} (P : IsLimit s) (Q : IsLimit t) (j : J) {Z : C} (h : F.obj j ⟶ Z) : CategoryStruct.comp (P.conePointUniqueUpToIso Q).hom (CategoryStruct.comp (t.π.app j) h) = CategoryStruct.comp (s.π.app j) h

@[simp]

theorem CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s t : Cone F} (P : IsLimit s) (Q : IsLimit t) (j : J) : CategoryStruct.comp (P.conePointUniqueUpToIso Q).inv (s.π.app j) = t.π.app j

@[simp]

theorem CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s t : Cone F} (P : IsLimit s) (Q : IsLimit t) (j : J) {Z : C} (h : F.obj j ⟶ Z) : CategoryStruct.comp (P.conePointUniqueUpToIso Q).inv (CategoryStruct.comp (s.π.app j) h) = CategoryStruct.comp (t.π.app j) h

@[simp]

theorem CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {r s t : Cone F} (P : IsLimit s) (Q : IsLimit t) : CategoryStruct.comp (P.lift r) (P.conePointUniqueUpToIso Q).hom = Q.lift r

@[simp]

theorem CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_hom_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {r s t : Cone F} (P : IsLimit s) (Q : IsLimit t) {Z : C} (h : t.pt ⟶ Z) : CategoryStruct.comp (P.lift r) (CategoryStruct.comp (P.conePointUniqueUpToIso Q).hom h) = CategoryStruct.comp (Q.lift r) h

@[simp]

theorem CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_inv {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {r s t : Cone F} (P : IsLimit s) (Q : IsLimit t) : CategoryStruct.comp (Q.lift r) (P.conePointUniqueUpToIso Q).inv = P.lift r

@[simp]

theorem CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_inv_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {r s t : Cone F} (P : IsLimit s) (Q : IsLimit t) {Z : C} (h : s.pt ⟶ Z) : CategoryStruct.comp (Q.lift r) (CategoryStruct.comp (P.conePointUniqueUpToIso Q).inv h) = CategoryStruct.comp (P.lift r) h

def CategoryTheory.Limits.IsLimit.ofIsoLimit {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {r t : Cone F} (P : IsLimit r) (i : r ≅ t) : IsLimit t

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

Equations

• P.ofIsoLimit i = CategoryTheory.Limits.IsLimit.mkConeMorphism (fun (s : CategoryTheory.Limits.Cone F) => CategoryTheory.CategoryStruct.comp (P.liftConeMorphism s) i.hom) ⋯

@[simp]

theorem CategoryTheory.Limits.IsLimit.ofIsoLimit_lift {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {r t : Cone F} (P : IsLimit r) (i : r ≅ t) (s : Cone F) : (P.ofIsoLimit i).lift s = CategoryStruct.comp (P.lift s) i.hom.hom

def CategoryTheory.Limits.IsLimit.equivIsoLimit {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {r t : Cone F} (i : r ≅ t) : IsLimit r ≃ IsLimit 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.

@[simp]

theorem CategoryTheory.Limits.IsLimit.equivIsoLimit_apply {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {r t : Cone F} (i : r ≅ t) (P : IsLimit r) : (equivIsoLimit i) P = P.ofIsoLimit i

@[simp]

theorem CategoryTheory.Limits.IsLimit.equivIsoLimit_symm_apply {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {r t : Cone F} (i : r ≅ t) (P : IsLimit t) : (equivIsoLimit i).symm P = P.ofIsoLimit i.symm

def CategoryTheory.Limits.IsLimit.ofPointIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {r t : Cone F} (P : IsLimit r) [i : IsIso (P.lift t)] : IsLimit 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

• P.ofPointIso = P.ofIsoLimit (CategoryTheory.asIso (P.liftConeMorphism t)).symm

theorem CategoryTheory.Limits.IsLimit.hom_lift {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cone F} (h : IsLimit t) {W : C} (m : W ⟶ t.pt) : m = h.lift { pt := W, π := { app := fun (b : J) => CategoryStruct.comp m (t.π.app b), naturality := ⋯ } }

theorem CategoryTheory.Limits.IsLimit.hom_ext {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cone F} (h : IsLimit t) {W : C} {f f' : W ⟶ t.pt} (w : ∀ (j : J), CategoryStruct.comp f (t.π.app j) = 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₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {D : Type u₄} [Category.{v₄, u₄} D] {G : Functor K D} {left : Functor (Cone F) (Cone G)} {right : Functor (Cone G) (Cone F)} (adj : left ⊣ right) {c : Cone G} (t : IsLimit c) : IsLimit (right.obj 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.

def CategoryTheory.Limits.IsLimit.ofConeEquiv {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} {D : Type u₄} [Category.{v₄, u₄} D] {G : Functor K D} (h : Cone G ≌ Cone F) {c : Cone G} : IsLimit (h.functor.obj c) ≃ IsLimit 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.

@[simp]

theorem CategoryTheory.Limits.IsLimit.ofConeEquiv_apply_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} {D : Type u₄} [Category.{v₄, u₄} D] {G : Functor K D} (h : Cone G ≌ Cone F) {c : Cone G} (P : IsLimit (h.functor.obj c)) (s : Cone G) : ((ofConeEquiv h) P).lift s = CategoryStruct.comp (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₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {D : Type u₄} [Category.{v₄, u₄} D] {G : Functor K D} (h : Cone G ≌ Cone F) {c : Cone G} (P : IsLimit c) (s : Cone F) : ((ofConeEquiv h).symm P).lift s = 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₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} (α : F ≅ G) (c : Cone F) : IsLimit ((Cones.postcompose α.hom).obj c) ≃ IsLimit c

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

Equations

• CategoryTheory.Limits.IsLimit.postcomposeHomEquiv α c = CategoryTheory.Limits.IsLimit.ofConeEquiv (CategoryTheory.Limits.Cones.postcomposeEquivalence α)

def CategoryTheory.Limits.IsLimit.postcomposeInvEquiv {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} (α : F ≅ G) (c : Cone G) : IsLimit ((Cones.postcompose α.inv).obj c) ≃ IsLimit c

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

Equations

• CategoryTheory.Limits.IsLimit.postcomposeInvEquiv α c = CategoryTheory.Limits.IsLimit.postcomposeHomEquiv α.symm c

def CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} (α : F ≅ G) (c : Cone F) (d : Cone G) (w : (Cones.postcompose α.hom).obj c ≅ d) : IsLimit c ≃ IsLimit 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

• CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso α c d w = (CategoryTheory.Limits.IsLimit.postcomposeHomEquiv α c).symm.trans (CategoryTheory.Limits.IsLimit.equivIsoLimit w)

def CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {s : Cone F} {t : Cone G} (P : IsLimit s) (Q : IsLimit 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 := CategoryTheory.Limits.IsLimit.map s Q w.hom, inv := CategoryTheory.Limits.IsLimit.map t P w.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {s : Cone F} {t : Cone G} (P : IsLimit s) (Q : IsLimit t) (w : F ≅ G) : (P.conePointsIsoOfNatIso Q w).hom = map s Q w.hom

@[simp]

theorem CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_inv {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {s : Cone F} {t : Cone G} (P : IsLimit s) (Q : IsLimit t) (w : F ≅ G) : (P.conePointsIsoOfNatIso Q w).inv = map t P w.inv

theorem CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_hom_comp {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {s : Cone F} {t : Cone G} (P : IsLimit s) (Q : IsLimit t) (w : F ≅ G) (j : J) : CategoryStruct.comp (P.conePointsIsoOfNatIso Q w).hom (t.π.app j) = CategoryStruct.comp (s.π.app j) (w.hom.app j)

theorem CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_hom_comp_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {s : Cone F} {t : Cone G} (P : IsLimit s) (Q : IsLimit t) (w : F ≅ G) (j : J) {Z : C} (h : G.obj j ⟶ Z) : CategoryStruct.comp (P.conePointsIsoOfNatIso Q w).hom (CategoryStruct.comp (t.π.app j) h) = CategoryStruct.comp (s.π.app j) (CategoryStruct.comp (w.hom.app j) h)

theorem CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_inv_comp {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {s : Cone F} {t : Cone G} (P : IsLimit s) (Q : IsLimit t) (w : F ≅ G) (j : J) : CategoryStruct.comp (P.conePointsIsoOfNatIso Q w).inv (s.π.app j) = CategoryStruct.comp (t.π.app j) (w.inv.app j)

theorem CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_inv_comp_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {s : Cone F} {t : Cone G} (P : IsLimit s) (Q : IsLimit t) (w : F ≅ G) (j : J) {Z : C} (h : F.obj j ⟶ Z) : CategoryStruct.comp (P.conePointsIsoOfNatIso Q w).inv (CategoryStruct.comp (s.π.app j) h) = CategoryStruct.comp (t.π.app j) (CategoryStruct.comp (w.inv.app j) h)

theorem CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {r s : Cone F} {t : Cone G} (P : IsLimit s) (Q : IsLimit t) (w : F ≅ G) : CategoryStruct.comp (P.lift r) (P.conePointsIsoOfNatIso Q w).hom = map r Q w.hom

theorem CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_hom_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {r s : Cone F} {t : Cone G} (P : IsLimit s) (Q : IsLimit t) (w : F ≅ G) {Z : C} (h : t.pt ⟶ Z) : CategoryStruct.comp (P.lift r) (CategoryStruct.comp (P.conePointsIsoOfNatIso Q w).hom h) = CategoryStruct.comp (map r Q w.hom) h

theorem CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_inv {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {r s : Cone G} {t : Cone F} (P : IsLimit t) (Q : IsLimit s) (w : F ≅ G) : CategoryStruct.comp (Q.lift r) (P.conePointsIsoOfNatIso Q w).inv = map r P w.inv

theorem CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_inv_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {r s : Cone G} {t : Cone F} (P : IsLimit t) (Q : IsLimit s) (w : F ≅ G) {Z : C} (h : t.pt ⟶ Z) : CategoryStruct.comp (Q.lift r) (CategoryStruct.comp (P.conePointsIsoOfNatIso Q w).inv h) = CategoryStruct.comp (map r P w.inv) h

def CategoryTheory.Limits.IsLimit.whiskerEquivalence {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} {s : Cone F} (P : IsLimit s) (e : K ≌ J) : IsLimit (Cone.whisker e.functor s)

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

Equations

• P.whiskerEquivalence e = CategoryTheory.Limits.IsLimit.ofRightAdjoint (CategoryTheory.Limits.Cones.whiskeringEquivalence e).symm.toAdjunction P

def CategoryTheory.Limits.IsLimit.ofWhiskerEquivalence {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} {s : Cone F} (e : K ≌ J) (P : IsLimit (Cone.whisker e.functor s)) : IsLimit s

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.

def CategoryTheory.Limits.IsLimit.whiskerEquivalenceEquiv {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} {s : Cone F} (e : K ≌ J) : IsLimit s ≃ IsLimit (Cone.whisker e.functor s)

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.

def CategoryTheory.Limits.IsLimit.extendIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s : Cone F} {X : C} (i : X ⟶ s.pt) [IsIso i] (hs : IsLimit s) : IsLimit (s.extend i)

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

Equations

• CategoryTheory.Limits.IsLimit.extendIso i hs = hs.ofIsoLimit (CategoryTheory.Limits.Cones.extendIso s (CategoryTheory.asIso i)).symm

def CategoryTheory.Limits.IsLimit.ofExtendIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s : Cone F} {X : C} (i : X ⟶ s.pt) [IsIso i] (hs : IsLimit (s.extend i)) : IsLimit s

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

Equations

• CategoryTheory.Limits.IsLimit.ofExtendIso i hs = hs.ofIsoLimit (CategoryTheory.Limits.Cones.extendIso s (CategoryTheory.asIso i))

def CategoryTheory.Limits.IsLimit.extendIsoEquiv {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s : Cone F} {X : C} (i : X ⟶ s.pt) [IsIso i] : IsLimit s ≃ IsLimit (s.extend i)

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

Equations

• CategoryTheory.Limits.IsLimit.extendIsoEquiv i = equivOfSubsingletonOfSubsingleton (CategoryTheory.Limits.IsLimit.extendIso i) (CategoryTheory.Limits.IsLimit.ofExtendIso i)

def CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence {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} {s : Cone F} {G : Functor K C} {t : Cone G} (P : IsLimit s) (Q : IsLimit 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.

@[simp]

theorem CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence_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} {s : Cone F} {G : Functor K C} {t : Cone G} (P : IsLimit s) (Q : IsLimit t) (e : J ≌ K) (w : e.functor.comp G ≅ F) : (P.conePointsIsoOfEquivalence Q e w).hom = Q.lift ((Cones.equivalenceOfReindexing e.symm ((isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G)).functor.obj s)

@[simp]

theorem CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence_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} {s : Cone F} {G : Functor K C} {t : Cone G} (P : IsLimit s) (Q : IsLimit t) (e : J ≌ K) (w : e.functor.comp G ≅ F) : (P.conePointsIsoOfEquivalence Q e w).inv = P.lift ((Cones.equivalenceOfReindexing e w).functor.obj t)

def CategoryTheory.Limits.IsLimit.homIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cone F} (h : IsLimit t) (W : C) : ULift.{u₁, v₃} (W ⟶ t.pt) ≅ (Functor.const J).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.

@[simp]

theorem CategoryTheory.Limits.IsLimit.homIso_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cone F} (h : IsLimit 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₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cone F} (h : IsLimit t) : (yoneda.obj t.pt).comp 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

• h.natIso = CategoryTheory.NatIso.ofComponents (fun (W : Cᵒᵖ) => h.homIso (Opposite.unop W)) ⋯

def CategoryTheory.Limits.IsLimit.homIso' {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cone F} (h : IsLimit t) (W : C) : ULift.{u₁, v₃} (W ⟶ t.pt) ≅ { p : (j : J) → W ⟶ F.obj j // ∀ {j j' : J} (f : j ⟶ j'), 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.

def CategoryTheory.Limits.IsLimit.ofFaithful {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cone F} {D : Type u₄} [Category.{v₄, u₄} D] (G : Functor C D) [G.Faithful] (ht : IsLimit (G.mapCone t)) (lift : (s : Cone F) → s.pt ⟶ t.pt) (h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)) : IsLimit t

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

• CategoryTheory.Limits.IsLimit.ofFaithful G ht lift h = { lift := lift, fac := ⋯, uniq := ⋯ }

def CategoryTheory.Limits.IsLimit.mapConeEquiv {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] {K : Functor J C} {F G : Functor C D} (h : F ≅ G) {c : Cone K} (t : IsLimit (F.mapCone c)) : IsLimit (G.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.

def CategoryTheory.Limits.IsLimit.isoUniqueConeMorphism {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cone F} : IsLimit t ≅ (s : Cone F) → 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.

def CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {X : C} (h : (yoneda.obj X).comp uliftFunctor.{u₁, v₃} ≅ F.cones) {Y : C} (f : Y ⟶ X) : Cone F

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

Equations

• CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom h f = { pt := Y, π := h.hom.app (Opposite.op Y) { down := f } }

def CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {X : C} (h : (yoneda.obj X).comp uliftFunctor.{u₁, v₃} ≅ F.cones) (s : Cone F) : s.pt ⟶ X

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

Equations

• CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone h s = (h.inv.app (Opposite.op s.pt) s.π).down

@[simp]

theorem CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom_homOfCone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {X : C} (h : (yoneda.obj X).comp uliftFunctor.{u₁, v₃} ≅ F.cones) (s : Cone F) : coneOfHom h (homOfCone h s) = s

@[simp]

theorem CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone_coneOfHom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {X : C} (h : (yoneda.obj X).comp uliftFunctor.{u₁, v₃} ≅ F.cones) {Y : C} (f : Y ⟶ X) : homOfCone h (coneOfHom h f) = f

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

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

Equations

• CategoryTheory.Limits.IsLimit.OfNatIso.limitCone h = CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom h (CategoryTheory.CategoryStruct.id X)

theorem CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom_fac {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {X : C} (h : (yoneda.obj X).comp uliftFunctor.{u₁, v₃} ≅ F.cones) {Y : C} (f : Y ⟶ X) : coneOfHom h f = (limitCone h).extend f

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₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {X : C} (h : (yoneda.obj X).comp uliftFunctor.{u₁, v₃} ≅ F.cones) (s : Cone F) : (limitCone h).extend (homOfCone h s) = 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₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {X : C} (h : (yoneda.obj X).comp uliftFunctor.{u₁, v₃} ≅ F.cones) : IsLimit (OfNatIso.limitCone h)

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

Equations

• CategoryTheory.Limits.IsLimit.ofNatIso h = { lift := fun (s : CategoryTheory.Limits.Cone F) => CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone h s, fac := ⋯, uniq := ⋯ }

structure CategoryTheory.Limits.IsColimit {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} (t : Cocone F) : 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.

See https://stacks.math.columbia.edu/tag/002F.

• desc (s : Cocone F) : t.pt ⟶ s.pt

  t.pt maps to all other cocone covertices

• fac (s : Cocone F) (j : J) : CategoryStruct.comp (t.ι.app j) (self.desc s) = s.ι.app j

  The map desc makes the diagram with the natural transformations commute

• uniq (s : Cocone F) (m : t.pt ⟶ s.pt) : (∀ (j : J), 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₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cocone F} (self : IsColimit t) (s : Cocone F) (j : J) {Z : C} (h : s.pt ⟶ Z) : CategoryStruct.comp (t.ι.app j) (CategoryStruct.comp (self.desc s) h) = CategoryStruct.comp (s.ι.app j) h

instance CategoryTheory.Limits.IsColimit.subsingleton {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cocone F} : Subsingleton (IsColimit t)

def CategoryTheory.Limits.IsColimit.map {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {s : Cocone F} (P : IsColimit s) (t : Cocone G) (α : 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 ((CategoryTheory.Limits.Cocones.precompose α).obj t)

@[simp]

theorem CategoryTheory.Limits.IsColimit.ι_map {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {c : Cocone F} (hc : IsColimit c) (d : Cocone G) (α : F ⟶ G) (j : J) : CategoryStruct.comp (c.ι.app j) (hc.map d α) = CategoryStruct.comp (α.app j) (d.ι.app j)

@[simp]

theorem CategoryTheory.Limits.IsColimit.ι_map_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {c : Cocone F} (hc : IsColimit c) (d : Cocone G) (α : F ⟶ G) (j : J) {Z : C} (h : d.pt ⟶ Z) : CategoryStruct.comp (c.ι.app j) (CategoryStruct.comp (hc.map d α) h) = CategoryStruct.comp (α.app j) (CategoryStruct.comp (d.ι.app j) h)

@[simp]

theorem CategoryTheory.Limits.IsColimit.desc_self {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cocone F} (h : IsColimit t) : h.desc t = CategoryStruct.id t.pt

def CategoryTheory.Limits.IsColimit.descCoconeMorphism {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cocone F} (h : IsColimit t) (s : Cocone F) : t ⟶ s

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

Equations

• h.descCoconeMorphism s = { hom := h.desc s, w := ⋯ }

@[simp]

theorem CategoryTheory.Limits.IsColimit.descCoconeMorphism_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cocone F} (h : IsColimit t) (s : Cocone F) : (h.descCoconeMorphism s).hom = h.desc s

theorem CategoryTheory.Limits.IsColimit.uniq_cocone_morphism {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s t : Cocone F} (h : IsColimit t) {f f' : t ⟶ s} : f = f'

theorem CategoryTheory.Limits.IsColimit.existsUnique {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cocone F} (h : IsColimit t) (s : Cocone F) : ∃! d : t.pt ⟶ s.pt, ∀ (j : J), 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₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cocone F} (ht : ∀ (s : Cocone F), ∃! d : t.pt ⟶ s.pt, ∀ (j : J), CategoryStruct.comp (t.ι.app j) d = s.ι.app j) : IsColimit t

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.IsColimit.mkCoconeMorphism {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cocone F} (desc : (s : Cocone F) → t ⟶ s) (uniq' : ∀ (s : Cocone F) (m : t ⟶ s), m = desc s) : IsColimit t

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

Equations

• CategoryTheory.Limits.IsColimit.mkCoconeMorphism desc uniq' = { desc := fun (s : CategoryTheory.Limits.Cocone F) => (desc s).hom, fac := ⋯, uniq := ⋯ }

@[simp]

theorem CategoryTheory.Limits.IsColimit.mkCoconeMorphism_desc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cocone F} (desc : (s : Cocone F) → t ⟶ s) (uniq' : ∀ (s : Cocone F) (m : t ⟶ s), m = desc s) (s : Cocone F) : (mkCoconeMorphism desc uniq').desc s = (desc s).hom

def CategoryTheory.Limits.IsColimit.uniqueUpToIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s t : Cocone F} (P : IsColimit s) (Q : IsColimit 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 := ⋯ }

@[simp]

theorem CategoryTheory.Limits.IsColimit.uniqueUpToIso_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) : (P.uniqueUpToIso Q).hom = P.descCoconeMorphism t

@[simp]

theorem CategoryTheory.Limits.IsColimit.uniqueUpToIso_inv {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) : (P.uniqueUpToIso Q).inv = Q.descCoconeMorphism s

theorem CategoryTheory.Limits.IsColimit.hom_isIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) (f : s ⟶ t) : IsIso f

Any cocone morphism between colimit cocones is an isomorphism.

def CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) : s.pt ≅ t.pt

Colimits of F are unique up to isomorphism.

Equations

• P.coconePointUniqueUpToIso Q = (CategoryTheory.Limits.Cocones.forget F).mapIso (P.uniqueUpToIso Q)

@[simp]

theorem CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) (j : J) : CategoryStruct.comp (s.ι.app j) (P.coconePointUniqueUpToIso Q).hom = t.ι.app j

@[simp]

theorem CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) (j : J) {Z : C} (h : t.pt ⟶ Z) : CategoryStruct.comp (s.ι.app j) (CategoryStruct.comp (P.coconePointUniqueUpToIso Q).hom h) = CategoryStruct.comp (t.ι.app j) h

@[simp]

theorem CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) (j : J) : CategoryStruct.comp (t.ι.app j) (P.coconePointUniqueUpToIso Q).inv = s.ι.app j

@[simp]

theorem CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) (j : J) {Z : C} (h : s.pt ⟶ Z) : CategoryStruct.comp (t.ι.app j) (CategoryStruct.comp (P.coconePointUniqueUpToIso Q).inv h) = CategoryStruct.comp (s.ι.app j) h

@[simp]

theorem CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_hom_desc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {r s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) : CategoryStruct.comp (P.coconePointUniqueUpToIso Q).hom (Q.desc r) = P.desc r

@[simp]

theorem CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_hom_desc_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {r s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) {Z : C} (h : r.pt ⟶ Z) : CategoryStruct.comp (P.coconePointUniqueUpToIso Q).hom (CategoryStruct.comp (Q.desc r) h) = CategoryStruct.comp (P.desc r) h

@[simp]

theorem CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_inv_desc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {r s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) : CategoryStruct.comp (P.coconePointUniqueUpToIso Q).inv (P.desc r) = Q.desc r

@[simp]

theorem CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_inv_desc_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {r s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) {Z : C} (h : r.pt ⟶ Z) : CategoryStruct.comp (P.coconePointUniqueUpToIso Q).inv (CategoryStruct.comp (P.desc r) h) = CategoryStruct.comp (Q.desc r) h

def CategoryTheory.Limits.IsColimit.ofIsoColimit {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {r t : Cocone F} (P : IsColimit r) (i : r ≅ t) : IsColimit t

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

Equations

• P.ofIsoColimit i = CategoryTheory.Limits.IsColimit.mkCoconeMorphism (fun (s : CategoryTheory.Limits.Cocone F) => CategoryTheory.CategoryStruct.comp i.inv (P.descCoconeMorphism s)) ⋯

@[simp]

theorem CategoryTheory.Limits.IsColimit.ofIsoColimit_desc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {r t : Cocone F} (P : IsColimit r) (i : r ≅ t) (s : Cocone F) : (P.ofIsoColimit i).desc s = CategoryStruct.comp i.inv.hom (P.desc s)

def CategoryTheory.Limits.IsColimit.equivIsoColimit {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {r t : Cocone F} (i : r ≅ t) : IsColimit r ≃ IsColimit 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.

@[simp]

theorem CategoryTheory.Limits.IsColimit.equivIsoColimit_apply {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {r t : Cocone F} (i : r ≅ t) (P : IsColimit r) : (equivIsoColimit i) P = P.ofIsoColimit i

@[simp]

theorem CategoryTheory.Limits.IsColimit.equivIsoColimit_symm_apply {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {r t : Cocone F} (i : r ≅ t) (P : IsColimit t) : (equivIsoColimit i).symm P = P.ofIsoColimit i.symm

def CategoryTheory.Limits.IsColimit.ofPointIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {r t : Cocone F} (P : IsColimit r) [i : IsIso (P.desc t)] : IsColimit 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

• P.ofPointIso = P.ofIsoColimit (CategoryTheory.asIso (P.descCoconeMorphism t))

theorem CategoryTheory.Limits.IsColimit.hom_desc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cocone F} (h : IsColimit t) {W : C} (m : t.pt ⟶ W) : m = h.desc { pt := W, ι := { app := fun (b : J) => CategoryStruct.comp (t.ι.app b) m, naturality := ⋯ } }

theorem CategoryTheory.Limits.IsColimit.hom_ext {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cocone F} (h : IsColimit t) {W : C} {f f' : t.pt ⟶ W} (w : ∀ (j : J), CategoryStruct.comp (t.ι.app j) f = 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₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {D : Type u₄} [Category.{v₄, u₄} D] {G : Functor K D} {left : Functor (Cocone G) (Cocone F)} {right : Functor (Cocone F) (Cocone G)} (adj : left ⊣ right) {c : Cocone G} (t : IsColimit c) : IsColimit (left.obj 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.

def CategoryTheory.Limits.IsColimit.ofCoconeEquiv {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} {D : Type u₄} [Category.{v₄, u₄} D] {G : Functor K D} (h : Cocone G ≌ Cocone F) {c : Cocone G} : IsColimit (h.functor.obj c) ≃ IsColimit 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.

@[simp]

theorem CategoryTheory.Limits.IsColimit.ofCoconeEquiv_apply_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} {D : Type u₄} [Category.{v₄, u₄} D] {G : Functor K D} (h : Cocone G ≌ Cocone F) {c : Cocone G} (P : IsColimit (h.functor.obj c)) (s : Cocone G) : ((ofCoconeEquiv h) P).desc s = CategoryStruct.comp (h.unit.app c).hom (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₁} [Category.{v₁, u₁} J] {K : Type u₂} [Category.{v₂, u₂} K] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {D : Type u₄} [Category.{v₄, u₄} D] {G : Functor K D} (h : Cocone G ≌ Cocone F) {c : Cocone G} (P : IsColimit c) (s : Cocone F) : ((ofCoconeEquiv h).symm P).desc s = 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₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} (α : F ≅ G) (c : Cocone G) : IsColimit ((Cocones.precompose α.hom).obj c) ≃ IsColimit c

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

Equations

• CategoryTheory.Limits.IsColimit.precomposeHomEquiv α c = CategoryTheory.Limits.IsColimit.ofCoconeEquiv (CategoryTheory.Limits.Cocones.precomposeEquivalence α)

def CategoryTheory.Limits.IsColimit.precomposeInvEquiv {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} (α : F ≅ G) (c : Cocone F) : IsColimit ((Cocones.precompose α.inv).obj c) ≃ IsColimit c

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

Equations

• CategoryTheory.Limits.IsColimit.precomposeInvEquiv α c = CategoryTheory.Limits.IsColimit.precomposeHomEquiv α.symm c

def CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} (α : F ≅ G) (c : Cocone F) (d : Cocone G) (w : (Cocones.precompose α.inv).obj c ≅ d) : IsColimit c ≃ IsColimit 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

• CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso α c d w = (CategoryTheory.Limits.IsColimit.precomposeInvEquiv α c).symm.trans (CategoryTheory.Limits.IsColimit.equivIsoColimit w)

def CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {s : Cocone F} {t : Cocone G} (P : IsColimit s) (Q : IsColimit 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 := ⋯ }

@[simp]

theorem CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {s : Cocone F} {t : Cocone G} (P : IsColimit s) (Q : IsColimit t) (w : F ≅ G) : (P.coconePointsIsoOfNatIso Q w).hom = P.map t w.hom

@[simp]

theorem CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_inv {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {s : Cocone F} {t : Cocone G} (P : IsColimit s) (Q : IsColimit t) (w : F ≅ G) : (P.coconePointsIsoOfNatIso Q w).inv = Q.map s w.inv

theorem CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {s : Cocone F} {t : Cocone G} (P : IsColimit s) (Q : IsColimit t) (w : F ≅ G) (j : J) : CategoryStruct.comp (s.ι.app j) (P.coconePointsIsoOfNatIso Q w).hom = CategoryStruct.comp (w.hom.app j) (t.ι.app j)

theorem CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_hom_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {s : Cocone F} {t : Cocone G} (P : IsColimit s) (Q : IsColimit t) (w : F ≅ G) (j : J) {Z : C} (h : t.pt ⟶ Z) : CategoryStruct.comp (s.ι.app j) (CategoryStruct.comp (P.coconePointsIsoOfNatIso Q w).hom h) = CategoryStruct.comp (w.hom.app j) (CategoryStruct.comp (t.ι.app j) h)

theorem CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_inv {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {s : Cocone F} {t : Cocone G} (P : IsColimit s) (Q : IsColimit t) (w : F ≅ G) (j : J) : CategoryStruct.comp (t.ι.app j) (P.coconePointsIsoOfNatIso Q w).inv = CategoryStruct.comp (w.inv.app j) (s.ι.app j)

theorem CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_inv_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {s : Cocone F} {t : Cocone G} (P : IsColimit s) (Q : IsColimit t) (w : F ≅ G) (j : J) {Z : C} (h : s.pt ⟶ Z) : CategoryStruct.comp (t.ι.app j) (CategoryStruct.comp (P.coconePointsIsoOfNatIso Q w).inv h) = CategoryStruct.comp (w.inv.app j) (CategoryStruct.comp (s.ι.app j) h)

theorem CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_hom_desc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {s : Cocone F} {r t : Cocone G} (P : IsColimit s) (Q : IsColimit t) (w : F ≅ G) : CategoryStruct.comp (P.coconePointsIsoOfNatIso Q w).hom (Q.desc r) = P.map r w.hom

theorem CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_hom_desc_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {s : Cocone F} {r t : Cocone G} (P : IsColimit s) (Q : IsColimit t) (w : F ≅ G) {Z : C} (h : r.pt ⟶ Z) : CategoryStruct.comp (P.coconePointsIsoOfNatIso Q w).hom (CategoryStruct.comp (Q.desc r) h) = CategoryStruct.comp (P.map r w.hom) h

theorem CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_inv_desc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {s : Cocone G} {r t : Cocone F} (P : IsColimit t) (Q : IsColimit s) (w : F ≅ G) : CategoryStruct.comp (P.coconePointsIsoOfNatIso Q w).inv (P.desc r) = Q.map r w.inv

theorem CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_inv_desc_assoc {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F G : Functor J C} {s : Cocone G} {r t : Cocone F} (P : IsColimit t) (Q : IsColimit s) (w : F ≅ G) {Z : C} (h : r.pt ⟶ Z) : CategoryStruct.comp (P.coconePointsIsoOfNatIso Q w).inv (CategoryStruct.comp (P.desc r) h) = CategoryStruct.comp (Q.map r w.inv) h

def CategoryTheory.Limits.IsColimit.whiskerEquivalence {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} {s : Cocone F} (P : IsColimit s) (e : K ≌ J) : IsColimit (Cocone.whisker e.functor s)

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

Equations

• P.whiskerEquivalence e = CategoryTheory.Limits.IsColimit.ofLeftAdjoint (CategoryTheory.Limits.Cocones.whiskeringEquivalence e).toAdjunction P

def CategoryTheory.Limits.IsColimit.ofWhiskerEquivalence {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} {s : Cocone F} (e : K ≌ J) (P : IsColimit (Cocone.whisker e.functor s)) : IsColimit s

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.

def CategoryTheory.Limits.IsColimit.whiskerEquivalenceEquiv {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} {s : Cocone F} (e : K ≌ J) : IsColimit s ≃ IsColimit (Cocone.whisker e.functor s)

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.

def CategoryTheory.Limits.IsColimit.extendIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s : Cocone F} {X : C} (i : s.pt ⟶ X) [IsIso i] (hs : IsColimit s) : IsColimit (s.extend i)

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

Equations

• CategoryTheory.Limits.IsColimit.extendIso i hs = hs.ofIsoColimit (CategoryTheory.Limits.Cocones.extendIso s (CategoryTheory.asIso i))

def CategoryTheory.Limits.IsColimit.ofExtendIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s : Cocone F} {X : C} (i : s.pt ⟶ X) [IsIso i] (hs : IsColimit (s.extend i)) : IsColimit s

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

Equations

• CategoryTheory.Limits.IsColimit.ofExtendIso i hs = hs.ofIsoColimit (CategoryTheory.Limits.Cocones.extendIso s (CategoryTheory.asIso i)).symm

def CategoryTheory.Limits.IsColimit.extendIsoEquiv {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {s : Cocone F} {X : C} (i : s.pt ⟶ X) [IsIso i] : IsColimit s ≃ IsColimit (s.extend i)

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

Equations

• CategoryTheory.Limits.IsColimit.extendIsoEquiv i = equivOfSubsingletonOfSubsingleton (CategoryTheory.Limits.IsColimit.extendIso i) (CategoryTheory.Limits.IsColimit.ofExtendIso i)

def CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence {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} {s : Cocone F} {G : Functor K C} {t : Cocone G} (P : IsColimit s) (Q : IsColimit 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.

@[simp]

theorem CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence_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} {s : Cocone F} {G : Functor K C} {t : Cocone G} (P : IsColimit s) (Q : IsColimit t) (e : J ≌ K) (w : e.functor.comp G ≅ F) : (P.coconePointsIsoOfEquivalence Q e w).inv = Q.desc ((Cocones.equivalenceOfReindexing e.symm ((isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G)).functor.obj s)

@[simp]

theorem CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence_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} {s : Cocone F} {G : Functor K C} {t : Cocone G} (P : IsColimit s) (Q : IsColimit t) (e : J ≌ K) (w : e.functor.comp G ≅ F) : (P.coconePointsIsoOfEquivalence Q e w).hom = P.desc ((Cocones.equivalenceOfReindexing e w).functor.obj t)

def CategoryTheory.Limits.IsColimit.homEquiv {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cocone F} (h : IsColimit t) (W : C) : (t.pt ⟶ W) ≃ (F ⟶ (Functor.const J).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 ⟶ (CategoryTheory.Functor.const J).obj W) => h.desc { pt := W, ι := ι }, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CategoryTheory.Limits.IsColimit.homEquiv_apply {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cocone F} (h : IsColimit t) {W : C} (f : t.pt ⟶ W) : (h.homEquiv W) f = (t.extend f).ι

def CategoryTheory.Limits.IsColimit.homIso {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cocone F} (h : IsColimit t) (W : C) : ULift.{u₁, v₃} (t.pt ⟶ W) ≅ F ⟶ (Functor.const J).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

@[simp]

theorem CategoryTheory.Limits.IsColimit.homIso_hom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cocone F} (h : IsColimit 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₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cocone F} (h : IsColimit t) : (coyoneda.obj (Opposite.op t.pt)).comp 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

• h.natIso = CategoryTheory.NatIso.ofComponents h.homIso ⋯

def CategoryTheory.Limits.IsColimit.homIso' {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cocone F} (h : IsColimit t) (W : C) : ULift.{u₁, v₃} (t.pt ⟶ W) ≅ { p : (j : J) → F.obj j ⟶ W // ∀ {j j' : J} (f : j ⟶ j'), 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.

def CategoryTheory.Limits.IsColimit.ofFaithful {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cocone F} {D : Type u₄} [Category.{v₄, u₄} D] (G : Functor C D) [G.Faithful] (ht : IsColimit (G.mapCocone t)) (desc : (s : Cocone F) → t.pt ⟶ s.pt) (h : ∀ (s : Cocone F), G.map (desc s) = ht.desc (G.mapCocone s)) : IsColimit t

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

• CategoryTheory.Limits.IsColimit.ofFaithful G ht desc h = { desc := desc, fac := ⋯, uniq := ⋯ }

def CategoryTheory.Limits.IsColimit.mapCoconeEquiv {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {D : Type u₄} [Category.{v₄, u₄} D] {K : Functor J C} {F G : Functor C D} (h : F ≅ G) {c : Cocone K} (t : IsColimit (F.mapCocone c)) : IsColimit (G.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.

def CategoryTheory.Limits.IsColimit.isoUniqueCoconeMorphism {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {t : Cocone F} : IsColimit t ≅ (s : Cocone F) → 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.

def CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {X : C} (h : (coyoneda.obj (Opposite.op X)).comp uliftFunctor.{u₁, v₃} ≅ F.cocones) {Y : C} (f : X ⟶ Y) : Cocone F

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

Equations

• CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom h f = { pt := Y, ι := h.hom.app Y { down := f } }

def CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {X : C} (h : (coyoneda.obj (Opposite.op X)).comp uliftFunctor.{u₁, v₃} ≅ F.cocones) (s : Cocone F) : X ⟶ s.pt

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

Equations

• CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone h s = (h.inv.app s.pt s.ι).down

@[simp]

theorem CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom_homOfCocone {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {X : C} (h : (coyoneda.obj (Opposite.op X)).comp uliftFunctor.{u₁, v₃} ≅ F.cocones) (s : Cocone F) : coconeOfHom h (homOfCocone h s) = s

@[simp]

theorem CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone_cooneOfHom {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {X : C} (h : (coyoneda.obj (Opposite.op X)).comp uliftFunctor.{u₁, v₃} ≅ F.cocones) {Y : C} (f : X ⟶ Y) : homOfCocone h (coconeOfHom h f) = f

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

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

Equations

• CategoryTheory.Limits.IsColimit.OfNatIso.colimitCocone h = CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom h (CategoryTheory.CategoryStruct.id X)

theorem CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom_fac {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {X : C} (h : (coyoneda.obj (Opposite.op X)).comp uliftFunctor.{u₁, v₃} ≅ F.cocones) {Y : C} (f : X ⟶ Y) : coconeOfHom h f = (colimitCocone h).extend f

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₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {X : C} (h : (coyoneda.obj (Opposite.op X)).comp uliftFunctor.{u₁, v₃} ≅ F.cocones) (s : Cocone F) : (colimitCocone h).extend (homOfCocone h s) = 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₁} [Category.{v₁, u₁} J] {C : Type u₃} [Category.{v₃, u₃} C] {F : Functor J C} {X : C} (h : (coyoneda.obj (Opposite.op X)).comp uliftFunctor.{u₁, v₃} ≅ F.cocones) : IsColimit (OfNatIso.colimitCocone h)

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

Equations

• CategoryTheory.Limits.IsColimit.ofNatIso h = { desc := fun (s : CategoryTheory.Limits.Cocone F) => CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone h s, fac := ⋯, uniq := ⋯ }