def
category_theory.limits.has_limit_of_has_colimit_left_op
{C : Type u}
[category_theory.category C]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ Cᵒᵖ)
[category_theory.limits.has_colimit F.left_op] :
If F.left_op : Jᵒᵖ ⥤ C has a chosen colimit, we can construct a chosen limit for F : J ⥤ Cᵒᵖ.
Equations
- category_theory.limits.has_limit_of_has_colimit_left_op F = {cone := category_theory.limits.cone_of_cocone_left_op (category_theory.limits.colimit.cocone F.left_op), is_limit := {lift := λ (s : category_theory.limits.cone F), (category_theory.limits.colimit.desc F.left_op (category_theory.limits.cocone_left_op_of_cone s)).op, fac' := _, uniq' := _}}
def
category_theory.limits.has_limits_of_shape_op_of_has_colimits_of_shape
{C : Type u}
[category_theory.category C]
{J : Type v}
[category_theory.small_category J]
[category_theory.limits.has_colimits_of_shape Jᵒᵖ C] :
If C has chosen colimits of shape Jᵒᵖ, we can construct chosen limits in Cᵒᵖ of shape J.
def
category_theory.limits.has_limits_op_of_has_colimits
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits C] :
If C has chosen colimits, we can construct chosen limits for Cᵒᵖ.
def
category_theory.limits.has_colimit_of_has_limit_left_op
{C : Type u}
[category_theory.category C]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ Cᵒᵖ)
[category_theory.limits.has_limit F.left_op] :
If F.left_op : Jᵒᵖ ⥤ C has a chosen limit, we can construct a chosen colimit for F : J ⥤ Cᵒᵖ.
Equations
- category_theory.limits.has_colimit_of_has_limit_left_op F = {cocone := category_theory.limits.cocone_of_cone_left_op (category_theory.limits.limit.cone F.left_op), is_colimit := {desc := λ (s : category_theory.limits.cocone F), (category_theory.limits.limit.lift F.left_op (category_theory.limits.cone_left_op_of_cocone s)).op, fac' := _, uniq' := _}}
def
category_theory.limits.has_colimits_of_shape_op_of_has_limits_of_shape
{C : Type u}
[category_theory.category C]
{J : Type v}
[category_theory.small_category J]
[category_theory.limits.has_limits_of_shape Jᵒᵖ C] :
If C has chosen colimits of shape Jᵒᵖ, we can construct chosen limits in Cᵒᵖ of shape J.
def
category_theory.limits.has_colimits_op_of_has_limits
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C] :
If C has chosen limits, we can construct chosen colimits for Cᵒᵖ.
def
category_theory.limits.has_coproducts_opposite
{C : Type u}
[category_theory.category C]
(X : Type v)
[category_theory.limits.has_products_of_shape X C] :
If C has products indexed by X, then Cᵒᵖ has coproducts indexed by X.
def
category_theory.limits.has_products_opposite
{C : Type u}
[category_theory.category C]
(X : Type v)
[category_theory.limits.has_coproducts_of_shape X C] :
If C has coproducts indexed by X, then Cᵒᵖ has products indexed by X.