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
is_limit c, forc : cone F,F : J ⥤ C, expressing thatcis a limit cone,
See also category_theory.limits.has_limits which further builds:
limit_cone F, which consists of a choice of cone forFand the fact it is a limit cone, andhas_limit 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 #
@[nolint]
structure
category_theory.limits.is_limit
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(t : category_theory.limits.cone F) :
Type (max u₁ u₃ v₃)
- lift : Π (s : category_theory.limits.cone F), s.X ⟶ t.X
- fac' : (∀ (s : category_theory.limits.cone F) (j : J), self.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 = self.lift s) . "obviously"
A cone t on F is a limit cone if each cone on F admits a unique
cone morphism to t.
See https://stacks.math.columbia.edu/tag/002E.
Instances for category_theory.limits.is_limit
- category_theory.limits.is_limit.has_sizeof_inst
- category_theory.limits.is_limit.subsingleton
@[simp]
theorem
category_theory.limits.is_limit.fac
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cone F}
(self : category_theory.limits.is_limit t)
(s : category_theory.limits.cone F)
(j : J) :
@[simp]
theorem
category_theory.limits.is_limit.fac_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cone F}
(self : category_theory.limits.is_limit t)
(s : category_theory.limits.cone F)
(j : J)
{X' : C}
(f' : F.obj j ⟶ X') :
theorem
category_theory.limits.is_limit.uniq
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cone F}
(self : category_theory.limits.is_limit t)
(s : category_theory.limits.cone F)
(m : s.X ⟶ t.X)
(w : ∀ (j : J), m ≫ t.π.app j = s.π.app j) :
@[protected, instance]
def
category_theory.limits.is_limit.subsingleton
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cone F} :
def
category_theory.limits.is_limit.map
{J : Type u₁}
[category_theory.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 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
@[simp]
theorem
category_theory.limits.is_limit.map_π
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(c : category_theory.limits.cone F)
{d : category_theory.limits.cone G}
(hd : category_theory.limits.is_limit d)
(α : F ⟶ G)
(j : J) :
@[simp]
theorem
category_theory.limits.is_limit.map_π_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(c : category_theory.limits.cone F)
{d : category_theory.limits.cone G}
(hd : category_theory.limits.is_limit d)
(α : F ⟶ G)
(j : J)
{X' : C}
(f' : G.obj j ⟶ X') :
theorem
category_theory.limits.is_limit.lift_self
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{c : category_theory.limits.cone F}
(t : category_theory.limits.is_limit c) :
def
category_theory.limits.is_limit.lift_cone_morphism
{J : Type u₁}
[category_theory.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 u₁}
[category_theory.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 u₁}
[category_theory.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'
theorem
category_theory.limits.is_limit.exists_unique
{J : Type u₁}
[category_theory.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) :
Restating the definition of a limit cone in terms of the ∃! operator.
noncomputable
def
category_theory.limits.is_limit.of_exists_unique
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cone F}
(ht : ∀ (s : category_theory.limits.cone F), ∃! (l : s.X ⟶ t.X), ∀ (j : J), l ≫ t.π.app j = s.π.app j) :
Noncomputably make a colimit cocone from the existence of unique factorizations.
Equations
- category_theory.limits.is_limit.of_exists_unique ht = (λ (_x : ∀ (s : category_theory.limits.cone F), (λ (l : s.X ⟶ t.X), ∀ (j : J), l ≫ t.π.app j = s.π.app j) ((λ (s : category_theory.limits.cone F), classical.some _) s) ∧ ∀ (y : s.X ⟶ t.X), (λ (l : s.X ⟶ t.X), ∀ (j : J), l ≫ t.π.app j = s.π.app j) y → y = (λ (s : category_theory.limits.cone F), classical.some _) s), {lift := λ (s : category_theory.limits.cone F), classical.some _, fac' := _, uniq' := _}) _
@[simp]
theorem
category_theory.limits.is_limit.mk_cone_morphism_lift
{J : Type u₁}
[category_theory.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)
(uniq' : ∀ (s : category_theory.limits.cone F) (m : s ⟶ t), m = lift s)
(s : category_theory.limits.cone F) :
(category_theory.limits.is_limit.mk_cone_morphism lift uniq').lift s = (lift s).hom
def
category_theory.limits.is_limit.mk_cone_morphism
{J : Type u₁}
[category_theory.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)
(uniq' : ∀ (s : category_theory.limits.cone F) (m : s ⟶ t), m = lift s) :
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 u₁}
[category_theory.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 u₁}
[category_theory.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) :
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 u₁}
[category_theory.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
theorem
category_theory.limits.is_limit.hom_is_iso
{J : Type u₁}
[category_theory.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.
def
category_theory.limits.is_limit.cone_point_unique_up_to_iso
{J : Type u₁}
[category_theory.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) :
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 u₁}
[category_theory.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 u₁}
[category_theory.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
{J : Type u₁}
[category_theory.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 u₁}
[category_theory.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.lift_comp_cone_point_unique_up_to_iso_hom_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{r s t : category_theory.limits.cone F}
(P : category_theory.limits.is_limit s)
(Q : category_theory.limits.is_limit t)
{X' : C}
(f' : t.X ⟶ X') :
@[simp]
theorem
category_theory.limits.is_limit.lift_comp_cone_point_unique_up_to_iso_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{r s t : category_theory.limits.cone F}
(P : category_theory.limits.is_limit s)
(Q : category_theory.limits.is_limit t) :
@[simp]
theorem
category_theory.limits.is_limit.lift_comp_cone_point_unique_up_to_iso_inv_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{r s t : category_theory.limits.cone F}
(P : category_theory.limits.is_limit s)
(Q : category_theory.limits.is_limit t)
{X' : C}
(f' : s.X ⟶ X') :
@[simp]
theorem
category_theory.limits.is_limit.lift_comp_cone_point_unique_up_to_iso_inv
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{r s t : category_theory.limits.cone F}
(P : category_theory.limits.is_limit s)
(Q : category_theory.limits.is_limit t) :
def
category_theory.limits.is_limit.of_iso_limit
{J : Type u₁}
[category_theory.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 : r ≅ 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) _
@[simp]
theorem
category_theory.limits.is_limit.of_iso_limit_lift
{J : Type u₁}
[category_theory.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 : r ≅ t)
(s : category_theory.limits.cone F) :
def
category_theory.limits.is_limit.equiv_iso_limit
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{r t : category_theory.limits.cone F}
(i : r ≅ t) :
Isomorphism of cones preserves whether or not they are limiting cones.
Equations
- category_theory.limits.is_limit.equiv_iso_limit i = {to_fun := λ (h : category_theory.limits.is_limit r), h.of_iso_limit i, inv_fun := λ (h : category_theory.limits.is_limit t), h.of_iso_limit i.symm, left_inv := _, right_inv := _}
@[simp]
theorem
category_theory.limits.is_limit.equiv_iso_limit_apply
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{r t : category_theory.limits.cone F}
(i : r ≅ t)
(P : category_theory.limits.is_limit r) :
@[simp]
theorem
category_theory.limits.is_limit.equiv_iso_limit_symm_apply
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{r t : category_theory.limits.cone F}
(i : r ≅ t)
(P : category_theory.limits.is_limit t) :
noncomputable
def
category_theory.limits.is_limit.of_point_iso
{J : Type u₁}
[category_theory.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 u₁}
[category_theory.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 u₁}
[category_theory.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}
(w : ∀ (j : J), f ≫ t.π.app j = f' ≫ t.π.app j) :
f = f'
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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.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}
(t : category_theory.limits.is_limit c) :
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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.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 := _}
@[simp]
theorem
category_theory.limits.is_limit.of_cone_equiv_apply_desc
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.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}
(P : category_theory.limits.is_limit (h.functor.obj c))
(s : category_theory.limits.cone G) :
@[simp]
theorem
category_theory.limits.is_limit.of_cone_equiv_symm_apply_desc
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.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}
(P : category_theory.limits.is_limit c)
(s : category_theory.limits.cone F) :
def
category_theory.limits.is_limit.postcompose_hom_equiv
{J : Type u₁}
[category_theory.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 u₁}
[category_theory.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.equiv_of_nat_iso_of_iso
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(α : F ≅ G)
(c : category_theory.limits.cone F)
(d : category_theory.limits.cone G)
(w : (category_theory.limits.cones.postcompose α.hom).obj c ≅ d) :
Constructing an equivalence is_limit c ≃ is_limit d from a natural isomorphism
between the underlying functors, and then an isomorphism between c transported along this and d.
def
category_theory.limits.is_limit.cone_points_iso_of_nat_iso
{J : Type u₁}
[category_theory.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) :
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 := category_theory.limits.is_limit.map s Q w.hom, inv := category_theory.limits.is_limit.map t P w.inv, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.is_limit.cone_points_iso_of_nat_iso_hom
{J : Type u₁}
[category_theory.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 = category_theory.limits.is_limit.map s Q w.hom
@[simp]
theorem
category_theory.limits.is_limit.cone_points_iso_of_nat_iso_inv
{J : Type u₁}
[category_theory.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 = category_theory.limits.is_limit.map t P w.inv
theorem
category_theory.limits.is_limit.cone_points_iso_of_nat_iso_hom_comp_assoc
{J : Type u₁}
[category_theory.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)
(j : J)
{X' : C}
(f' : G.obj j ⟶ X') :
theorem
category_theory.limits.is_limit.cone_points_iso_of_nat_iso_hom_comp
{J : Type u₁}
[category_theory.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)
(j : J) :
theorem
category_theory.limits.is_limit.cone_points_iso_of_nat_iso_inv_comp
{J : Type u₁}
[category_theory.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)
(j : J) :
theorem
category_theory.limits.is_limit.cone_points_iso_of_nat_iso_inv_comp_assoc
{J : Type u₁}
[category_theory.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)
(j : J)
{X' : C}
(f' : F.obj j ⟶ X') :
theorem
category_theory.limits.is_limit.lift_comp_cone_points_iso_of_nat_iso_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
{r 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.lift r ≫ (P.cone_points_iso_of_nat_iso Q w).hom = category_theory.limits.is_limit.map r Q w.hom
theorem
category_theory.limits.is_limit.lift_comp_cone_points_iso_of_nat_iso_hom_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
{r 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)
{X' : C}
(f' : t.X ⟶ X') :
P.lift r ≫ (P.cone_points_iso_of_nat_iso Q w).hom ≫ f' = category_theory.limits.is_limit.map r Q w.hom ≫ f'
theorem
category_theory.limits.is_limit.lift_comp_cone_points_iso_of_nat_iso_inv_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
{r s : category_theory.limits.cone G}
{t : category_theory.limits.cone F}
(P : category_theory.limits.is_limit t)
(Q : category_theory.limits.is_limit s)
(w : F ≅ G)
{X' : C}
(f' : t.X ⟶ X') :
Q.lift r ≫ (P.cone_points_iso_of_nat_iso Q w).inv ≫ f' = category_theory.limits.is_limit.map r P w.inv ≫ f'
theorem
category_theory.limits.is_limit.lift_comp_cone_points_iso_of_nat_iso_inv
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
{r s : category_theory.limits.cone G}
{t : category_theory.limits.cone F}
(P : category_theory.limits.is_limit t)
(Q : category_theory.limits.is_limit s)
(w : F ≅ G) :
Q.lift r ≫ (P.cone_points_iso_of_nat_iso Q w).inv = category_theory.limits.is_limit.map r P w.inv
def
category_theory.limits.is_limit.whisker_equivalence
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.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.of_whisker_equivalence
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{s : category_theory.limits.cone F}
(e : K ≌ J)
(P : category_theory.limits.is_limit (category_theory.limits.cone.whisker e.functor s)) :
If s : cone F whiskered by an equivalence e is a limit cone, so is s.
Equations
- category_theory.limits.is_limit.of_whisker_equivalence e P = ⇑(category_theory.limits.is_limit.equiv_iso_limit ((category_theory.limits.cones.whiskering_equivalence e).unit_iso.app s).symm) (category_theory.limits.is_limit.of_right_adjoint (category_theory.limits.cones.whiskering_equivalence e).inverse P)
def
category_theory.limits.is_limit.whisker_equivalence_equiv
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{s : category_theory.limits.cone F}
(e : K ≌ J) :
Given an equivalence of diagrams e, s is a limit cone iff s.whisker e.functor is.
Equations
@[simp]
theorem
category_theory.limits.is_limit.cone_points_iso_of_equivalence_hom
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.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.cone_points_iso_of_equivalence
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.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) :
We can prove two cone points (s : cone F).X and (t.cone G).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' := _}
def
category_theory.limits.is_limit.hom_iso
{J : Type u₁}
[category_theory.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 u₁}
[category_theory.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 : ulift (W ⟶ t.X)) :
def
category_theory.limits.is_limit.nat_iso
{J : Type u₁}
[category_theory.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) :
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 u₁}
[category_theory.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 u₁}
[category_theory.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)
(h : ∀ (s : category_theory.limits.cone F), G.map (lift s) = ht.lift (G.map_cone s)) :
If G : C → D is a faithful functor which sends t to a limit cone, then it suffices to check that the induced maps for the image of t can be lifted to maps of C.
def
category_theory.limits.is_limit.map_cone_equiv
{J : Type u₁}
[category_theory.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}
(t : category_theory.limits.is_limit (F.map_cone c)) :
If F and G are naturally isomorphic, then F.map_cone c being a limit implies
G.map_cone c is also a limit.
def
category_theory.limits.is_limit.iso_unique_cone_morphism
{J : Type u₁}
[category_theory.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.hom, fac' := _, uniq' := _}, hom_inv_id' := _, inv_hom_id' := _}
def
category_theory.limits.is_limit.of_nat_iso.cone_of_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.yoneda.obj X ⋙ category_theory.ulift_functor ≅ F.cones)
{Y : C}
(f : Y ⟶ X) :
If F.cones is represented by X, each morphism f : Y ⟶ X gives a cone with cone point
Y.
Equations
- category_theory.limits.is_limit.of_nat_iso.cone_of_hom h f = {X := Y, π := h.hom.app (opposite.op Y) {down := f}}
def
category_theory.limits.is_limit.of_nat_iso.hom_of_cone
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.yoneda.obj X ⋙ category_theory.ulift_functor ≅ 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
- category_theory.limits.is_limit.of_nat_iso.hom_of_cone h s = (h.inv.app (opposite.op s.X) s.π).down
@[simp]
theorem
category_theory.limits.is_limit.of_nat_iso.cone_of_hom_of_cone
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.yoneda.obj X ⋙ category_theory.ulift_functor ≅ 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 u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.yoneda.obj X ⋙ category_theory.ulift_functor ≅ F.cones)
{Y : C}
(f : Y ⟶ X) :
def
category_theory.limits.is_limit.of_nat_iso.limit_cone
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.yoneda.obj X ⋙ category_theory.ulift_functor ≅ F.cones) :
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 u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.yoneda.obj X ⋙ category_theory.ulift_functor ≅ 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 u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.yoneda.obj X ⋙ category_theory.ulift_functor ≅ 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 u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.yoneda.obj X ⋙ category_theory.ulift_functor ≅ 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 u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
(t : category_theory.limits.cocone F) :
Type (max u₁ 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 ≫ self.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 = self.desc s) . "obviously"
A cocone t on F is a colimit cocone if each cocone on F admits a unique
cocone morphism from t.
See https://stacks.math.columbia.edu/tag/002F.
Instances for category_theory.limits.is_colimit
- category_theory.limits.is_colimit.has_sizeof_inst
- category_theory.limits.is_colimit.subsingleton
@[simp]
theorem
category_theory.limits.is_colimit.fac
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cocone F}
(self : category_theory.limits.is_colimit t)
(s : category_theory.limits.cocone F)
(j : J) :
@[simp]
theorem
category_theory.limits.is_colimit.fac_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cocone F}
(self : category_theory.limits.is_colimit t)
(s : category_theory.limits.cocone F)
(j : J)
{X' : C}
(f' : s.X ⟶ X') :
theorem
category_theory.limits.is_colimit.uniq
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cocone F}
(self : category_theory.limits.is_colimit t)
(s : category_theory.limits.cocone F)
(m : t.X ⟶ s.X)
(w : ∀ (j : J), t.ι.app j ≫ m = s.ι.app j) :
@[protected, instance]
def
category_theory.limits.is_colimit.subsingleton
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cocone F} :
def
category_theory.limits.is_colimit.map
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
{s : category_theory.limits.cocone F}
(P : category_theory.limits.is_colimit s)
(t : category_theory.limits.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 ((category_theory.limits.cocones.precompose α).obj t)
@[simp]
theorem
category_theory.limits.is_colimit.ι_map_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_colimit c)
(d : category_theory.limits.cocone G)
(α : F ⟶ G)
(j : J)
{X' : C}
(f' : d.X ⟶ X') :
@[simp]
theorem
category_theory.limits.is_colimit.ι_map
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_colimit c)
(d : category_theory.limits.cocone G)
(α : F ⟶ G)
(j : J) :
@[simp]
theorem
category_theory.limits.is_colimit.desc_self
{J : Type u₁}
[category_theory.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) :
def
category_theory.limits.is_colimit.desc_cocone_morphism
{J : Type u₁}
[category_theory.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 cocone.
@[simp]
theorem
category_theory.limits.is_colimit.desc_cocone_morphism_hom
{J : Type u₁}
[category_theory.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 u₁}
[category_theory.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'
theorem
category_theory.limits.is_colimit.exists_unique
{J : Type u₁}
[category_theory.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) :
Restating the definition of a colimit cocone in terms of the ∃! operator.
noncomputable
def
category_theory.limits.is_colimit.of_exists_unique
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{t : category_theory.limits.cocone F}
(ht : ∀ (s : category_theory.limits.cocone F), ∃! (d : t.X ⟶ s.X), ∀ (j : J), t.ι.app j ≫ d = s.ι.app j) :
Noncomputably make a colimit cocone from the existence of unique factorizations.
Equations
- category_theory.limits.is_colimit.of_exists_unique ht = (λ (_x : ∀ (s : category_theory.limits.cocone F), (λ (d : t.X ⟶ s.X), ∀ (j : J), t.ι.app j ≫ d = s.ι.app j) ((λ (s : category_theory.limits.cocone F), classical.some _) s) ∧ ∀ (y : t.X ⟶ s.X), (λ (d : t.X ⟶ s.X), ∀ (j : J), t.ι.app j ≫ d = s.ι.app j) y → y = (λ (s : category_theory.limits.cocone F), classical.some _) s), {desc := λ (s : category_theory.limits.cocone F), classical.some _, fac' := _, uniq' := _}) _
def
category_theory.limits.is_colimit.mk_cocone_morphism
{J : Type u₁}
[category_theory.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)
(uniq' : ∀ (s : category_theory.limits.cocone F) (m : t ⟶ s), m = desc s) :
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' := _}
@[simp]
theorem
category_theory.limits.is_colimit.mk_cocone_morphism_desc
{J : Type u₁}
[category_theory.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)
(uniq' : ∀ (s : category_theory.limits.cocone F) (m : t ⟶ s), m = desc s)
(s : category_theory.limits.cocone F) :
(category_theory.limits.is_colimit.mk_cocone_morphism desc uniq').desc s = (desc s).hom
@[simp]
theorem
category_theory.limits.is_colimit.unique_up_to_iso_hom
{J : Type u₁}
[category_theory.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
def
category_theory.limits.is_colimit.unique_up_to_iso
{J : Type u₁}
[category_theory.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) :
s ≅ t
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_inv
{J : Type u₁}
[category_theory.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
theorem
category_theory.limits.is_colimit.hom_is_iso
{J : Type u₁}
[category_theory.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.
def
category_theory.limits.is_colimit.cocone_point_unique_up_to_iso
{J : Type u₁}
[category_theory.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) :
Colimits of F are unique up to isomorphism.
Equations
@[simp]
theorem
category_theory.limits.is_colimit.comp_cocone_point_unique_up_to_iso_hom_assoc
{J : Type u₁}
[category_theory.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_hom
{J : Type u₁}
[category_theory.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_inv
{J : Type u₁}
[category_theory.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_inv_assoc
{J : Type u₁}
[category_theory.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.cocone_point_unique_up_to_iso_hom_desc
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{r s t : category_theory.limits.cocone F}
(P : category_theory.limits.is_colimit s)
(Q : category_theory.limits.is_colimit t) :
@[simp]
theorem
category_theory.limits.is_colimit.cocone_point_unique_up_to_iso_hom_desc_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{r s t : category_theory.limits.cocone F}
(P : category_theory.limits.is_colimit s)
(Q : category_theory.limits.is_colimit t)
{X' : C}
(f' : r.X ⟶ X') :
@[simp]
theorem
category_theory.limits.is_colimit.cocone_point_unique_up_to_iso_inv_desc_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{r s t : category_theory.limits.cocone F}
(P : category_theory.limits.is_colimit s)
(Q : category_theory.limits.is_colimit t)
{X' : C}
(f' : r.X ⟶ X') :
@[simp]
theorem
category_theory.limits.is_colimit.cocone_point_unique_up_to_iso_inv_desc
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{r s t : category_theory.limits.cocone F}
(P : category_theory.limits.is_colimit s)
(Q : category_theory.limits.is_colimit t) :
def
category_theory.limits.is_colimit.of_iso_colimit
{J : Type u₁}
[category_theory.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 : r ≅ t) :
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) _
@[simp]
theorem
category_theory.limits.is_colimit.of_iso_colimit_desc
{J : Type u₁}
[category_theory.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 : r ≅ t)
(s : category_theory.limits.cocone F) :
def
category_theory.limits.is_colimit.equiv_iso_colimit
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{r t : category_theory.limits.cocone F}
(i : r ≅ t) :
Isomorphism of cocones preserves whether or not they are colimiting cocones.
Equations
- category_theory.limits.is_colimit.equiv_iso_colimit i = {to_fun := λ (h : category_theory.limits.is_colimit r), h.of_iso_colimit i, inv_fun := λ (h : category_theory.limits.is_colimit t), h.of_iso_colimit i.symm, left_inv := _, right_inv := _}
@[simp]
theorem
category_theory.limits.is_colimit.equiv_iso_colimit_apply
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{r t : category_theory.limits.cocone F}
(i : r ≅ t)
(P : category_theory.limits.is_colimit r) :
@[simp]
theorem
category_theory.limits.is_colimit.equiv_iso_colimit_symm_apply
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{r t : category_theory.limits.cocone F}
(i : r ≅ t)
(P : category_theory.limits.is_colimit t) :
noncomputable
def
category_theory.limits.is_colimit.of_point_iso
{J : Type u₁}
[category_theory.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 u₁}
[category_theory.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 u₁}
[category_theory.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}
(w : ∀ (j : J), t.ι.app j ≫ f = t.ι.app j ≫ f') :
f = f'
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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.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}
(t : category_theory.limits.is_colimit c) :
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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.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 := _}
@[simp]
theorem
category_theory.limits.is_colimit.of_cocone_equiv_apply_desc
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.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}
(P : category_theory.limits.is_colimit (h.functor.obj c))
(s : category_theory.limits.cocone G) :
@[simp]
theorem
category_theory.limits.is_colimit.of_cocone_equiv_symm_apply_desc
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.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}
(P : category_theory.limits.is_colimit c)
(s : category_theory.limits.cocone F) :
def
category_theory.limits.is_colimit.precompose_hom_equiv
{J : Type u₁}
[category_theory.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 u₁}
[category_theory.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.
def
category_theory.limits.is_colimit.equiv_of_nat_iso_of_iso
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
(α : F ≅ G)
(c : category_theory.limits.cocone F)
(d : category_theory.limits.cocone G)
(w : (category_theory.limits.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
category_theory.limits.is_colimit.cocone_points_iso_of_nat_iso
{J : Type u₁}
[category_theory.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) :
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.map t w.hom, inv := Q.map s w.inv, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.is_colimit.cocone_points_iso_of_nat_iso_inv
{J : Type u₁}
[category_theory.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.map s w.inv
@[simp]
theorem
category_theory.limits.is_colimit.cocone_points_iso_of_nat_iso_hom
{J : Type u₁}
[category_theory.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.map t w.hom
theorem
category_theory.limits.is_colimit.comp_cocone_points_iso_of_nat_iso_hom
{J : Type u₁}
[category_theory.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)
(j : J) :
theorem
category_theory.limits.is_colimit.comp_cocone_points_iso_of_nat_iso_hom_assoc
{J : Type u₁}
[category_theory.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)
(j : J)
{X' : C}
(f' : t.X ⟶ X') :
theorem
category_theory.limits.is_colimit.comp_cocone_points_iso_of_nat_iso_inv_assoc
{J : Type u₁}
[category_theory.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)
(j : J)
{X' : C}
(f' : s.X ⟶ X') :
theorem
category_theory.limits.is_colimit.comp_cocone_points_iso_of_nat_iso_inv
{J : Type u₁}
[category_theory.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)
(j : J) :
theorem
category_theory.limits.is_colimit.cocone_points_iso_of_nat_iso_hom_desc_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
{s : category_theory.limits.cocone F}
{r t : category_theory.limits.cocone G}
(P : category_theory.limits.is_colimit s)
(Q : category_theory.limits.is_colimit t)
(w : F ≅ G)
{X' : C}
(f' : r.X ⟶ X') :
theorem
category_theory.limits.is_colimit.cocone_points_iso_of_nat_iso_hom_desc
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
{s : category_theory.limits.cocone F}
{r t : category_theory.limits.cocone G}
(P : category_theory.limits.is_colimit s)
(Q : category_theory.limits.is_colimit t)
(w : F ≅ G) :
theorem
category_theory.limits.is_colimit.cocone_points_iso_of_nat_iso_inv_desc_assoc
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
{s : category_theory.limits.cocone G}
{r t : category_theory.limits.cocone F}
(P : category_theory.limits.is_colimit t)
(Q : category_theory.limits.is_colimit s)
(w : F ≅ G)
{X' : C}
(f' : r.X ⟶ X') :
theorem
category_theory.limits.is_colimit.cocone_points_iso_of_nat_iso_inv_desc
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F G : J ⥤ C}
{s : category_theory.limits.cocone G}
{r t : category_theory.limits.cocone F}
(P : category_theory.limits.is_colimit t)
(Q : category_theory.limits.is_colimit s)
(w : F ≅ G) :
def
category_theory.limits.is_colimit.whisker_equivalence
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.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 : cocone F is a colimit cocone, so is s whiskered by an equivalence e.
def
category_theory.limits.is_colimit.of_whisker_equivalence
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{s : category_theory.limits.cocone F}
(e : K ≌ J)
(P : category_theory.limits.is_colimit (category_theory.limits.cocone.whisker e.functor s)) :
If s : cocone F whiskered by an equivalence e is a colimit cocone, so is s.
Equations
- category_theory.limits.is_colimit.of_whisker_equivalence e P = ⇑(category_theory.limits.is_colimit.equiv_iso_colimit ((category_theory.limits.cocones.whiskering_equivalence e).unit_iso.app s).symm) (category_theory.limits.is_colimit.of_left_adjoint (category_theory.limits.cocones.whiskering_equivalence e).inverse P)
def
category_theory.limits.is_colimit.whisker_equivalence_equiv
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.category K]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{s : category_theory.limits.cocone F}
(e : K ≌ J) :
Given an equivalence of diagrams e, s is a colimit cocone iff s.whisker e.functor is.
Equations
@[simp]
theorem
category_theory.limits.is_colimit.cocone_points_iso_of_equivalence_hom
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.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)
@[simp]
theorem
category_theory.limits.is_colimit.cocone_points_iso_of_equivalence_inv
{J : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.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 : Type u₁}
[category_theory.category J]
{K : Type u₂}
[category_theory.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) :
We can prove two cocone points (s : cocone F).X and (t.cocone G).X 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
- 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' := _}
def
category_theory.limits.is_colimit.hom_iso
{J : Type u₁}
[category_theory.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 u₁}
[category_theory.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 : ulift (t.X ⟶ W)) :
def
category_theory.limits.is_colimit.nat_iso
{J : Type u₁}
[category_theory.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) :
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 u₁}
[category_theory.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 u₁}
[category_theory.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)
(h : ∀ (s : category_theory.limits.cocone F), G.map (desc s) = ht.desc (G.map_cocone 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.
def
category_theory.limits.is_colimit.map_cocone_equiv
{J : Type u₁}
[category_theory.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.cocone K}
(t : category_theory.limits.is_colimit (F.map_cocone c)) :
If F and G are naturally isomorphic, then F.map_cone c being a colimit implies
G.map_cone c is also a colimit.
def
category_theory.limits.is_colimit.iso_unique_cocone_morphism
{J : Type u₁}
[category_theory.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.hom, fac' := _, uniq' := _}, hom_inv_id' := _, inv_hom_id' := _}
def
category_theory.limits.is_colimit.of_nat_iso.cocone_of_hom
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.coyoneda.obj (opposite.op X) ⋙ category_theory.ulift_functor ≅ F.cocones)
{Y : C}
(f : X ⟶ Y) :
If F.cocones is corepresented by X, each morphism f : X ⟶ Y gives a cocone with cone
point Y.
def
category_theory.limits.is_colimit.of_nat_iso.hom_of_cocone
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.coyoneda.obj (opposite.op X) ⋙ category_theory.ulift_functor ≅ 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 u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.coyoneda.obj (opposite.op X) ⋙ category_theory.ulift_functor ≅ 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 u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.coyoneda.obj (opposite.op X) ⋙ category_theory.ulift_functor ≅ F.cocones)
{Y : C}
(f : X ⟶ Y) :
def
category_theory.limits.is_colimit.of_nat_iso.colimit_cocone
{J : Type u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.coyoneda.obj (opposite.op X) ⋙ category_theory.ulift_functor ≅ F.cocones) :
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 u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.coyoneda.obj (opposite.op X) ⋙ category_theory.ulift_functor ≅ 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 u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.coyoneda.obj (opposite.op X) ⋙ category_theory.ulift_functor ≅ 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 u₁}
[category_theory.category J]
{C : Type u₃}
[category_theory.category C]
{F : J ⥤ C}
{X : C}
(h : category_theory.coyoneda.obj (opposite.op X) ⋙ category_theory.ulift_functor ≅ 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' := _}