theorem
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 colimit, we can construct a limit for F : J ⥤ Cᵒᵖ.
theorem
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 colimits of shape Jᵒᵖ, we can construct limits in Cᵒᵖ of shape J.
theorem
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 colimits, we can construct limits for Cᵒᵖ.
theorem
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 limit, we can construct a colimit for F : J ⥤ Cᵒᵖ.
theorem
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 colimits of shape Jᵒᵖ, we can construct limits in Cᵒᵖ of shape J.
theorem
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 limits, we can construct colimits for Cᵒᵖ.
theorem
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.
theorem
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.