mathlib documentation

category_theory.limits.opposites

Limits in C give colimits in Cᵒᵖ. #

We also give special cases for (co)products, (co)equalizers, and pullbacks / pushouts.

Turn a colimit for F : J ⥤ C into a limit for F.op : Jᵒᵖ ⥤ Cᵒᵖ.

Equations

Turn a limit for F : J ⥤ C into a colimit for F.op : Jᵒᵖ ⥤ Cᵒᵖ.

Equations

Turn a colimit for F.op : Jᵒᵖ ⥤ Cᵒᵖ into a limit for F : J ⥤ C.

Equations

Turn a limit for F.op : Jᵒᵖ ⥤ Cᵒᵖ into a colimit for F : J ⥤ C.

Equations

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 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 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.