# mathlibdocumentation

category_theory.limits.opposites

theorem category_theory.limits.has_limit_of_has_colimit_left_op {C : Type u} {J : Type v} (F : J Cᵒᵖ)  :

If F.left_op : Jᵒᵖ ⥤ C has a colimit, we can construct a limit for F : J ⥤ Cᵒᵖ.

If C has colimits of shape Jᵒᵖ, we can construct limits in Cᵒᵖ of shape J.

If C has colimits, we can construct limits for Cᵒᵖ.

theorem category_theory.limits.has_colimit_of_has_limit_left_op {C : Type u} {J : Type v} (F : J Cᵒᵖ)  :

If F.left_op : Jᵒᵖ ⥤ C has a limit, we can construct a colimit for F : J ⥤ Cᵒᵖ.

If C has colimits of shape Jᵒᵖ, we can construct limits in Cᵒᵖ of shape J.

If C has limits, we can construct colimits for Cᵒᵖ.

theorem category_theory.limits.has_coproducts_opposite {C : Type u} (X : Type v)  :

If C has products indexed by X, then Cᵒᵖ has coproducts indexed by X.

theorem category_theory.limits.has_products_opposite {C : Type u} (X : Type v)  :

If C has coproducts indexed by X, then Cᵒᵖ has products indexed by X.