@[nolint]
structure
category_theory.limits.is_limit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C} :
category_theory.limits.cone F → Type (max u v)
- lift : Π (s : category_theory.limits.cone F), s.X ⟶ t.X
- fac' : (∀ (s : category_theory.limits.cone F) (j : J), c.lift s ≫ t.π.app j = s.π.app j) . "obviously"
- uniq' : (∀ (s : category_theory.limits.cone F) (m : s.X ⟶ t.X), (∀ (j : J), m ≫ t.π.app j = s.π.app j) → m = c.lift s) . "obviously"
A cone t on F is a limit cone if each cone on F admits a unique
cone morphism to t.
@[instance]
def
category_theory.limits.is_limit.subsingleton
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cone F} :
Equations
def
category_theory.limits.is_limit.lift_cone_morphism
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cone F}
(h : category_theory.limits.is_limit t)
(s : category_theory.limits.cone F) :
s ⟶ t
The universal morphism from any other cone to a limit cone.
@[simp]
theorem
category_theory.limits.is_limit.lift_cone_morphism_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cone F}
(h : category_theory.limits.is_limit t)
(s : category_theory.limits.cone F) :
(h.lift_cone_morphism s).hom = h.lift s
theorem
category_theory.limits.is_limit.uniq_cone_morphism
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s t : category_theory.limits.cone F}
(h : category_theory.limits.is_limit t)
{f f' : s ⟶ t} :
f = f'
def
category_theory.limits.is_limit.mk_cone_morphism
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cone F}
(lift : Π (s : category_theory.limits.cone F), s ⟶ t) :
(∀ (s : category_theory.limits.cone F) (m : s ⟶ t), m = lift s) → category_theory.limits.is_limit t
Alternative constructor for is_limit,
providing a morphism of cones rather than a morphism between the cone points
and separately the factorisation condition.
Equations
- category_theory.limits.is_limit.mk_cone_morphism lift uniq' = {lift := λ (s : category_theory.limits.cone F), (lift s).hom, fac' := _, uniq' := _}
@[simp]
theorem
category_theory.limits.is_limit.unique_up_to_iso_inv
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s t : category_theory.limits.cone F}
(P : category_theory.limits.is_limit s)
(Q : category_theory.limits.is_limit t) :
(P.unique_up_to_iso Q).inv = P.lift_cone_morphism t
def
category_theory.limits.is_limit.unique_up_to_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s t : category_theory.limits.cone F} :
category_theory.limits.is_limit s → category_theory.limits.is_limit t → (s ≅ t)
Limit cones on F are unique up to isomorphism.
Equations
- P.unique_up_to_iso Q = {hom := Q.lift_cone_morphism s, inv := P.lift_cone_morphism t, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.is_limit.unique_up_to_iso_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s t : category_theory.limits.cone F}
(P : category_theory.limits.is_limit s)
(Q : category_theory.limits.is_limit t) :
(P.unique_up_to_iso Q).hom = Q.lift_cone_morphism s
def
category_theory.limits.is_limit.hom_is_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s t : category_theory.limits.cone F}
(P : category_theory.limits.is_limit s)
(Q : category_theory.limits.is_limit t)
(f : s ⟶ t) :
Any cone morphism between limit cones is an isomorphism.
Equations
- P.hom_is_iso Q f = {inv := P.lift_cone_morphism t, hom_inv_id' := _, inv_hom_id' := _}
def
category_theory.limits.is_limit.cone_point_unique_up_to_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s t : category_theory.limits.cone F} :
category_theory.limits.is_limit s → category_theory.limits.is_limit t → (s.X ≅ t.X)
Limits of F are unique up to isomorphism.
Equations
@[simp]
theorem
category_theory.limits.is_limit.cone_point_unique_up_to_iso_hom_comp_assoc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s t : category_theory.limits.cone F}
(P : category_theory.limits.is_limit s)
(Q : category_theory.limits.is_limit t)
(j : J)
{X' : C}
(f' : F.obj j ⟶ X') :
@[simp]
theorem
category_theory.limits.is_limit.cone_point_unique_up_to_iso_hom_comp
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s t : category_theory.limits.cone F}
(P : category_theory.limits.is_limit s)
(Q : category_theory.limits.is_limit t)
(j : J) :
@[simp]
theorem
category_theory.limits.is_limit.cone_point_unique_up_to_iso_inv_comp_assoc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s t : category_theory.limits.cone F}
(P : category_theory.limits.is_limit s)
(Q : category_theory.limits.is_limit t)
(j : J)
{X' : C}
(f' : F.obj j ⟶ X') :
@[simp]
theorem
category_theory.limits.is_limit.cone_point_unique_up_to_iso_inv_comp
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s t : category_theory.limits.cone F}
(P : category_theory.limits.is_limit s)
(Q : category_theory.limits.is_limit t)
(j : J) :
def
category_theory.limits.is_limit.of_iso_limit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{r t : category_theory.limits.cone F} :
category_theory.limits.is_limit r → (r ≅ t) → category_theory.limits.is_limit t
Transport evidence that a cone is a limit cone across an isomorphism of cones.
Equations
- P.of_iso_limit i = category_theory.limits.is_limit.mk_cone_morphism (λ (s : category_theory.limits.cone F), P.lift_cone_morphism s ≫ i.hom) _
def
category_theory.limits.is_limit.of_point_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{r t : category_theory.limits.cone F}
(P : category_theory.limits.is_limit r)
[i : category_theory.is_iso (P.lift t)] :
If the canonical morphism from a cone point to a limiting cone point is an iso, then the first cone was limiting also.
Equations
theorem
category_theory.limits.is_limit.hom_lift
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cone F}
(h : category_theory.limits.is_limit t)
{W : C}
(m : W ⟶ t.X) :
theorem
category_theory.limits.is_limit.hom_ext
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cone F}
(h : category_theory.limits.is_limit t)
{W : C}
{f f' : W ⟶ t.X} :
Two morphisms into a limit are equal if their compositions with each cone morphism are equal.
def
category_theory.limits.is_limit.of_right_adjoint
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{D : Type u'}
[category_theory.category D]
{G : K ⥤ D}
(h : category_theory.limits.cone G ⥤ category_theory.limits.cone F)
[category_theory.is_right_adjoint h]
{c : category_theory.limits.cone G} :
Given a right adjoint functor between categories of cones, the image of a limit cone is a limit cone.
Equations
def
category_theory.limits.is_limit.of_cone_equiv
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{D : Type u'}
[category_theory.category D]
{G : K ⥤ D}
(h : category_theory.limits.cone G ≌ category_theory.limits.cone F)
{c : category_theory.limits.cone G} :
Given two functors which have equivalent categories of cones, we can transport a limiting cone across the equivalence.
Equations
- category_theory.limits.is_limit.of_cone_equiv h = {to_fun := λ (P : category_theory.limits.is_limit (h.functor.obj c)), (category_theory.limits.is_limit.of_right_adjoint h.inverse P).of_iso_limit (h.unit_iso.symm.app c), inv_fun := category_theory.limits.is_limit.of_right_adjoint h.functor c, left_inv := _, right_inv := _}
def
category_theory.limits.is_limit.postcompose_hom_equiv
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
(α : F ≅ G)
(c : category_theory.limits.cone F) :
A cone postcomposed with a natural isomorphism is a limit cone if and only if the original cone is.
def
category_theory.limits.is_limit.postcompose_inv_equiv
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
(α : F ≅ G)
(c : category_theory.limits.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
category_theory.limits.is_limit.cone_points_iso_of_nat_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
{s : category_theory.limits.cone F}
{t : category_theory.limits.cone G} :
category_theory.limits.is_limit s → category_theory.limits.is_limit t → (F ≅ G) → (s.X ≅ t.X)
The cone points of two limit cones for naturally isomorphic functors are themselves isomorphic.
Equations
- P.cone_points_iso_of_nat_iso Q w = {hom := Q.lift ((category_theory.limits.cones.postcompose w.hom).obj s), inv := P.lift ((category_theory.limits.cones.postcompose w.inv).obj t), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.is_limit.cone_points_iso_of_nat_iso_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
{s : category_theory.limits.cone F}
{t : category_theory.limits.cone G}
(P : category_theory.limits.is_limit s)
(Q : category_theory.limits.is_limit t)
(w : F ≅ G) :
(P.cone_points_iso_of_nat_iso Q w).hom = Q.lift ((category_theory.limits.cones.postcompose w.hom).obj s)
@[simp]
theorem
category_theory.limits.is_limit.cone_points_iso_of_nat_iso_inv
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
{s : category_theory.limits.cone F}
{t : category_theory.limits.cone G}
(P : category_theory.limits.is_limit s)
(Q : category_theory.limits.is_limit t)
(w : F ≅ G) :
(P.cone_points_iso_of_nat_iso Q w).inv = P.lift ((category_theory.limits.cones.postcompose w.inv).obj t)
def
category_theory.limits.is_limit.whisker_equivalence
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s : category_theory.limits.cone F}
(P : category_theory.limits.is_limit s)
(e : K ≌ J) :
If s : cone F is a limit cone, so is s whiskered by an equivalence e.
def
category_theory.limits.is_limit.cone_points_iso_of_equivalence
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s : category_theory.limits.cone F}
{G : K ⥤ C}
{t : category_theory.limits.cone G}
(P : category_theory.limits.is_limit s)
(Q : category_theory.limits.is_limit t)
(e : J ≌ K) :
We can prove two cone points (s : cone F).X and (t.cone F).X 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
- P.cone_points_iso_of_equivalence Q e w = let w' : e.inverse ⋙ F ≅ G := (category_theory.iso_whisker_left e.inverse w).symm ≪≫ e.inv_fun_id_assoc G in {hom := Q.lift ((category_theory.limits.cones.equivalence_of_reindexing e.symm w').functor.obj s), inv := P.lift ((category_theory.limits.cones.equivalence_of_reindexing e w).functor.obj t), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.is_limit.cone_points_iso_of_equivalence_hom
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s : category_theory.limits.cone F}
{G : K ⥤ C}
{t : category_theory.limits.cone G}
(P : category_theory.limits.is_limit s)
(Q : category_theory.limits.is_limit t)
(e : J ≌ K)
(w : e.functor ⋙ G ≅ F) :
(P.cone_points_iso_of_equivalence Q e w).hom = Q.lift ((category_theory.limits.cones.equivalence_of_reindexing e.symm ((category_theory.iso_whisker_left e.inverse w).symm ≪≫ e.inv_fun_id_assoc G)).functor.obj s)
@[simp]
theorem
category_theory.limits.is_limit.cone_points_iso_of_equivalence_inv
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s : category_theory.limits.cone F}
{G : K ⥤ C}
{t : category_theory.limits.cone G}
(P : category_theory.limits.is_limit s)
(Q : category_theory.limits.is_limit t)
(e : J ≌ K)
(w : e.functor ⋙ G ≅ F) :
(P.cone_points_iso_of_equivalence Q e w).inv = P.lift ((category_theory.limits.cones.equivalence_of_reindexing e w).functor.obj t)
def
category_theory.limits.is_limit.hom_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cone F}
(h : category_theory.limits.is_limit t)
(W : C) :
The universal property of a limit cone: a map W ⟶ X is the same as
a cone on F with vertex W.
@[simp]
theorem
category_theory.limits.is_limit.hom_iso_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cone F}
(h : category_theory.limits.is_limit t)
{W : C}
(f : W ⟶ t.X) :
def
category_theory.limits.is_limit.nat_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cone F} :
The limit of F represents the functor taking W to
the set of cones on F with vertex W.
Equations
- h.nat_iso = category_theory.nat_iso.of_components (λ (W : Cᵒᵖ), h.hom_iso (opposite.unop W)) _
def
category_theory.limits.is_limit.hom_iso'
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cone F}
(h : category_theory.limits.is_limit t)
(W : C) :
Another, more explicit, formulation of the universal property of a limit cone.
See also hom_iso.
def
category_theory.limits.is_limit.of_faithful
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cone F}
{D : Type u'}
[category_theory.category D]
(G : C ⥤ D)
[category_theory.faithful G]
(ht : category_theory.limits.is_limit (G.map_cone t))
(lift : Π (s : category_theory.limits.cone F), s.X ⟶ t.X) :
(∀ (s : category_theory.limits.cone F), G.map (lift s) = ht.lift (G.map_cone s)) → category_theory.limits.is_limit 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.
def
category_theory.limits.is_limit.map_cone_equiv
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
{K : J ⥤ C}
{F G : C ⥤ D}
(h : F ≅ G)
{c : category_theory.limits.cone K} :
If F and G are naturally isomorphic, then F.map_cone c being a limit implies
G.map_cone c is also a limit.
Equations
- category_theory.limits.is_limit.map_cone_equiv h t = {lift := λ (s : category_theory.limits.cone (K ⋙ G)), t.lift ((category_theory.limits.cones.postcompose (category_theory.iso_whisker_left K h).inv).obj s) ≫ h.hom.app c.X, fac' := _, uniq' := _}
def
category_theory.limits.is_limit.iso_unique_cone_morphism
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cone F} :
category_theory.limits.is_limit t ≅ Π (s : category_theory.limits.cone F), unique (s ⟶ t)
A cone is a limit cone exactly if there is a unique cone morphism from any other cone.
Equations
- category_theory.limits.is_limit.iso_unique_cone_morphism = {hom := λ (h : category_theory.limits.is_limit t) (s : category_theory.limits.cone F), {to_inhabited := {default := h.lift_cone_morphism s}, uniq := _}, inv := λ (h : Π (s : category_theory.limits.cone F), unique (s ⟶ t)), {lift := λ (s : category_theory.limits.cone F), (inhabited.default (s ⟶ t)).hom, fac' := _, uniq' := _}, hom_inv_id' := _, inv_hom_id' := _}
def
category_theory.limits.is_limit.of_nat_iso.cone_of_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.yoneda.obj X ≅ F.cones)
{Y : C} :
(Y ⟶ X) → category_theory.limits.cone F
If F.cones is represented by X, each morphism f : Y ⟶ X gives a cone with cone point Y.
Equations
- category_theory.limits.is_limit.of_nat_iso.cone_of_hom h f = {X := Y, π := h.hom.app (opposite.op Y) f}
def
category_theory.limits.is_limit.of_nat_iso.hom_of_cone
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.yoneda.obj X ≅ F.cones)
(s : category_theory.limits.cone F) :
If F.cones is represented by X, each cone s gives a morphism s.X ⟶ X.
Equations
@[simp]
theorem
category_theory.limits.is_limit.of_nat_iso.cone_of_hom_of_cone
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.yoneda.obj X ≅ F.cones)
(s : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.is_limit.of_nat_iso.hom_of_cone_of_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.yoneda.obj X ≅ F.cones)
{Y : C}
(f : Y ⟶ X) :
def
category_theory.limits.is_limit.of_nat_iso.limit_cone
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{X : C} :
If F.cones is represented by X, the cone corresponding to the identity morphism on X
will be a limit cone.
theorem
category_theory.limits.is_limit.of_nat_iso.cone_of_hom_fac
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.yoneda.obj X ≅ F.cones)
{Y : C}
(f : Y ⟶ X) :
If F.cones is represented by X, the cone corresponding to a morphism f : Y ⟶ X is
the limit cone extended by f.
theorem
category_theory.limits.is_limit.of_nat_iso.cone_fac
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.yoneda.obj X ≅ F.cones)
(s : category_theory.limits.cone F) :
If F.cones is represented by X, any cone is the extension of the limit cone by the
corresponding morphism.
def
category_theory.limits.is_limit.of_nat_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.yoneda.obj X ≅ F.cones) :
If F.cones is representable, then the cone corresponding to the identity morphism on
the representing object is a limit cone.
Equations
- category_theory.limits.is_limit.of_nat_iso h = {lift := λ (s : category_theory.limits.cone F), category_theory.limits.is_limit.of_nat_iso.hom_of_cone h s, fac' := _, uniq' := _}
@[nolint]
structure
category_theory.limits.is_colimit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C} :
category_theory.limits.cocone F → Type (max u v)
- desc : Π (s : category_theory.limits.cocone F), t.X ⟶ s.X
- fac' : (∀ (s : category_theory.limits.cocone F) (j : J), t.ι.app j ≫ c.desc s = s.ι.app j) . "obviously"
- uniq' : (∀ (s : category_theory.limits.cocone F) (m : t.X ⟶ s.X), (∀ (j : J), t.ι.app j ≫ m = s.ι.app j) → m = c.desc s) . "obviously"
A cocone t on F is a colimit cocone if each cocone on F admits a unique
cocone morphism from t.
@[instance]
def
category_theory.limits.is_colimit.subsingleton
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cocone F} :
Equations
def
category_theory.limits.is_colimit.desc_cocone_morphism
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cocone F}
(h : category_theory.limits.is_colimit t)
(s : category_theory.limits.cocone F) :
t ⟶ s
The universal morphism from a colimit cocone to any other cone.
@[simp]
theorem
category_theory.limits.is_colimit.desc_cocone_morphism_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cocone F}
(h : category_theory.limits.is_colimit t)
(s : category_theory.limits.cocone F) :
(h.desc_cocone_morphism s).hom = h.desc s
theorem
category_theory.limits.is_colimit.uniq_cocone_morphism
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s t : category_theory.limits.cocone F}
(h : category_theory.limits.is_colimit t)
{f f' : t ⟶ s} :
f = f'
def
category_theory.limits.is_colimit.mk_cocone_morphism
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cocone F}
(desc : Π (s : category_theory.limits.cocone F), t ⟶ s) :
(∀ (s : category_theory.limits.cocone F) (m : t ⟶ s), m = desc s) → category_theory.limits.is_colimit t
Alternative constructor for is_colimit,
providing a morphism of cocones rather than a morphism between the cocone points
and separately the factorisation condition.
Equations
- category_theory.limits.is_colimit.mk_cocone_morphism desc uniq' = {desc := λ (s : category_theory.limits.cocone F), (desc s).hom, fac' := _, uniq' := _}
def
category_theory.limits.is_colimit.unique_up_to_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s t : category_theory.limits.cocone F} :
Colimit cocones on F are unique up to isomorphism.
Equations
- P.unique_up_to_iso Q = {hom := P.desc_cocone_morphism t, inv := Q.desc_cocone_morphism s, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.is_colimit.unique_up_to_iso_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s t : category_theory.limits.cocone F}
(P : category_theory.limits.is_colimit s)
(Q : category_theory.limits.is_colimit t) :
(P.unique_up_to_iso Q).hom = P.desc_cocone_morphism t
@[simp]
theorem
category_theory.limits.is_colimit.unique_up_to_iso_inv
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s t : category_theory.limits.cocone F}
(P : category_theory.limits.is_colimit s)
(Q : category_theory.limits.is_colimit t) :
(P.unique_up_to_iso Q).inv = Q.desc_cocone_morphism s
def
category_theory.limits.is_colimit.hom_is_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s t : category_theory.limits.cocone F}
(P : category_theory.limits.is_colimit s)
(Q : category_theory.limits.is_colimit t)
(f : s ⟶ t) :
Any cocone morphism between colimit cocones is an isomorphism.
Equations
- P.hom_is_iso Q f = {inv := Q.desc_cocone_morphism s, hom_inv_id' := _, inv_hom_id' := _}
def
category_theory.limits.is_colimit.cocone_point_unique_up_to_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s t : category_theory.limits.cocone F} :
category_theory.limits.is_colimit s → category_theory.limits.is_colimit t → (s.X ≅ t.X)
Colimits of F are unique up to isomorphism.
Equations
@[simp]
theorem
category_theory.limits.is_colimit.comp_cocone_point_unique_up_to_iso_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s t : category_theory.limits.cocone F}
(P : category_theory.limits.is_colimit s)
(Q : category_theory.limits.is_colimit t)
(j : J) :
@[simp]
theorem
category_theory.limits.is_colimit.comp_cocone_point_unique_up_to_iso_hom_assoc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s t : category_theory.limits.cocone F}
(P : category_theory.limits.is_colimit s)
(Q : category_theory.limits.is_colimit t)
(j : J)
{X' : C}
(f' : t.X ⟶ X') :
@[simp]
theorem
category_theory.limits.is_colimit.comp_cocone_point_unique_up_to_iso_inv_assoc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s t : category_theory.limits.cocone F}
(P : category_theory.limits.is_colimit s)
(Q : category_theory.limits.is_colimit t)
(j : J)
{X' : C}
(f' : s.X ⟶ X') :
@[simp]
theorem
category_theory.limits.is_colimit.comp_cocone_point_unique_up_to_iso_inv
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s t : category_theory.limits.cocone F}
(P : category_theory.limits.is_colimit s)
(Q : category_theory.limits.is_colimit t)
(j : J) :
def
category_theory.limits.is_colimit.of_iso_colimit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{r t : category_theory.limits.cocone F} :
Transport evidence that a cocone is a colimit cocone across an isomorphism of cocones.
Equations
- P.of_iso_colimit i = category_theory.limits.is_colimit.mk_cocone_morphism (λ (s : category_theory.limits.cocone F), i.inv ≫ P.desc_cocone_morphism s) _
def
category_theory.limits.is_colimit.of_point_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{r t : category_theory.limits.cocone F}
(P : category_theory.limits.is_colimit r)
[i : category_theory.is_iso (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
theorem
category_theory.limits.is_colimit.hom_desc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cocone F}
(h : category_theory.limits.is_colimit t)
{W : C}
(m : t.X ⟶ W) :
theorem
category_theory.limits.is_colimit.hom_ext
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cocone F}
(h : category_theory.limits.is_colimit t)
{W : C}
{f f' : t.X ⟶ W} :
Two morphisms out of a colimit are equal if their compositions with each cocone morphism are equal.
def
category_theory.limits.is_colimit.of_left_adjoint
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{D : Type u'}
[category_theory.category D]
{G : K ⥤ D}
(h : category_theory.limits.cocone G ⥤ category_theory.limits.cocone F)
[category_theory.is_left_adjoint h]
{c : category_theory.limits.cocone G} :
Given a left adjoint functor between categories of cocones, the image of a colimit cocone is a colimit cocone.
Equations
def
category_theory.limits.is_colimit.of_cocone_equiv
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{D : Type u'}
[category_theory.category D]
{G : K ⥤ D}
(h : category_theory.limits.cocone G ≌ category_theory.limits.cocone F)
{c : category_theory.limits.cocone G} :
Given two functors which have equivalent categories of cocones, we can transport a colimiting cocone across the equivalence.
Equations
- category_theory.limits.is_colimit.of_cocone_equiv h = {to_fun := λ (P : category_theory.limits.is_colimit (h.functor.obj c)), (category_theory.limits.is_colimit.of_left_adjoint h.inverse P).of_iso_colimit (h.unit_iso.symm.app c), inv_fun := category_theory.limits.is_colimit.of_left_adjoint h.functor c, left_inv := _, right_inv := _}
def
category_theory.limits.is_colimit.precompose_hom_equiv
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
(α : F ≅ G)
(c : category_theory.limits.cocone G) :
A cocone precomposed with a natural isomorphism is a colimit cocone if and only if the original cocone is.
def
category_theory.limits.is_colimit.precompose_inv_equiv
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
(α : F ≅ G)
(c : category_theory.limits.cocone F) :
A cocone precomposed with the inverse of a natural isomorphism is a colimit cocone if and only if the original cocone is.
@[simp]
theorem
category_theory.limits.is_colimit.cocone_points_iso_of_nat_iso_inv
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
{s : category_theory.limits.cocone F}
{t : category_theory.limits.cocone G}
(P : category_theory.limits.is_colimit s)
(Q : category_theory.limits.is_colimit t)
(w : F ≅ G) :
(P.cocone_points_iso_of_nat_iso Q w).inv = Q.desc ((category_theory.limits.cocones.precompose w.inv).obj s)
def
category_theory.limits.is_colimit.cocone_points_iso_of_nat_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
{s : category_theory.limits.cocone F}
{t : category_theory.limits.cocone G} :
category_theory.limits.is_colimit s → category_theory.limits.is_colimit t → (F ≅ G) → (s.X ≅ t.X)
The cocone points of two colimit cocones for naturally isomorphic functors are themselves isomorphic.
Equations
- P.cocone_points_iso_of_nat_iso Q w = {hom := P.desc ((category_theory.limits.cocones.precompose w.hom).obj t), inv := Q.desc ((category_theory.limits.cocones.precompose w.inv).obj s), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.is_colimit.cocone_points_iso_of_nat_iso_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
{s : category_theory.limits.cocone F}
{t : category_theory.limits.cocone G}
(P : category_theory.limits.is_colimit s)
(Q : category_theory.limits.is_colimit t)
(w : F ≅ G) :
(P.cocone_points_iso_of_nat_iso Q w).hom = P.desc ((category_theory.limits.cocones.precompose w.hom).obj t)
def
category_theory.limits.is_colimit.whisker_equivalence
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s : category_theory.limits.cocone F}
(P : category_theory.limits.is_colimit s)
(e : K ≌ J) :
If s : cone F is a limit cone, so is s whiskered by an equivalence e.
@[simp]
theorem
category_theory.limits.is_colimit.cocone_points_iso_of_equivalence_inv
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s : category_theory.limits.cocone F}
{G : K ⥤ C}
{t : category_theory.limits.cocone G}
(P : category_theory.limits.is_colimit s)
(Q : category_theory.limits.is_colimit t)
(e : J ≌ K)
(w : e.functor ⋙ G ≅ F) :
(P.cocone_points_iso_of_equivalence Q e w).inv = Q.desc ((category_theory.limits.cocones.equivalence_of_reindexing e.symm ((category_theory.iso_whisker_left e.inverse w).symm ≪≫ e.inv_fun_id_assoc G)).functor.obj s)
def
category_theory.limits.is_colimit.cocone_points_iso_of_equivalence
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s : category_theory.limits.cocone F}
{G : K ⥤ C}
{t : category_theory.limits.cocone G}
(P : category_theory.limits.is_colimit s)
(Q : category_theory.limits.is_colimit t)
(e : J ≌ K) :
We can prove two cocone points (s : cocone F).X and (t.cocone F).X are isomorphic if
- both cocones are colimit ccoones
- 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
- P.cocone_points_iso_of_equivalence Q e w = let w' : e.inverse ⋙ F ≅ G := (category_theory.iso_whisker_left e.inverse w).symm ≪≫ e.inv_fun_id_assoc G in {hom := P.desc ((category_theory.limits.cocones.equivalence_of_reindexing e w).functor.obj t), inv := Q.desc ((category_theory.limits.cocones.equivalence_of_reindexing e.symm w').functor.obj s), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.is_colimit.cocone_points_iso_of_equivalence_hom
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{s : category_theory.limits.cocone F}
{G : K ⥤ C}
{t : category_theory.limits.cocone G}
(P : category_theory.limits.is_colimit s)
(Q : category_theory.limits.is_colimit t)
(e : J ≌ K)
(w : e.functor ⋙ G ≅ F) :
(P.cocone_points_iso_of_equivalence Q e w).hom = P.desc ((category_theory.limits.cocones.equivalence_of_reindexing e w).functor.obj t)
def
category_theory.limits.is_colimit.hom_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cocone F}
(h : category_theory.limits.is_colimit t)
(W : C) :
The universal property of a colimit cocone: a map X ⟶ W is the same as
a cocone on F with vertex W.
@[simp]
theorem
category_theory.limits.is_colimit.hom_iso_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cocone F}
(h : category_theory.limits.is_colimit t)
{W : C}
(f : t.X ⟶ W) :
def
category_theory.limits.is_colimit.nat_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cocone F} :
The colimit of F represents the functor taking W to
the set of cocones on F with vertex W.
Equations
def
category_theory.limits.is_colimit.hom_iso'
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cocone F}
(h : category_theory.limits.is_colimit t)
(W : C) :
Another, more explicit, formulation of the universal property of a colimit cocone.
See also hom_iso.
def
category_theory.limits.is_colimit.of_faithful
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cocone F}
{D : Type u'}
[category_theory.category D]
(G : C ⥤ D)
[category_theory.faithful G]
(ht : category_theory.limits.is_colimit (G.map_cocone t))
(desc : Π (s : category_theory.limits.cocone F), t.X ⟶ s.X) :
(∀ (s : category_theory.limits.cocone F), G.map (desc s) = ht.desc (G.map_cocone s)) → category_theory.limits.is_colimit 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.
def
category_theory.limits.is_colimit.iso_unique_cocone_morphism
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cocone F} :
category_theory.limits.is_colimit t ≅ Π (s : category_theory.limits.cocone F), unique (t ⟶ s)
A cocone is a colimit cocone exactly if there is a unique cocone morphism from any other cocone.
Equations
- category_theory.limits.is_colimit.iso_unique_cocone_morphism = {hom := λ (h : category_theory.limits.is_colimit t) (s : category_theory.limits.cocone F), {to_inhabited := {default := h.desc_cocone_morphism s}, uniq := _}, inv := λ (h : Π (s : category_theory.limits.cocone F), unique (t ⟶ s)), {desc := λ (s : category_theory.limits.cocone F), (inhabited.default (t ⟶ s)).hom, fac' := _, uniq' := _}, hom_inv_id' := _, inv_hom_id' := _}
def
category_theory.limits.is_colimit.of_nat_iso.cocone_of_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.coyoneda.obj (opposite.op X) ≅ F.cocones)
{Y : C} :
(X ⟶ Y) → category_theory.limits.cocone F
If F.cocones is corepresented by X, each morphism f : X ⟶ Y gives a cocone with cone point Y.
def
category_theory.limits.is_colimit.of_nat_iso.hom_of_cocone
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.coyoneda.obj (opposite.op X) ≅ F.cocones)
(s : category_theory.limits.cocone F) :
If F.cocones is corepresented by X, each cocone s gives a morphism X ⟶ s.X.
@[simp]
theorem
category_theory.limits.is_colimit.of_nat_iso.cocone_of_hom_of_cocone
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.coyoneda.obj (opposite.op X) ≅ F.cocones)
(s : category_theory.limits.cocone F) :
@[simp]
theorem
category_theory.limits.is_colimit.of_nat_iso.hom_of_cocone_of_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.coyoneda.obj (opposite.op X) ≅ F.cocones)
{Y : C}
(f : X ⟶ Y) :
def
category_theory.limits.is_colimit.of_nat_iso.colimit_cocone
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{X : C} :
If F.cocones is corepresented by X, the cocone corresponding to the identity morphism on X
will be a colimit cocone.
theorem
category_theory.limits.is_colimit.of_nat_iso.cocone_of_hom_fac
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.coyoneda.obj (opposite.op X) ≅ F.cocones)
{Y : C}
(f : X ⟶ Y) :
If F.cocones is corepresented by X, the cocone corresponding to a morphism f : Y ⟶ X is
the colimit cocone extended by f.
theorem
category_theory.limits.is_colimit.of_nat_iso.cocone_fac
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.coyoneda.obj (opposite.op X) ≅ F.cocones)
(s : category_theory.limits.cocone F) :
If F.cocones is corepresented by X, any cocone is the extension of the colimit cocone by the
corresponding morphism.
def
category_theory.limits.is_colimit.of_nat_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.coyoneda.obj (opposite.op X) ≅ F.cocones) :
If F.cocones is corepresentable, then the cocone corresponding to the identity morphism on
the representing object is a colimit cocone.
Equations
- category_theory.limits.is_colimit.of_nat_iso h = {desc := λ (s : category_theory.limits.cocone F), category_theory.limits.is_colimit.of_nat_iso.hom_of_cocone h s, fac' := _, uniq' := _}
@[class]
structure
category_theory.limits.has_limit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C] :
J ⥤ C → Type (max u v)
- cone : category_theory.limits.cone F
- is_limit : category_theory.limits.is_limit category_theory.limits.has_limit.cone
has_limit F represents a particular chosen limit of the diagram F.
Instances
- category_theory.limits.has_limit_of_has_limits_of_shape
- category_theory.limits.has_product_of_has_biproduct
- category_theory.limits.has_limit_equivalence_comp
- category_theory.limits.has_binary_biproduct.has_limit_pair
- AddCommGroup.has_limit.has_limit_discrete
- category_theory.adjunction.has_limit_comp_equivalence
- category_theory.under.has_limit
- category_theory.comp_comparison_forget_has_limit
- category_theory.comp_comparison_has_limit
@[class]
structure
category_theory.limits.has_limits_of_shape
(J : Type v)
[category_theory.small_category J]
(C : Type u)
[category_theory.category C] :
Type (max u v)
- has_limit : Π (F : J ⥤ C), category_theory.limits.has_limit F
C has limits of shape J if we have chosen a particular limit of
every functor F : J ⥤ C.
Instances
- category_theory.limits.has_limits_of_shape_of_has_limits
- category_theory.limits.has_limits_of_shape_of_has_finite_limits
- category_theory.limits.has_limits_of_shape_wide_pullback_shape
- category_theory.limits.has_limits_of_shape_discrete
- category_theory.limits.functor_category_has_limits_of_shape
- category_theory.under.has_limits_of_shape
- category_theory.over.has_connected_limits
@[class]
structure
category_theory.limits.has_limits
(C : Type u)
[category_theory.category C] :
Type (max u (v+1))
- has_limits_of_shape : Π (J : Type ?) [𝒥 : category_theory.small_category J], category_theory.limits.has_limits_of_shape J C
C has all (small) limits if it has limits of every shape.
Instances
- category_theory.limits.has_limits_of_complete_lattice
- category_theory.limits.types.category_theory.limits.has_limits
- Mon.has_limits
- AddMon.has_limits
- CommMon.has_limits
- AddCommMon.has_limits
- Group.has_limits
- AddGroup.has_limits
- CommGroup.has_limits
- AddCommGroup.has_limits
- Module.has_limits
- SemiRing.has_limits
- CommSemiRing.has_limits
- Ring.has_limits
- CommRing.has_limits
- Algebra.has_limits
- category_theory.limits.functor_category_has_limits
- category_theory.under.has_limits
- category_theory.limits.category_theory.limits.has_limits
- category_theory.over.has_limits
- Top.Top_has_limits
@[instance]
def
category_theory.limits.has_limit_of_has_limits_of_shape
{C : Type u}
[category_theory.category C]
{J : Type v}
[category_theory.small_category J]
[H : category_theory.limits.has_limits_of_shape J C]
(F : J ⥤ C) :
@[instance]
def
category_theory.limits.has_limits_of_shape_of_has_limits
{C : Type u}
[category_theory.category C]
{J : Type v}
[category_theory.small_category J]
[H : category_theory.limits.has_limits C] :
def
category_theory.limits.limit.cone
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F] :
The chosen limit cone of a functor.
def
category_theory.limits.limit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F] :
C
The chosen limit object of a functor.
Equations
def
category_theory.limits.limit.π
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
(j : J) :
category_theory.limits.limit F ⟶ F.obj j
The projection from the chosen limit object to a value of the functor.
Equations
@[simp]
theorem
category_theory.limits.limit.cone_π
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(j : J) :
@[simp]
theorem
category_theory.limits.limit.w
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
{j j' : J}
(f : j ⟶ j') :
category_theory.limits.limit.π F j ≫ F.map f = category_theory.limits.limit.π F j'
def
category_theory.limits.limit.is_limit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F] :
Evidence that the chosen cone is a limit cone.
def
category_theory.limits.limit.lift
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
(c : category_theory.limits.cone F) :
The morphism from the cone point of any other cone to the chosen limit object.
Equations
@[simp]
theorem
category_theory.limits.limit.is_limit_lift
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(c : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.limit.lift_π_assoc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(c : category_theory.limits.cone F)
(j : J)
{X' : C}
(f' : F.obj j ⟶ X') :
category_theory.limits.limit.lift F c ≫ category_theory.limits.limit.π F j ≫ f' = c.π.app j ≫ f'
@[simp]
theorem
category_theory.limits.limit.lift_π
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(c : category_theory.limits.cone F)
(j : J) :
def
category_theory.limits.limit.cone_morphism
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(c : category_theory.limits.cone F) :
The cone morphism from any cone to the chosen limit cone.
@[simp]
theorem
category_theory.limits.limit.cone_morphism_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(c : category_theory.limits.cone F) :
theorem
category_theory.limits.limit.cone_morphism_π
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(c : category_theory.limits.cone F)
(j : J) :
@[simp]
theorem
category_theory.limits.limit.cone_point_unique_up_to_iso_hom_comp
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
{c : category_theory.limits.cone F}
(hc : category_theory.limits.is_limit c)
(j : J) :
@[simp]
theorem
category_theory.limits.limit.cone_point_unique_up_to_iso_hom_comp_assoc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
{c : category_theory.limits.cone F}
(hc : category_theory.limits.is_limit c)
(j : J)
{X' : C}
(f' : F.obj j ⟶ X') :
(hc.cone_point_unique_up_to_iso (category_theory.limits.limit.is_limit F)).hom ≫ category_theory.limits.limit.π F j ≫ f' = c.π.app j ≫ f'
@[simp]
theorem
category_theory.limits.limit.cone_point_unique_up_to_iso_inv_comp
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
{c : category_theory.limits.cone F}
(hc : category_theory.limits.is_limit c)
(j : J) :
@[simp]
theorem
category_theory.limits.limit.cone_point_unique_up_to_iso_inv_comp_assoc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
{c : category_theory.limits.cone F}
(hc : category_theory.limits.is_limit c)
(j : J)
{X' : C}
(f' : F.obj j ⟶ X') :
((category_theory.limits.limit.is_limit F).cone_point_unique_up_to_iso hc).inv ≫ category_theory.limits.limit.π F j ≫ f' = c.π.app j ≫ f'
@[ext]
theorem
category_theory.limits.limit.hom_ext
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
{X : C}
{f f' : X ⟶ category_theory.limits.limit F} :
(∀ (j : J), f ≫ category_theory.limits.limit.π F j = f' ≫ category_theory.limits.limit.π F j) → f = f'
def
category_theory.limits.limit.hom_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
(W : C) :
(W ⟶ category_theory.limits.limit F) ≅ F.cones.obj (opposite.op W)
The isomorphism (in Type) between
morphisms from a specified object W to the limit object,
and cones with cone point W.
Equations
@[simp]
theorem
category_theory.limits.limit.hom_iso_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
{W : C}
(f : W ⟶ category_theory.limits.limit F) :
def
category_theory.limits.limit.hom_iso'
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
(W : C) :
The isomorphism (in Type) between
morphisms from a specified object W to the limit object,
and an explicit componentwise description of cones with cone point W.
Equations
theorem
category_theory.limits.limit.lift_extend
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
(c : category_theory.limits.cone F)
{X : C}
(f : X ⟶ c.X) :
def
category_theory.limits.has_limit_of_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F] :
(F ≅ G) → category_theory.limits.has_limit G
If we've chosen a limit for a functor F,
we can transport that choice across a natural isomorphism.
Equations
- category_theory.limits.has_limit_of_iso α = {cone := (category_theory.limits.cones.postcompose α.hom).obj (category_theory.limits.limit.cone F), is_limit := {lift := λ (s : category_theory.limits.cone G), category_theory.limits.limit.lift F ((category_theory.limits.cones.postcompose α.inv).obj s), fac' := _, uniq' := _}}
def
category_theory.limits.has_limit.of_cones_iso
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
(F : J ⥤ C)
(G : K ⥤ C)
(h : F.cones ≅ G.cones)
[category_theory.limits.has_limit F] :
If a functor G has the same collection of cones as a functor F
which has a limit, then G also has a limit.
def
category_theory.limits.has_limit.iso_of_nat_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit G] :
(F ≅ G) → (category_theory.limits.limit F ≅ category_theory.limits.limit G)
The chosen limits of F : J ⥤ C and G : J ⥤ C are isomorphic,
if the functors are naturally isomorphic.
@[simp]
theorem
category_theory.limits.has_limit.iso_of_nat_iso_hom_π_assoc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit G]
(w : F ≅ G)
(j : J)
{X' : C}
(f' : G.obj j ⟶ X') :
(category_theory.limits.has_limit.iso_of_nat_iso w).hom ≫ category_theory.limits.limit.π G j ≫ f' = category_theory.limits.limit.π F j ≫ w.hom.app j ≫ f'
@[simp]
theorem
category_theory.limits.has_limit.iso_of_nat_iso_hom_π
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit G]
(w : F ≅ G)
(j : J) :
def
category_theory.limits.has_limit.iso_of_equivalence
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
{G : K ⥤ C}
[category_theory.limits.has_limit G]
(e : J ≌ K) :
(e.functor ⋙ G ≅ F) → (category_theory.limits.limit F ≅ category_theory.limits.limit G)
The chosen limits of F : J ⥤ C and G : K ⥤ C are isomorphic,
if there is an equivalence e : J ≌ K making the triangle commute up to natural isomorphism.
@[simp]
theorem
category_theory.limits.has_limit.iso_of_equivalence_π
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limit F]
{G : K ⥤ C}
[category_theory.limits.has_limit G]
(e : J ≌ K)
(w : e.functor ⋙ G ≅ F)
(k : K) :
def
category_theory.limits.limit.pre
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
(E : K ⥤ J)
[category_theory.limits.has_limit (E ⋙ F)] :
The canonical morphism
from the chosen limit of F
to the chosen limit of E ⋙ F.
Equations
- category_theory.limits.limit.pre F E = category_theory.limits.limit.lift (E ⋙ F) {X := category_theory.limits.limit F _inst_4, π := {app := λ (k : K), category_theory.limits.limit.π F (E.obj k), naturality' := _}}
@[simp]
theorem
category_theory.limits.limit.pre_π
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
(E : K ⥤ J)
[category_theory.limits.has_limit (E ⋙ F)]
(k : K) :
category_theory.limits.limit.pre F E ≫ category_theory.limits.limit.π (E ⋙ F) k = category_theory.limits.limit.π F (E.obj k)
@[simp]
theorem
category_theory.limits.limit.lift_pre
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
(E : K ⥤ J)
[category_theory.limits.has_limit (E ⋙ F)]
(c : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.limit.pre_pre
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_limit F]
(E : K ⥤ J)
[category_theory.limits.has_limit (E ⋙ F)]
{L : Type v}
[category_theory.small_category L]
(D : L ⥤ K)
[category_theory.limits.has_limit (D ⋙ E ⋙ F)] :
category_theory.limits.limit.pre F E ≫ category_theory.limits.limit.pre (E ⋙ F) D = category_theory.limits.limit.pre F (D ⋙ E)
def
category_theory.limits.limit.post
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_limit F]
(G : C ⥤ D)
[category_theory.limits.has_limit (F ⋙ G)] :
G.obj (category_theory.limits.limit F) ⟶ category_theory.limits.limit (F ⋙ G)
The canonical morphism
from G applied to the chosen limit of F
to the chosen limit of F ⋙ G.
Equations
- category_theory.limits.limit.post F G = category_theory.limits.limit.lift (F ⋙ G) {X := G.obj (category_theory.limits.limit F), π := {app := λ (j : J), G.map (category_theory.limits.limit.π F j), naturality' := _}}
@[simp]
theorem
category_theory.limits.limit.post_π
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_limit F]
(G : C ⥤ D)
[category_theory.limits.has_limit (F ⋙ G)]
(j : J) :
category_theory.limits.limit.post F G ≫ category_theory.limits.limit.π (F ⋙ G) j = G.map (category_theory.limits.limit.π F j)
@[simp]
theorem
category_theory.limits.limit.lift_post
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_limit F]
(G : C ⥤ D)
[category_theory.limits.has_limit (F ⋙ G)]
(c : category_theory.limits.cone F) :
G.map (category_theory.limits.limit.lift F c) ≫ category_theory.limits.limit.post F G = category_theory.limits.limit.lift (F ⋙ G) (G.map_cone c)
@[simp]
theorem
category_theory.limits.limit.post_post
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_limit F]
(G : C ⥤ D)
[category_theory.limits.has_limit (F ⋙ G)]
{E : Type u''}
[category_theory.category E]
(H : D ⥤ E)
[category_theory.limits.has_limit ((F ⋙ G) ⋙ H)] :
H.map (category_theory.limits.limit.post F G) ≫ category_theory.limits.limit.post (F ⋙ G) H = category_theory.limits.limit.post F (G ⋙ H)
theorem
category_theory.limits.limit.pre_post
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
(E : K ⥤ J)
(F : J ⥤ C)
(G : C ⥤ D)
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit (E ⋙ F)]
[category_theory.limits.has_limit (F ⋙ G)]
[category_theory.limits.has_limit ((E ⋙ F) ⋙ G)] :
G.map (category_theory.limits.limit.pre F E) ≫ category_theory.limits.limit.post (E ⋙ F) G = category_theory.limits.limit.post F G ≫ category_theory.limits.limit.pre (F ⋙ G) E
@[instance]
def
category_theory.limits.has_limit_equivalence_comp
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
(e : K ≌ J)
[category_theory.limits.has_limit F] :
def
category_theory.limits.has_limit_of_equivalence_comp
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
(e : K ≌ J)
[category_theory.limits.has_limit (e.functor ⋙ F)] :
If a E ⋙ F has a chosen limit, and E is an equivalence, we can construct a chosen limit of F.
def
category_theory.limits.lim_map
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit G] :
(F ⟶ G) → (category_theory.limits.limit F ⟶ category_theory.limits.limit G)
Functoriality of limits.
Usually this morphism should be accessed through lim.map,
but may be needed separately when you have specified limits for the source and target functors,
but not necessarily for all functors of shape J.
Equations
- category_theory.limits.lim_map α = category_theory.limits.limit.lift G {X := category_theory.limits.limit F _inst_4, π := {app := λ (j : J), category_theory.limits.limit.π F j ≫ α.app j, naturality' := _}}
@[simp]
theorem
category_theory.limits.lim_map_π
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit G]
(α : F ⟶ G)
(j : J) :
@[simp]
theorem
category_theory.limits.lim_map_π_assoc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_limit F]
[category_theory.limits.has_limit G]
(α : F ⟶ G)
(j : J)
{X' : C}
(f' : G.obj j ⟶ X') :
category_theory.limits.lim_map α ≫ category_theory.limits.limit.π G j ≫ f' = category_theory.limits.limit.π F j ≫ α.app j ≫ f'
def
category_theory.limits.lim
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape J C] :
limit F is functorial in F, when C has all limits of shape J.
Equations
- category_theory.limits.lim = {obj := λ (F : J ⥤ C), category_theory.limits.limit F, map := λ (F G : J ⥤ C) (α : F ⟶ G), category_theory.limits.lim_map α, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.limits.limit.map_π_assoc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limits_of_shape J C]
{G : J ⥤ C}
(α : F ⟶ G)
(j : J)
{X' : C}
(f' : G.obj j ⟶ X') :
category_theory.limits.lim.map α ≫ category_theory.limits.limit.π G j ≫ f' = category_theory.limits.limit.π F j ≫ α.app j ≫ f'
@[simp]
theorem
category_theory.limits.limit.map_π
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limits_of_shape J C]
{G : J ⥤ C}
(α : F ⟶ G)
(j : J) :
@[simp]
theorem
category_theory.limits.limit.lift_map
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limits_of_shape J C]
{G : J ⥤ C}
(α : F ⟶ G)
(c : category_theory.limits.cone F) :
theorem
category_theory.limits.limit.map_pre
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limits_of_shape J C]
{G : J ⥤ C}
(α : F ⟶ G)
[category_theory.limits.has_limits_of_shape K C]
(E : K ⥤ J) :
theorem
category_theory.limits.limit.map_pre'
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape J C]
[category_theory.limits.has_limits_of_shape K C]
(F : J ⥤ C)
{E₁ E₂ : K ⥤ J}
(α : E₁ ⟶ E₂) :
theorem
category_theory.limits.limit.id_pre
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape J C]
(F : J ⥤ C) :
theorem
category_theory.limits.limit.map_post
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_limits_of_shape J C]
{G : J ⥤ C}
(α : F ⟶ G)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_limits_of_shape J D]
(H : C ⥤ D) :
def
category_theory.limits.lim_yoneda
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape J C] :
The isomorphism between
morphisms from W to the cone point of the limit cone for F
and cones over F with cone point W
is natural in F.
Equations
- category_theory.limits.lim_yoneda = category_theory.nat_iso.of_components (λ (F : J ⥤ C), category_theory.nat_iso.of_components (λ (W : Cᵒᵖ), category_theory.limits.limit.hom_iso F (opposite.unop W)) _) category_theory.limits.lim_yoneda._proof_2
def
category_theory.limits.has_limits_of_shape_of_equivalence
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{J' : Type v}
[category_theory.small_category J']
(e : J ≌ J')
[category_theory.limits.has_limits_of_shape J C] :
We can transport chosen limits of shape J along an equivalence J ≌ J'.
Equations
@[class]
structure
category_theory.limits.has_colimit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C] :
J ⥤ C → Type (max u v)
- cocone : category_theory.limits.cocone F
- is_colimit : category_theory.limits.is_colimit category_theory.limits.has_colimit.cocone
has_colimit F represents a particular chosen colimit of the diagram F.
Instances
- category_theory.limits.has_colimit_of_has_colimits_of_shape
- category_theory.limits.has_coproduct_of_has_biproduct
- category_theory.limits.has_colimit_equivalence_comp
- category_theory.limits.has_binary_biproduct.has_colimit_pair
- category_theory.adjunction.has_colimit_comp_equivalence
- category_theory.over.has_colimit
@[class]
structure
category_theory.limits.has_colimits_of_shape
(J : Type v)
[category_theory.small_category J]
(C : Type u)
[category_theory.category C] :
Type (max u v)
- has_colimit : Π (F : J ⥤ C), category_theory.limits.has_colimit F
C has colimits of shape J if we have chosen a particular colimit of
every functor F : J ⥤ C.
Instances
- category_theory.limits.has_colimits_of_shape_of_has_colimits
- category_theory.limits.has_colimits_of_shape_of_has_finite_colimits
- category_theory.limits.has_colimits_of_shape_wide_pushout_shape
- category_theory.limits.has_colimits_of_shape_discrete
- category_theory.limits.functor_category_has_colimits_of_shape
- category_theory.over.has_colimits_of_shape
@[class]
structure
category_theory.limits.has_colimits
(C : Type u)
[category_theory.category C] :
Type (max u (v+1))
- has_colimits_of_shape : Π (J : Type ?) [𝒥 : category_theory.small_category J], category_theory.limits.has_colimits_of_shape J C
C has all (small) colimits if it has colimits of every shape.
Instances
- category_theory.limits.has_colimits_of_complete_lattice
- category_theory.limits.types.category_theory.limits.has_colimits
- CommRing.colimits.has_colimits_CommRing
- AddCommGroup.colimits.has_colimits_AddCommGroup
- Mon.colimits.has_colimits_Mon
- category_theory.limits.functor_category_has_colimits
- category_theory.over.has_colimits
- category_theory.limits.category_theory.limits.has_colimits
- Top.Top_has_colimits
@[instance]
def
category_theory.limits.has_colimit_of_has_colimits_of_shape
{C : Type u}
[category_theory.category C]
{J : Type v}
[category_theory.small_category J]
[H : category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ C) :
@[instance]
def
category_theory.limits.has_colimits_of_shape_of_has_colimits
{C : Type u}
[category_theory.category C]
{J : Type v}
[category_theory.small_category J]
[H : category_theory.limits.has_colimits C] :
def
category_theory.limits.colimit.cocone
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F] :
The chosen colimit cocone of a functor.
def
category_theory.limits.colimit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F] :
C
The chosen colimit object of a functor.
Equations
def
category_theory.limits.colimit.ι
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
(j : J) :
The coprojection from a value of the functor to the chosen colimit object.
Equations
@[simp]
theorem
category_theory.limits.colimit.cocone_ι
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
(j : J) :
@[simp]
theorem
category_theory.limits.colimit.w
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
{j j' : J}
(f : j ⟶ j') :
def
category_theory.limits.colimit.is_colimit
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F] :
Evidence that the chosen cocone is a colimit cocone.
def
category_theory.limits.colimit.desc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
(c : category_theory.limits.cocone F) :
The morphism from the chosen colimit object to the cone point of any other cocone.
Equations
@[simp]
theorem
category_theory.limits.colimit.is_colimit_desc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
(c : category_theory.limits.cocone F) :
@[simp]
theorem
category_theory.limits.colimit.ι_desc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
(c : category_theory.limits.cocone F)
(j : J) :
We have lots of lemmas describing how to simplify colimit.ι F j ≫ _,
and combined with colimit.ext we rely on these lemmas for many calculations.
However, since category.assoc is a @[simp] lemma, often expressions are
right associated, and it's hard to apply these lemmas about colimit.ι.
We thus use reassoc to define additional @[simp] lemmas, with an arbitrary extra morphism.
(see tactic/reassoc_axiom.lean)
@[simp]
theorem
category_theory.limits.colimit.ι_desc_assoc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
(c : category_theory.limits.cocone F)
(j : J)
{X' : C}
(f' : c.X ⟶ X') :
category_theory.limits.colimit.ι F j ≫ category_theory.limits.colimit.desc F c ≫ f' = c.ι.app j ≫ f'
def
category_theory.limits.colimit.cocone_morphism
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
(c : category_theory.limits.cocone F) :
The cocone morphism from the chosen colimit cocone to any cocone.
@[simp]
theorem
category_theory.limits.colimit.cocone_morphism_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
(c : category_theory.limits.cocone F) :
theorem
category_theory.limits.colimit.ι_cocone_morphism
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
(c : category_theory.limits.cocone F)
(j : J) :
@[simp]
theorem
category_theory.limits.colimit.comp_cocone_point_unique_up_to_iso_hom_assoc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_colimit c)
(j : J)
{X' : C}
(f' : c.X ⟶ X') :
category_theory.limits.colimit.ι F j ≫ ((category_theory.limits.colimit.is_colimit F).cocone_point_unique_up_to_iso hc).hom ≫ f' = c.ι.app j ≫ f'
@[simp]
theorem
category_theory.limits.colimit.comp_cocone_point_unique_up_to_iso_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_colimit c)
(j : J) :
@[simp]
theorem
category_theory.limits.colimit.comp_cocone_point_unique_up_to_iso_inv
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_colimit c)
(j : J) :
@[simp]
theorem
category_theory.limits.colimit.comp_cocone_point_unique_up_to_iso_inv_assoc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_colimit c)
(j : J)
{X' : C}
(f' : c.X ⟶ X') :
category_theory.limits.colimit.ι F j ≫ (hc.cocone_point_unique_up_to_iso (category_theory.limits.colimit.is_colimit F)).inv ≫ f' = c.ι.app j ≫ f'
@[ext]
theorem
category_theory.limits.colimit.hom_ext
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
{X : C}
{f f' : category_theory.limits.colimit F ⟶ X} :
(∀ (j : J), category_theory.limits.colimit.ι F j ≫ f = category_theory.limits.colimit.ι F j ≫ f') → f = f'
def
category_theory.limits.colimit.hom_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
(W : C) :
(category_theory.limits.colimit F ⟶ W) ≅ F.cocones.obj W
The isomorphism (in Type) between
morphisms from the colimit object to a specified object W,
and cocones with cone point W.
Equations
@[simp]
theorem
category_theory.limits.colimit.hom_iso_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
{W : C}
(f : category_theory.limits.colimit F ⟶ W) :
def
category_theory.limits.colimit.hom_iso'
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
(W : C) :
The isomorphism (in Type) between
morphisms from the colimit object to a specified object W,
and an explicit componentwise description of cocones with cone point W.
Equations
theorem
category_theory.limits.colimit.desc_extend
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
(c : category_theory.limits.cocone F)
{X : C}
(f : c.X ⟶ X) :
def
category_theory.limits.has_colimit_of_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimit F] :
(G ≅ F) → category_theory.limits.has_colimit G
If we've chosen a colimit for a functor F,
we can transport that choice across a natural isomorphism.
Equations
- category_theory.limits.has_colimit_of_iso α = {cocone := (category_theory.limits.cocones.precompose α.hom).obj (category_theory.limits.colimit.cocone F), is_colimit := {desc := λ (s : category_theory.limits.cocone G), category_theory.limits.colimit.desc F ((category_theory.limits.cocones.precompose α.inv).obj s), fac' := _, uniq' := _}}
def
category_theory.limits.has_colimit.of_cocones_iso
{C : Type u}
[category_theory.category C]
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
(F : J ⥤ C)
(G : K ⥤ C)
(h : F.cocones ≅ G.cocones)
[category_theory.limits.has_colimit F] :
If a functor G has the same collection of cocones as a functor F
which has a colimit, then G also has a colimit.
Equations
- category_theory.limits.has_colimit.of_cocones_iso F G h = {cocone := category_theory.limits.is_colimit.of_nat_iso.colimit_cocone ((category_theory.limits.colimit.is_colimit F).nat_iso ≪≫ h), is_colimit := category_theory.limits.is_colimit.of_nat_iso ((category_theory.limits.colimit.is_colimit F).nat_iso ≪≫ h)}
def
category_theory.limits.has_colimit.iso_of_nat_iso
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit G] :
(F ≅ G) → (category_theory.limits.colimit F ≅ category_theory.limits.colimit G)
The chosen colimits of F : J ⥤ C and G : J ⥤ C are isomorphic,
if the functors are naturally isomorphic.
@[simp]
theorem
category_theory.limits.has_colimit.iso_of_nat_iso_ι_hom_assoc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit G]
(w : F ≅ G)
(j : J)
{X' : C}
(f' : category_theory.limits.colimit G ⟶ X') :
category_theory.limits.colimit.ι F j ≫ (category_theory.limits.has_colimit.iso_of_nat_iso w).hom ≫ f' = w.hom.app j ≫ category_theory.limits.colimit.ι G j ≫ f'
@[simp]
theorem
category_theory.limits.has_colimit.iso_of_nat_iso_ι_hom
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit G]
(w : F ≅ G)
(j : J) :
def
category_theory.limits.has_colimit.iso_of_equivalence
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
{G : K ⥤ C}
[category_theory.limits.has_colimit G]
(e : J ≌ K) :
(e.functor ⋙ G ≅ F) → (category_theory.limits.colimit F ≅ category_theory.limits.colimit G)
The chosen colimits of F : J ⥤ C and G : K ⥤ C are isomorphic,
if there is an equivalence e : J ≌ K making the triangle commute up to natural isomorphism.
@[simp]
theorem
category_theory.limits.has_colimit.iso_of_equivalence_π
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimit F]
{G : K ⥤ C}
[category_theory.limits.has_colimit G]
(e : J ≌ K)
(w : e.functor ⋙ G ≅ F)
(j : J) :
def
category_theory.limits.colimit.pre
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
(E : K ⥤ J)
[category_theory.limits.has_colimit (E ⋙ F)] :
The canonical morphism
from the chosen colimit of E ⋙ F
to the chosen colimit of F.
Equations
- category_theory.limits.colimit.pre F E = category_theory.limits.colimit.desc (E ⋙ F) {X := category_theory.limits.colimit F _inst_4, ι := {app := λ (k : K), category_theory.limits.colimit.ι F (E.obj k), naturality' := _}}
@[simp]
theorem
category_theory.limits.colimit.ι_pre
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
(E : K ⥤ J)
[category_theory.limits.has_colimit (E ⋙ F)]
(k : K) :
category_theory.limits.colimit.ι (E ⋙ F) k ≫ category_theory.limits.colimit.pre F E = category_theory.limits.colimit.ι F (E.obj k)
@[simp]
theorem
category_theory.limits.colimit.ι_pre_assoc
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
(E : K ⥤ J)
[category_theory.limits.has_colimit (E ⋙ F)]
(k : K)
{X' : C}
(f' : category_theory.limits.colimit F ⟶ X') :
category_theory.limits.colimit.ι (E ⋙ F) k ≫ category_theory.limits.colimit.pre F E ≫ f' = category_theory.limits.colimit.ι F (E.obj k) ≫ f'
@[simp]
theorem
category_theory.limits.colimit.pre_desc
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
(E : K ⥤ J)
[category_theory.limits.has_colimit (E ⋙ F)]
(c : category_theory.limits.cocone F) :
@[simp]
theorem
category_theory.limits.colimit.pre_pre
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
[category_theory.limits.has_colimit F]
(E : K ⥤ J)
[category_theory.limits.has_colimit (E ⋙ F)]
{L : Type v}
[category_theory.small_category L]
(D : L ⥤ K)
[category_theory.limits.has_colimit (D ⋙ E ⋙ F)] :
def
category_theory.limits.colimit.post
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_colimit F]
(G : C ⥤ D)
[category_theory.limits.has_colimit (F ⋙ G)] :
The canonical morphism
from G applied to the chosen colimit of F ⋙ G
to G applied to the chosen colimit of F.
Equations
- category_theory.limits.colimit.post F G = category_theory.limits.colimit.desc (F ⋙ G) {X := G.obj (category_theory.limits.colimit F), ι := {app := λ (j : J), G.map (category_theory.limits.colimit.ι F j), naturality' := _}}
@[simp]
theorem
category_theory.limits.colimit.ι_post
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_colimit F]
(G : C ⥤ D)
[category_theory.limits.has_colimit (F ⋙ G)]
(j : J) :
@[simp]
theorem
category_theory.limits.colimit.ι_post_assoc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_colimit F]
(G : C ⥤ D)
[category_theory.limits.has_colimit (F ⋙ G)]
(j : J)
{X' : D}
(f' : G.obj (category_theory.limits.colimit F) ⟶ X') :
category_theory.limits.colimit.ι (F ⋙ G) j ≫ category_theory.limits.colimit.post F G ≫ f' = G.map (category_theory.limits.colimit.ι F j) ≫ f'
@[simp]
theorem
category_theory.limits.colimit.post_desc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_colimit F]
(G : C ⥤ D)
[category_theory.limits.has_colimit (F ⋙ G)]
(c : category_theory.limits.cocone F) :
category_theory.limits.colimit.post F G ≫ G.map (category_theory.limits.colimit.desc F c) = category_theory.limits.colimit.desc (F ⋙ G) (G.map_cocone c)
@[simp]
theorem
category_theory.limits.colimit.post_post
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
(F : J ⥤ C)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_colimit F]
(G : C ⥤ D)
[category_theory.limits.has_colimit (F ⋙ G)]
{E : Type u''}
[category_theory.category E]
(H : D ⥤ E)
[category_theory.limits.has_colimit ((F ⋙ G) ⋙ H)] :
category_theory.limits.colimit.post (F ⋙ G) H ≫ H.map (category_theory.limits.colimit.post F G) = category_theory.limits.colimit.post F (G ⋙ H)
theorem
category_theory.limits.colimit.pre_post
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
(E : K ⥤ J)
(F : J ⥤ C)
(G : C ⥤ D)
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit (E ⋙ F)]
[category_theory.limits.has_colimit (F ⋙ G)]
[category_theory.limits.has_colimit ((E ⋙ F) ⋙ G)] :
category_theory.limits.colimit.post (E ⋙ F) G ≫ G.map (category_theory.limits.colimit.pre F E) = category_theory.limits.colimit.pre (F ⋙ G) E ≫ category_theory.limits.colimit.post F G
@[instance]
def
category_theory.limits.has_colimit_equivalence_comp
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
(e : K ≌ J)
[category_theory.limits.has_colimit F] :
def
category_theory.limits.has_colimit_of_equivalence_comp
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
(e : K ≌ J)
[category_theory.limits.has_colimit (e.functor ⋙ F)] :
If a E ⋙ F has a chosen colimit, and E is an equivalence, we can construct a chosen colimit of F.
def
category_theory.limits.colim_map
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit G] :
(F ⟶ G) → (category_theory.limits.colimit F ⟶ category_theory.limits.colimit G)
Functoriality of colimits.
Usually this morphism should be accessed through colim.map,
but may be needed separately when you have specified colimits for the source and target functors,
but not necessarily for all functors of shape J.
Equations
- category_theory.limits.colim_map α = category_theory.limits.colimit.desc F {X := category_theory.limits.colimit G _inst_5, ι := {app := λ (j : J), α.app j ≫ category_theory.limits.colimit.ι G j, naturality' := _}}
@[simp]
theorem
category_theory.limits.ι_colim_map_assoc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit G]
(α : F ⟶ G)
(j : J)
{X' : C}
(f' : category_theory.limits.colimit G ⟶ X') :
category_theory.limits.colimit.ι F j ≫ category_theory.limits.colim_map α ≫ f' = α.app j ≫ category_theory.limits.colimit.ι G j ≫ f'
@[simp]
theorem
category_theory.limits.ι_colim_map
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F G : J ⥤ C}
[category_theory.limits.has_colimit F]
[category_theory.limits.has_colimit G]
(α : F ⟶ G)
(j : J) :
def
category_theory.limits.colim
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J C] :
colimit F is functorial in F, when C has all colimits of shape J.
Equations
- category_theory.limits.colim = {obj := λ (F : J ⥤ C), category_theory.limits.colimit F, map := λ (F G : J ⥤ C) (α : F ⟶ G), category_theory.limits.colim_map α, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.limits.colimit.ι_map
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimits_of_shape J C]
{G : J ⥤ C}
(α : F ⟶ G)
(j : J) :
@[simp]
theorem
category_theory.limits.colimit.ι_map_assoc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimits_of_shape J C]
{G : J ⥤ C}
(α : F ⟶ G)
(j : J)
{X' : C}
(f' : category_theory.limits.colim.obj G ⟶ X') :
category_theory.limits.colimit.ι F j ≫ category_theory.limits.colim.map α ≫ f' = α.app j ≫ category_theory.limits.colimit.ι G j ≫ f'
@[simp]
theorem
category_theory.limits.colimit.map_desc
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimits_of_shape J C]
{G : J ⥤ C}
(α : F ⟶ G)
(c : category_theory.limits.cocone G) :
theorem
category_theory.limits.colimit.pre_map
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimits_of_shape J C]
{G : J ⥤ C}
(α : F ⟶ G)
[category_theory.limits.has_colimits_of_shape K C]
(E : K ⥤ J) :
theorem
category_theory.limits.colimit.pre_map'
{J K : Type v}
[category_theory.small_category J]
[category_theory.small_category K]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J C]
[category_theory.limits.has_colimits_of_shape K C]
(F : J ⥤ C)
{E₁ E₂ : K ⥤ J}
(α : E₁ ⟶ E₂) :
theorem
category_theory.limits.colimit.pre_id
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J C]
(F : J ⥤ C) :
theorem
category_theory.limits.colimit.map_post
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{F : J ⥤ C}
[category_theory.limits.has_colimits_of_shape J C]
{G : J ⥤ C}
(α : F ⟶ G)
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_colimits_of_shape J D]
(H : C ⥤ D) :
def
category_theory.limits.colim_coyoneda
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape J C] :
The isomorphism between
morphisms from the cone point of the chosen colimit cocone for F to W
and cocones over F with cone point W
is natural in F.
Equations
- category_theory.limits.colim_coyoneda = category_theory.nat_iso.of_components (λ (F : (J ⥤ C)ᵒᵖ), category_theory.nat_iso.of_components (category_theory.limits.colimit.hom_iso (opposite.unop F)) _) category_theory.limits.colim_coyoneda._proof_2
def
category_theory.limits.has_colimits_of_shape_of_equivalence
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
{J' : Type v}
[category_theory.small_category J']
(e : J ≌ J')
[category_theory.limits.has_colimits_of_shape J C] :
We can transport chosen colimits of shape J along an equivalence J ≌ J'.