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ᵒᵖ
.
Instances For
Turn a limit for F : J ⥤ C
into a colimit for F.op : Jᵒᵖ ⥤ Cᵒᵖ
.
Instances For
Turn a colimit for F : J ⥤ Cᵒᵖ
into a limit for F.leftOp : Jᵒᵖ ⥤ C
.
Instances For
Turn a limit of F : J ⥤ Cᵒᵖ
into a colimit of F.leftOp : Jᵒᵖ ⥤ C
.
Instances For
Turn a colimit for F : Jᵒᵖ ⥤ C
into a limit for F.rightOp : J ⥤ Cᵒᵖ
.
Instances For
Turn a limit for F : Jᵒᵖ ⥤ C
into a colimit for F.rightOp : J ⥤ Cᵒᵖ
.
Instances For
Turn a colimit for F : Jᵒᵖ ⥤ Cᵒᵖ
into a limit for F.unop : J ⥤ C
.
Instances For
Turn a limit of F : Jᵒᵖ ⥤ Cᵒᵖ
into a colimit of F.unop : J ⥤ C
.
Instances For
Turn a colimit for F.op : Jᵒᵖ ⥤ Cᵒᵖ
into a limit for F : J ⥤ C
.
Instances For
Turn a limit for F.op : Jᵒᵖ ⥤ Cᵒᵖ
into a colimit for F : J ⥤ C
.
Instances For
Turn a colimit for F.leftOp : Jᵒᵖ ⥤ C
into a limit for F : J ⥤ Cᵒᵖ
.
Instances For
Turn a limit of F.leftOp : Jᵒᵖ ⥤ C
into a colimit of F : J ⥤ Cᵒᵖ
.
Instances For
Turn a colimit for F.rightOp : J ⥤ Cᵒᵖ
into a limit for F : Jᵒᵖ ⥤ C
.
Instances For
Turn a limit for F.rightOp : J ⥤ Cᵒᵖ
into a limit for F : Jᵒᵖ ⥤ C
.
Instances For
Turn a colimit for F.unop : J ⥤ C
into a limit for F : Jᵒᵖ ⥤ Cᵒᵖ
.
Instances For
Turn a limit for F.unop : J ⥤ C
into a colimit for F : Jᵒᵖ ⥤ Cᵒᵖ
.
Instances For
If F.leftOp : 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ᵒᵖ
.
If F.leftOp : 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ᵒᵖ
.
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
.
The isomorphism from the opposite of the coproduct to the product.
Instances For
The isomorphism from the opposite of the product to the coproduct.
Instances For
The canonical isomorphism relating Span f.op g.op
and (Cospan f g).op
Instances For
The canonical isomorphism relating (Cospan f g).op
and Span f.op g.op
Instances For
The canonical isomorphism relating Cospan f.op g.op
and (Span f g).op
Instances For
The canonical isomorphism relating (Span f g).op
and Cospan f.op g.op
Instances For
The obvious map PushoutCocone f g → PullbackCone f.unop g.unop
Instances For
The obvious map PushoutCocone f.op g.op → PullbackCone f g
Instances For
The obvious map PullbackCone f g → PushoutCocone f.unop g.unop
Instances For
The obvious map PullbackCone f g → PushoutCocone f.op g.op
Instances For
If c
is a pullback cone, then c.op.unop
is isomorphic to c
.
Instances For
If c
is a pullback cone in Cᵒᵖ
, then c.unop.op
is isomorphic to c
.
Instances For
If c
is a pushout cocone, then c.op.unop
is isomorphic to c
.
Instances For
If c
is a pushout cocone in Cᵒᵖ
, then c.unop.op
is isomorphic to c
.
Instances For
A pushout cone is a colimit cocone if and only if the corresponding pullback cone in the opposite category is a limit cone.
Instances For
A pushout cone is a colimit cocone in Cᵒᵖ
if and only if the corresponding pullback cone
in C
is a limit cone.
Instances For
A pullback cone is a limit cone if and only if the corresponding pushout cocone in the opposite category is a colimit cocone.
Instances For
A pullback cone is a limit cone in Cᵒᵖ
if and only if the corresponding pushout cocone
in C
is a colimit cocone.
Instances For
The pullback of f
and g
in C
is isomorphic to the pushout of
f.op
and g.op
in Cᵒᵖ
.
Instances For
The pushout of f
and g
in C
is isomorphic to the pullback of
f.op
and g.op
in Cᵒᵖ
.
Instances For
A colimit cokernel cofork gives a limit kernel fork in the opposite category
Instances For
A colimit cokernel cofork in the opposite category gives a limit kernel fork in the original category
Instances For
A limit kernel fork gives a colimit cokernel cofork in the opposite category
Instances For
A limit kernel fork in the opposite category gives a colimit cokernel cofork in the original category