mathlib documentation

category_theory.limits.opposites

Limits in C give colimits in Cᵒᵖ. #

We also give special cases for (co)products, but not yet for pullbacks / pushouts or for (co)equalizers.

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

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

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

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