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, forc : Cone F,F : J ⥤ C, expressing thatcis a limit cone,
See also CategoryTheory.Limits.HasLimits which further builds:
LimitCone F, which consists of a choice of cone forFand the fact it is a limit cone, andHasLimit F, asserting the mere existence of some limit cone forF.
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₁}
[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.
@[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)
:
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)
:
@[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)
:
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)
:
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)
:
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}
:
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)
:
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)
:
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)
:
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_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)
:
@[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)
:
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)
:
Limits of F are unique up to isomorphism.
Equations
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
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)
:
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)
:
@[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)
:
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)
:
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))
:
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)
:
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}
:
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)
:
A cone postcomposed with a natural isomorphism is a limit cone if and only if the original cone is.
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)
:
A cone postcomposed with the inverse of a natural isomorphism is a limit cone if and only if the original cone is.
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)
:
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.
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)
:
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_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)
:
@[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)
:
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)
:
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)
:
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.
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)
:
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)
:
A limit cone extended by an isomorphism is a limit cone.
Equations
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
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]
:
A cone is a limit cone iff its extension by an isomorphism is.
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)
:
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.homEquiv
{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}
:
The universal property of a limit cone: a wap W ⟶ t.pt is the same as
a cone on F with cone point W.
@[simp]
theorem
CategoryTheory.Limits.IsLimit.homEquiv_apply
{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 : W ⟶ t.pt)
:
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)
:
The universal property of a limit cone: a map W ⟶ X is the same as
a cone on F with cone point W.
@[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))
:
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)
:
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)
:
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))
:
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}
:
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 : F.cones.RepresentableBy X)
{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.homEquiv 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 : F.cones.RepresentableBy X)
(s : Cone F)
:
If F.cones is represented by X, each cone s gives a morphism s.pt ⟶ X.
Equations
@[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 : F.cones.RepresentableBy X)
(s : Cone F)
:
@[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 : F.cones.RepresentableBy X)
{Y : C}
(f : Y ⟶ X)
:
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 : F.cones.RepresentableBy X)
:
Cone F
If F.cones is represented by X, the cone corresponding to the identity morphism on X
will be a limit cone.
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 : F.cones.RepresentableBy X)
{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₁}
[Category.{v₁, u₁} J]
{C : Type u₃}
[Category.{v₃, u₃} C]
{F : Functor J C}
{X : C}
(h : F.cones.RepresentableBy X)
(s : Cone F)
:
If F.cones is represented by X, any cone is the extension of the limit cone by the
corresponding morphism.
def
CategoryTheory.Limits.IsLimit.ofRepresentableBy
{J : Type u₁}
[Category.{v₁, u₁} J]
{C : Type u₃}
[Category.{v₃, u₃} C]
{F : Functor J C}
{X : C}
(h : F.cones.RepresentableBy X)
:
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.ofRepresentableBy h = { lift := fun (s : CategoryTheory.Limits.Cone F) => CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone h s, fac := ⋯, uniq := ⋯ }
@[deprecated CategoryTheory.Limits.IsLimit.ofRepresentableBy (since := "2025-05-09")]
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 : F.cones.RepresentableBy X)
:
Alias of CategoryTheory.Limits.IsLimit.ofRepresentableBy.
If F.cones is representable, then the cone corresponding to the identity morphism on
the representing object is a limit cone.
def
CategoryTheory.Limits.IsLimit.representableBy
{J : Type u₁}
[Category.{v₁, u₁} J]
{C : Type u₃}
[Category.{v₃, u₃} C]
{F : Functor J C}
{t : Cone F}
(hc : IsLimit t)
:
F.cones.RepresentableBy t.pt
Given a limit cone, F.cones is representable by the point of the cone.
Equations
- hc.representableBy = { homEquiv := fun {X : C} => hc.homEquiv, homEquiv_comp := ⋯ }
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.
@[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}
:
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)
:
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)
:
@[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)
:
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)
:
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)
:
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}
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
@[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)
:
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)
:
Colimits of F are unique up to isomorphism.
Equations
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
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)
:
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)
:
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)
:
@[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)
:
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)]
:
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)
:
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')
:
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)
:
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}
:
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)
:
A cocone precomposed with a natural isomorphism is a colimit cocone if and only if the original cocone is.
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)
:
A cocone precomposed with the inverse of a natural isomorphism is a colimit cocone if and only if the original cocone is.
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)
:
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.
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)
:
The cocone points of two colimit cocones for naturally isomorphic functors are themselves isomorphic.
@[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)
:
@[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)
:
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)
:
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)
:
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.
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))
:
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)
:
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)
:
A colimit cocone extended by an isomorphism is a colimit cocone.
Equations
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))
:
A cocone is a colimit cocone if its extension by an isomorphism is.
Equations
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]
:
A cocone is a colimit cocone iff its extension by an isomorphism is.
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)
:
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_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)
@[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)
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}
:
The universal property of a colimit cocone: a map X ⟶ W is the same as
a cocone on F with cone point W.
@[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)
:
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)
:
The universal property of a colimit cocone: a map X ⟶ W is the same as
a cocone on F with cone point W.
@[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))
:
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)
:
The colimit of F represents the functor taking W to
the set of cocones on F with cone point W.
Equations
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)
:
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))
:
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))
:
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}
:
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 : F.cocones.CorepresentableBy X)
{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.homEquiv 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 : F.cocones.CorepresentableBy X)
(s : Cocone F)
:
If F.cocones is corepresented by X, each cocone s gives a morphism X ⟶ s.pt.
Equations
@[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 : F.cocones.CorepresentableBy X)
(s : Cocone F)
:
@[simp]
theorem
CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone_coconeOfHom
{J : Type u₁}
[Category.{v₁, u₁} J]
{C : Type u₃}
[Category.{v₃, u₃} C]
{F : Functor J C}
{X : C}
(h : F.cocones.CorepresentableBy X)
{Y : C}
(f : X ⟶ Y)
:
@[deprecated CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone_coconeOfHom (since := "2025-05-13")]
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 : F.cocones.CorepresentableBy X)
{Y : C}
(f : X ⟶ Y)
:
Alias of CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone_coconeOfHom.
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 : F.cocones.CorepresentableBy X)
:
Cocone F
If F.cocones is corepresented by X, the cocone corresponding to the identity morphism on X
will be a colimit cocone.
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 : F.cocones.CorepresentableBy X)
{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₁}
[Category.{v₁, u₁} J]
{C : Type u₃}
[Category.{v₃, u₃} C]
{F : Functor J C}
{X : C}
(h : F.cocones.CorepresentableBy X)
(s : Cocone F)
:
If F.cocones is corepresented by X, any cocone is the extension of the colimit cocone by the
corresponding morphism.
def
CategoryTheory.Limits.IsColimit.ofCorepresentableBy
{J : Type u₁}
[Category.{v₁, u₁} J]
{C : Type u₃}
[Category.{v₃, u₃} C]
{F : Functor J C}
{X : C}
(h : F.cocones.CorepresentableBy X)
:
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.ofCorepresentableBy h = { desc := fun (s : CategoryTheory.Limits.Cocone F) => CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone h s, fac := ⋯, uniq := ⋯ }
@[deprecated CategoryTheory.Limits.IsColimit.ofCorepresentableBy (since := "2025-05-09")]
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 : F.cocones.CorepresentableBy X)
:
Alias of CategoryTheory.Limits.IsColimit.ofCorepresentableBy.
If F.cocones is corepresentable, then the cocone corresponding to the identity morphism on
the representing object is a colimit cocone.
def
CategoryTheory.Limits.IsColimit.corepresentableBy
{J : Type u₁}
[Category.{v₁, u₁} J]
{C : Type u₃}
[Category.{v₃, u₃} C]
{F : Functor J C}
{t : Cocone F}
(hc : IsColimit t)
:
Given a colimit cocone, F.cocones is corepresentable by the point of the cocone.
Equations
- hc.corepresentableBy = { homEquiv := fun {Y : C} => hc.homEquiv, homEquiv_comp := ⋯ }