Limits in C
give colimits in Cᵒᵖ
. #
We construct limits and colimits in the opposite categories.
Turn a colimit for F : J ⥤ Cᵒᵖ
into a limit for F.leftOp : Jᵒᵖ ⥤ C
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Turn a limit of F : J ⥤ Cᵒᵖ
into a colimit of F.leftOp : Jᵒᵖ ⥤ C
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Turn a colimit for F : Jᵒᵖ ⥤ C
into a limit for F.rightOp : J ⥤ Cᵒᵖ
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Turn a limit for F : Jᵒᵖ ⥤ C
into a colimit for F.rightOp : J ⥤ Cᵒᵖ
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Turn a colimit for F : Jᵒᵖ ⥤ Cᵒᵖ
into a limit for F.unop : J ⥤ C
.
Equations
- CategoryTheory.Limits.isLimitConeUnopOfCocone F hc = { lift := fun (s : CategoryTheory.Limits.Cone F.unop) => (hc.desc (CategoryTheory.Limits.coconeOfConeUnop s)).unop, fac := ⋯, uniq := ⋯ }
Instances For
Turn a limit of F : Jᵒᵖ ⥤ Cᵒᵖ
into a colimit of F.unop : J ⥤ C
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Turn a colimit for F.leftOp : Jᵒᵖ ⥤ C
into a limit for F : J ⥤ Cᵒᵖ
.
Equations
- CategoryTheory.Limits.isLimitConeOfCoconeLeftOp F hc = { lift := fun (s : CategoryTheory.Limits.Cone F) => (hc.desc (CategoryTheory.Limits.coconeLeftOpOfCone s)).op, fac := ⋯, uniq := ⋯ }
Instances For
Turn a limit of F.leftOp : Jᵒᵖ ⥤ C
into a colimit of F : J ⥤ Cᵒᵖ
.
Equations
- CategoryTheory.Limits.isColimitCoconeOfConeLeftOp F hc = { desc := fun (s : CategoryTheory.Limits.Cocone F) => (hc.lift (CategoryTheory.Limits.coneLeftOpOfCocone s)).op, fac := ⋯, uniq := ⋯ }
Instances For
Turn a colimit for F.rightOp : J ⥤ Cᵒᵖ
into a limit for F : Jᵒᵖ ⥤ C
.
Equations
- CategoryTheory.Limits.isLimitConeOfCoconeRightOp F hc = { lift := fun (s : CategoryTheory.Limits.Cone F) => (hc.desc (CategoryTheory.Limits.coconeRightOpOfCone s)).unop, fac := ⋯, uniq := ⋯ }
Instances For
Turn a limit for F.rightOp : J ⥤ Cᵒᵖ
into a colimit for F : Jᵒᵖ ⥤ C
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Turn a colimit for F.unop : J ⥤ C
into a limit for F : Jᵒᵖ ⥤ Cᵒᵖ
.
Equations
- CategoryTheory.Limits.isLimitConeOfCoconeUnop F hc = { lift := fun (s : CategoryTheory.Limits.Cone F) => (hc.desc (CategoryTheory.Limits.coconeUnopOfCone s)).op, fac := ⋯, uniq := ⋯ }
Instances For
Turn a limit for F.unop : J ⥤ C
into a colimit for F : Jᵒᵖ ⥤ Cᵒᵖ
.
Equations
- CategoryTheory.Limits.isColimitCoconeOfConeUnop F hc = { desc := fun (s : CategoryTheory.Limits.Cocone F) => (hc.lift (CategoryTheory.Limits.coneUnopOfCocone s)).op, fac := ⋯, uniq := ⋯ }
Instances For
Turn a limit for F.leftOp : Jᵒᵖ ⥤ C
into a colimit for F : J ⥤ Cᵒᵖ
.
Equations
Instances For
Turn a colimit for F.leftOp : Jᵒᵖ ⥤ C
into a limit for F : J ⥤ Cᵒᵖ
.
Equations
Instances For
Turn a limit for F.rightOp : J ⥤ Cᵒᵖ
into a colimit for F : Jᵒᵖ ⥤ C
.
Equations
Instances For
Turn a colimit for F.rightOp : J ⥤ Cᵒᵖ
into a limit for F : Jᵒᵖ ⥤ C
.
Equations
Instances For
Turn a limit for F.unop : J ⥤ C
into a colimit for F : Jᵒᵖ ⥤ Cᵒᵖ
.
Equations
Instances For
Turn a colimit for F.unop : J ⥤ C
into a limit for F : Jᵒᵖ ⥤ Cᵒᵖ
.
Equations
Instances For
Turn a limit for F : J ⥤ Cᵒᵖ
into a colimit for F.leftOp : Jᵒᵖ ⥤ C
.
Equations
Instances For
Turn a colimit for F : J ⥤ Cᵒᵖ
into a limit for F.leftOp : Jᵒᵖ ⥤ C
.
Equations
Instances For
Turn a limit for F : Jᵒᵖ ⥤ C
into a colimit for F.rightOp : J ⥤ Cᵒᵖ.
Equations
Instances For
Turn a colimit for F : Jᵒᵖ ⥤ C
into a limit for F.rightOp : J ⥤ Cᵒᵖ
.
Equations
Instances For
Turn a limit for F : Jᵒᵖ ⥤ Cᵒᵖ
into a colimit for F.unop : J ⥤ C
.
Equations
Instances For
Turn a colimit for F : Jᵒᵖ ⥤ Cᵒᵖ
into a limit for F.unop : J ⥤ C
.
Equations
Instances For
If F.leftOp : Jᵒᵖ ⥤ C
has a colimit, we can construct a limit for F : J ⥤ Cᵒᵖ
.
The limit of F.op
is the opposite of colimit F
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The limit of F.leftOp
is the unopposite of colimit F
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The limit of F.rightOp
is the opposite of colimit F
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The limit of F.unop
is the unopposite of colimit F
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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ᵒᵖ
.
The colimit of F.op
is the opposite of limit F
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The colimit of F.leftOp
is the unopposite of limit F
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The colimit of F.rightOp
is the opposite of limit F
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The colimit of F.unop
is the unopposite of limit F
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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ᵒᵖ
.