Documentation

@[simp]

theorem CategoryTheory.Limits.isLimitConeLeftOpOfCocone_lift {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) {c : Cocone F} (hc : IsColimit c) (s : Cone F.leftOp) :

(isLimitConeLeftOpOfCocone F hc).lift s = (hc.desc (coconeOfConeLeftOp s)).unop

def CategoryTheory.Limits.isColimitCoconeLeftOpOfCone {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) {c : Cone F} (hc : IsLimit c) :

IsColimit (coconeLeftOpOfCone c)

Turn a limit of F : J ⥤ Cᵒᵖ into a colimit of F.leftOp : Jᵒᵖ ⥤ C.

Instances For

@[simp]

theorem CategoryTheory.Limits.isColimitCoconeLeftOpOfCone_desc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) {c : Cone F} (hc : IsLimit c) (s : Cocone F.leftOp) :

(isColimitCoconeLeftOpOfCone F hc).desc s = (hc.lift (coneOfCoconeLeftOp s)).unop

def CategoryTheory.Limits.isLimitConeRightOpOfCocone {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) {c : Cocone F} (hc : IsColimit c) :

IsLimit (coneRightOpOfCocone c)

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

Instances For

@[simp]

theorem CategoryTheory.Limits.isLimitConeRightOpOfCocone_lift {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) {c : Cocone F} (hc : IsColimit c) (s : Cone F.rightOp) :

(isLimitConeRightOpOfCocone F hc).lift s = (hc.desc (coconeOfConeRightOp s)).op

def CategoryTheory.Limits.isColimitCoconeRightOpOfCone {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) {c : Cone F} (hc : IsLimit c) :

IsColimit (coconeRightOpOfCone c)

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

Instances For

@[simp]

theorem CategoryTheory.Limits.isColimitCoconeRightOpOfCone_desc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) {c : Cone F} (hc : IsLimit c) (s : Cocone F.rightOp) :

(isColimitCoconeRightOpOfCone F hc).desc s = (hc.lift (coneOfCoconeRightOp s)).op

def CategoryTheory.Limits.isLimitConeUnopOfCocone {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) {c : Cocone F} (hc : IsColimit c) :

IsLimit (coneUnopOfCocone c)

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

Instances For

@[simp]

theorem CategoryTheory.Limits.isLimitConeUnopOfCocone_lift {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) {c : Cocone F} (hc : IsColimit c) (s : Cone F.unop) :

(isLimitConeUnopOfCocone F hc).lift s = (hc.desc (coconeOfConeUnop s)).unop

def CategoryTheory.Limits.isColimitCoconeUnopOfCone {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) {c : Cone F} (hc : IsLimit c) :

IsColimit (coconeUnopOfCone c)

Turn a limit of F : Jᵒᵖ ⥤ Cᵒᵖ into a colimit of F.unop : J ⥤ C.

Instances For

@[simp]

theorem CategoryTheory.Limits.isColimitCoconeUnopOfCone_desc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) {c : Cone F} (hc : IsLimit c) (s : Cocone F.unop) :

(isColimitCoconeUnopOfCone F hc).desc s = (hc.lift (coneOfCoconeUnop s)).unop

def CategoryTheory.Limits.isLimitConeOfCoconeLeftOp {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) {c : Cocone F.leftOp} (hc : IsColimit c) :

IsLimit (coneOfCoconeLeftOp c)

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

Instances For

@[simp]

theorem CategoryTheory.Limits.isLimitConeOfCoconeLeftOp_lift {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) {c : Cocone F.leftOp} (hc : IsColimit c) (s : Cone F) :

(isLimitConeOfCoconeLeftOp F hc).lift s = (hc.desc (coconeLeftOpOfCone s)).op

def CategoryTheory.Limits.isColimitCoconeOfConeLeftOp {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) {c : Cone F.leftOp} (hc : IsLimit c) :

IsColimit (coconeOfConeLeftOp c)

Turn a limit of F.leftOp : Jᵒᵖ ⥤ C into a colimit of F : J ⥤ Cᵒᵖ.

Instances For

@[simp]

theorem CategoryTheory.Limits.isColimitCoconeOfConeLeftOp_desc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) {c : Cone F.leftOp} (hc : IsLimit c) (s : Cocone F) :

(isColimitCoconeOfConeLeftOp F hc).desc s = (hc.lift (coneLeftOpOfCocone s)).op

def CategoryTheory.Limits.isLimitConeOfCoconeRightOp {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) {c : Cocone F.rightOp} (hc : IsColimit c) :

IsLimit (coneOfCoconeRightOp c)

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

Instances For

@[simp]

theorem CategoryTheory.Limits.isLimitConeOfCoconeRightOp_lift {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) {c : Cocone F.rightOp} (hc : IsColimit c) (s : Cone F) :

(isLimitConeOfCoconeRightOp F hc).lift s = (hc.desc (coconeRightOpOfCone s)).unop

def CategoryTheory.Limits.isColimitCoconeOfConeRightOp {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) {c : Cone F.rightOp} (hc : IsLimit c) :

IsColimit (coconeOfConeRightOp c)

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

Instances For

@[simp]

theorem CategoryTheory.Limits.isColimitCoconeOfConeRightOp_desc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) {c : Cone F.rightOp} (hc : IsLimit c) (s : Cocone F) :

(isColimitCoconeOfConeRightOp F hc).desc s = (hc.lift (coneRightOpOfCocone s)).unop

def CategoryTheory.Limits.isLimitConeOfCoconeUnop {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) {c : Cocone F.unop} (hc : IsColimit c) :

IsLimit (coneOfCoconeUnop c)

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

Instances For

@[simp]

theorem CategoryTheory.Limits.isLimitConeOfCoconeUnop_lift {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) {c : Cocone F.unop} (hc : IsColimit c) (s : Cone F) :

(isLimitConeOfCoconeUnop F hc).lift s = (hc.desc (coconeUnopOfCone s)).op

def CategoryTheory.Limits.isColimitCoconeOfConeUnop {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) {c : Cone F.unop} (hc : IsLimit c) :

IsColimit (coconeOfConeUnop c)

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

Instances For

@[simp]

theorem CategoryTheory.Limits.isColimitCoconeOfConeUnop_desc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) {c : Cone F.unop} (hc : IsLimit c) (s : Cocone F) :

(isColimitCoconeOfConeUnop F hc).desc s = (hc.lift (coneUnopOfCocone s)).op

def CategoryTheory.Limits.isColimitOfConeLeftOpOfCocone {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) {c : Cocone F} (hc : IsLimit (coneLeftOpOfCocone c)) :

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

Instances For

@[simp]

theorem CategoryTheory.Limits.isColimitOfConeLeftOpOfCocone_desc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) {c : Cocone F} (hc : IsLimit (coneLeftOpOfCocone c)) (s : Cocone F) :

(isColimitOfConeLeftOpOfCocone F hc).desc s = (hc.lift (coneLeftOpOfCocone s)).op

def CategoryTheory.Limits.isLimitOfCoconeLeftOpOfCone {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) {c : Cone F} (hc : IsColimit (coconeLeftOpOfCone c)) :

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

Instances For

@[simp]

theorem CategoryTheory.Limits.isLimitOfCoconeLeftOpOfCone_lift {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) {c : Cone F} (hc : IsColimit (coconeLeftOpOfCone c)) (s : Cone F) :

(isLimitOfCoconeLeftOpOfCone F hc).lift s = (hc.desc (coconeLeftOpOfCone s)).op

def CategoryTheory.Limits.isColimitOfConeRightOpOfCocone {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) {c : Cocone F} (hc : IsLimit (coneRightOpOfCocone c)) :

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

Instances For

@[simp]

theorem CategoryTheory.Limits.isColimitOfConeRightOpOfCocone_desc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) {c : Cocone F} (hc : IsLimit (coneRightOpOfCocone c)) (s : Cocone F) :

(isColimitOfConeRightOpOfCocone F hc).desc s = (hc.lift (coneRightOpOfCocone s)).unop

def CategoryTheory.Limits.isLimitOfCoconeRightOpOfCone {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) {c : Cone F} (hc : IsColimit (coconeRightOpOfCone c)) :

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

Instances For

@[simp]

theorem CategoryTheory.Limits.isLimitOfCoconeRightOpOfCone_lift {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) {c : Cone F} (hc : IsColimit (coconeRightOpOfCone c)) (s : Cone F) :

(isLimitOfCoconeRightOpOfCone F hc).lift s = (hc.desc (coconeRightOpOfCone s)).unop

def CategoryTheory.Limits.isColimitOfConeUnopOfCocone {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) {c : Cocone F} (hc : IsLimit (coneUnopOfCocone c)) :

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

Instances For

@[simp]

theorem CategoryTheory.Limits.isColimitOfConeUnopOfCocone_desc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) {c : Cocone F} (hc : IsLimit (coneUnopOfCocone c)) (s : Cocone F) :

(isColimitOfConeUnopOfCocone F hc).desc s = (hc.lift (coneUnopOfCocone s)).op

def CategoryTheory.Limits.isLimitOfCoconeUnopOfCone {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) {c : Cone F} (hc : IsColimit (coconeUnopOfCone c)) :

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

Instances For

@[simp]

theorem CategoryTheory.Limits.isLimitOfCoconeUnopOfCone_lift {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) {c : Cone F} (hc : IsColimit (coconeUnopOfCone c)) (s : Cone F) :

(isLimitOfCoconeUnopOfCone F hc).lift s = (hc.desc (coconeUnopOfCone s)).op

def CategoryTheory.Limits.isColimitOfConeOfCoconeLeftOp {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) {c : Cocone F.leftOp} (hc : IsLimit (coneOfCoconeLeftOp c)) :

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

Instances For

@[simp]

theorem CategoryTheory.Limits.isColimitOfConeOfCoconeLeftOp_desc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) {c : Cocone F.leftOp} (hc : IsLimit (coneOfCoconeLeftOp c)) (s : Cocone F.leftOp) :

(isColimitOfConeOfCoconeLeftOp F hc).desc s = (hc.lift (coneOfCoconeLeftOp s)).unop

def CategoryTheory.Limits.isLimitOfCoconeOfConeLeftOp {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) {c : Cone F.leftOp} (hc : IsColimit (coconeOfConeLeftOp c)) :

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

Instances For

@[simp]

theorem CategoryTheory.Limits.isLimitOfCoconeOfConeLeftOp_lift {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) {c : Cone F.leftOp} (hc : IsColimit (coconeOfConeLeftOp c)) (s : Cone F.leftOp) :

(isLimitOfCoconeOfConeLeftOp F hc).lift s = (hc.desc (coconeOfConeLeftOp s)).unop

def CategoryTheory.Limits.isColimitOfConeOfCoconeRightOp {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) {c : Cocone F.rightOp} (hc : IsLimit (coneOfCoconeRightOp c)) :

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

Instances For

@[simp]

theorem CategoryTheory.Limits.isColimitOfConeOfCoconeRightOp_desc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) {c : Cocone F.rightOp} (hc : IsLimit (coneOfCoconeRightOp c)) (s : Cocone F.rightOp) :

(isColimitOfConeOfCoconeRightOp F hc).desc s = (hc.lift (coneOfCoconeRightOp s)).op

def CategoryTheory.Limits.isLimitOfCoconeOfConeRightOp {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) {c : Cone F.rightOp} (hc : IsColimit (coconeOfConeRightOp c)) :

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

Instances For

@[simp]

theorem CategoryTheory.Limits.isLimitOfCoconeOfConeRightOp_lift {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) {c : Cone F.rightOp} (hc : IsColimit (coconeOfConeRightOp c)) (s : Cone F.rightOp) :

(isLimitOfCoconeOfConeRightOp F hc).lift s = (hc.desc (coconeOfConeRightOp s)).op

def CategoryTheory.Limits.isColimitOfConeOfCoconeUnop {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) {c : Cocone F.unop} (hc : IsLimit (coneOfCoconeUnop c)) :

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

Instances For

@[simp]

theorem CategoryTheory.Limits.isColimitOfConeOfCoconeUnop_desc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) {c : Cocone F.unop} (hc : IsLimit (coneOfCoconeUnop c)) (s : Cocone F.unop) :

(isColimitOfConeOfCoconeUnop F hc).desc s = (hc.lift (coneOfCoconeUnop s)).unop

def CategoryTheory.Limits.isLimitOfCoconeOfConeUnop {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) {c : Cone F.unop} (hc : IsColimit (coconeOfConeUnop c)) :

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

Instances For

@[simp]

theorem CategoryTheory.Limits.isLimitOfCoconeOfConeUnop_lift {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) {c : Cone F.unop} (hc : IsColimit (coconeOfConeUnop c)) (s : Cone F.unop) :

(isLimitOfCoconeOfConeUnop F hc).lift s = (hc.desc (coconeOfConeUnop s)).unop

theorem CategoryTheory.Limits.hasLimit_of_hasColimit_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) [HasColimit F.leftOp] :

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

theorem CategoryTheory.Limits.hasLimit_of_hasColimit_op {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J C) [HasColimit F.op] :

theorem CategoryTheory.Limits.hasLimit_of_hasColimit_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) [HasColimit F.rightOp] :

theorem CategoryTheory.Limits.hasLimit_of_hasColimit_unop {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) [HasColimit F.unop] :

instance CategoryTheory.Limits.hasLimit_op_of_hasColimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J C) [HasColimit F] :

HasLimit F.op

instance CategoryTheory.Limits.hasLimit_leftOp_of_hasColimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) [HasColimit F] :

HasLimit F.leftOp

instance CategoryTheory.Limits.hasLimit_rightOp_of_hasColimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) [HasColimit F] :

HasLimit F.rightOp

instance CategoryTheory.Limits.hasLimit_unop_of_hasColimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) [HasColimit F] :

HasLimit F.unop

noncomputable def CategoryTheory.Limits.limitOpIsoOpColimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J C) [HasColimit F] :

limit F.op ≅ Opposite.op (colimit F)

The limit of F.op is the opposite of colimit F.

Instances For

@[simp]

theorem CategoryTheory.Limits.limitOpIsoOpColimit_inv_comp_π {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J C) [HasColimit F] (j : Jᵒᵖ) :

CategoryStruct.comp (limitOpIsoOpColimit F).inv (limit.π F.op j) = (colimit.ι F (Opposite.unop j)).op

@[simp]

theorem CategoryTheory.Limits.limitOpIsoOpColimit_inv_comp_π_assoc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J C) [HasColimit F] (j : Jᵒᵖ) {Z : Cᵒᵖ} (h : F.op.obj j ⟶ Z) :

CategoryStruct.comp (limitOpIsoOpColimit F).inv (CategoryStruct.comp (limit.π F.op j) h) = CategoryStruct.comp (colimit.ι F (Opposite.unop j)).op h

@[simp]

theorem CategoryTheory.Limits.limitOpIsoOpColimit_hom_comp_ι {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J C) [HasColimit F] (j : J) :

CategoryStruct.comp (limitOpIsoOpColimit F).hom (colimit.ι F j).op = limit.π F.op (Opposite.op j)

@[simp]

theorem CategoryTheory.Limits.limitOpIsoOpColimit_hom_comp_ι_assoc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J C) [HasColimit F] (j : J) {Z : Cᵒᵖ} (h : Opposite.op (F.obj j) ⟶ Z) :

CategoryStruct.comp (limitOpIsoOpColimit F).hom (CategoryStruct.comp (colimit.ι F j).op h) = CategoryStruct.comp (limit.π F.op (Opposite.op j)) h

noncomputable def CategoryTheory.Limits.limitLeftOpIsoUnopColimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) [HasColimit F] :

limit F.leftOp ≅ Opposite.unop (colimit F)

The limit of F.leftOp is the unopposite of colimit F.

Instances For

@[simp]

theorem CategoryTheory.Limits.limitLeftOpIsoUnopColimit_inv_comp_π {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) [HasColimit F] (j : Jᵒᵖ) :

CategoryStruct.comp (limitLeftOpIsoUnopColimit F).inv (limit.π F.leftOp j) = (colimit.ι F (Opposite.unop j)).unop

@[simp]

theorem CategoryTheory.Limits.limitLeftOpIsoUnopColimit_inv_comp_π_assoc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) [HasColimit F] (j : Jᵒᵖ) {Z : C} (h : F.leftOp.obj j ⟶ Z) :

CategoryStruct.comp (limitLeftOpIsoUnopColimit F).inv (CategoryStruct.comp (limit.π F.leftOp j) h) = CategoryStruct.comp (colimit.ι F (Opposite.unop j)).unop h

@[simp]

theorem CategoryTheory.Limits.limitLeftOpIsoUnopColimit_hom_comp_ι {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) [HasColimit F] (j : J) :

CategoryStruct.comp (limitLeftOpIsoUnopColimit F).hom (colimit.ι F j).unop = limit.π F.leftOp (Opposite.op j)

@[simp]

theorem CategoryTheory.Limits.limitLeftOpIsoUnopColimit_hom_comp_ι_assoc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) [HasColimit F] (j : J) {Z : C} (h : Opposite.unop (F.obj j) ⟶ Z) :

CategoryStruct.comp (limitLeftOpIsoUnopColimit F).hom (CategoryStruct.comp (colimit.ι F j).unop h) = CategoryStruct.comp (limit.π F.leftOp (Opposite.op j)) h

noncomputable def CategoryTheory.Limits.limitRightOpIsoOpColimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) [HasColimit F] :

limit F.rightOp ≅ Opposite.op (colimit F)

The limit of F.rightOp is the opposite of colimit F.

Instances For

@[simp]

theorem CategoryTheory.Limits.limitRightOpIsoOpColimit_inv_comp_π {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) [HasColimit F] (j : J) :

CategoryStruct.comp (limitRightOpIsoOpColimit F).inv (limit.π F.rightOp j) = (colimit.ι F (Opposite.op j)).op

@[simp]

theorem CategoryTheory.Limits.limitRightOpIsoOpColimit_inv_comp_π_assoc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) [HasColimit F] (j : J) {Z : Cᵒᵖ} (h : F.rightOp.obj j ⟶ Z) :

CategoryStruct.comp (limitRightOpIsoOpColimit F).inv (CategoryStruct.comp (limit.π F.rightOp j) h) = CategoryStruct.comp (colimit.ι F (Opposite.op j)).op h

@[simp]

theorem CategoryTheory.Limits.limitRightOpIsoOpColimit_hom_comp_ι {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) [HasColimit F] (j : Jᵒᵖ) :

CategoryStruct.comp (limitRightOpIsoOpColimit F).hom (colimit.ι F j).op = limit.π F.rightOp (Opposite.unop j)

@[simp]

theorem CategoryTheory.Limits.limitRightOpIsoOpColimit_hom_comp_ι_assoc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) [HasColimit F] (j : Jᵒᵖ) {Z : Cᵒᵖ} (h : Opposite.op (F.obj j) ⟶ Z) :

CategoryStruct.comp (limitRightOpIsoOpColimit F).hom (CategoryStruct.comp (colimit.ι F j).op h) = CategoryStruct.comp (limit.π F.rightOp (Opposite.unop j)) h

noncomputable def CategoryTheory.Limits.limitUnopIsoUnopColimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) [HasColimit F] :

limit F.unop ≅ Opposite.unop (colimit F)

The limit of F.unop is the unopposite of colimit F.

Instances For

@[simp]

theorem CategoryTheory.Limits.limitUnopIsoUnopColimit_inv_comp_π {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) [HasColimit F] (j : J) :

CategoryStruct.comp (limitUnopIsoUnopColimit F).inv (limit.π F.unop j) = (colimit.ι F (Opposite.op j)).unop

@[simp]

theorem CategoryTheory.Limits.limitUnopIsoUnopColimit_inv_comp_π_assoc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) [HasColimit F] (j : J) {Z : C} (h : F.unop.obj j ⟶ Z) :

CategoryStruct.comp (limitUnopIsoUnopColimit F).inv (CategoryStruct.comp (limit.π F.unop j) h) = CategoryStruct.comp (colimit.ι F (Opposite.op j)).unop h

@[simp]

theorem CategoryTheory.Limits.limitUnopIsoUnopColimit_hom_comp_ι {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) [HasColimit F] (j : Jᵒᵖ) :

CategoryStruct.comp (limitUnopIsoUnopColimit F).hom (colimit.ι F j).unop = limit.π F.unop (Opposite.unop j)

@[simp]

theorem CategoryTheory.Limits.limitUnopIsoUnopColimit_hom_comp_ι_assoc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) [HasColimit F] (j : Jᵒᵖ) {Z : C} (h : Opposite.unop (F.obj j) ⟶ Z) :

CategoryStruct.comp (limitUnopIsoUnopColimit F).hom (CategoryStruct.comp (colimit.ι F j).unop h) = CategoryStruct.comp (limit.π F.unop (Opposite.unop j)) h

theorem CategoryTheory.Limits.hasLimitsOfShape_op_of_hasColimitsOfShape {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] [HasColimitsOfShape Jᵒᵖ C] :

HasLimitsOfShape J Cᵒᵖ

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

theorem CategoryTheory.Limits.hasLimitsOfShape_of_hasColimitsOfShape_op {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] [HasColimitsOfShape Jᵒᵖ Cᵒᵖ] :

HasLimitsOfShape J C

HasLimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ

instance CategoryTheory.Limits.hasLimits_op_of_hasColimits {C : Type u₁} [Category.{v₁, u₁} C] [HasColimitsOfSize.{v₂, u₂, v₁, u₁} C] :

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

HasLimitsOfSize.{v₂, u₂, v₁, u₁} C

theorem CategoryTheory.Limits.hasLimits_of_hasColimits_op {C : Type u₁} [Category.{v₁, u₁} C] [HasColimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ] :

theorem CategoryTheory.Limits.hasColimit_of_hasLimit_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) [HasLimit F.leftOp] :

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

theorem CategoryTheory.Limits.hasColimit_of_hasLimit_op {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J C) [HasLimit F.op] :

theorem CategoryTheory.Limits.hasColimit_of_hasLimit_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) [HasLimit F.rightOp] :

theorem CategoryTheory.Limits.hasColimit_of_hasLimit_unop {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) [HasLimit F.unop] :

instance CategoryTheory.Limits.hasColimit_op_of_hasLimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J C) [HasLimit F] :

HasColimit F.op

instance CategoryTheory.Limits.hasColimit_leftOp_of_hasLimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) [HasLimit F] :

HasColimit F.leftOp

instance CategoryTheory.Limits.hasColimit_rightOp_of_hasLimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) [HasLimit F] :

HasColimit F.rightOp

instance CategoryTheory.Limits.hasColimit_unop_of_hasLimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) [HasLimit F] :

HasColimit F.unop

noncomputable def CategoryTheory.Limits.colimitOpIsoOpLimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J C) [HasLimit F] :

colimit F.op ≅ Opposite.op (limit F)

The colimit of F.op is the opposite of limit F.

Instances For

@[simp]

theorem CategoryTheory.Limits.ι_comp_colimitOpIsoOpLimit_hom {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J C) [HasLimit F] (j : Jᵒᵖ) :

CategoryStruct.comp (colimit.ι F.op j) (colimitOpIsoOpLimit F).hom = (limit.π F (Opposite.unop j)).op

@[simp]

theorem CategoryTheory.Limits.ι_comp_colimitOpIsoOpLimit_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J C) [HasLimit F] (j : Jᵒᵖ) {Z : Cᵒᵖ} (h : Opposite.op (limit F) ⟶ Z) :

CategoryStruct.comp (colimit.ι F.op j) (CategoryStruct.comp (colimitOpIsoOpLimit F).hom h) = CategoryStruct.comp (limit.π F (Opposite.unop j)).op h

@[simp]

theorem CategoryTheory.Limits.π_comp_colimitOpIsoOpLimit_inv {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J C) [HasLimit F] (j : J) :

CategoryStruct.comp (limit.π F j).op (colimitOpIsoOpLimit F).inv = colimit.ι F.op (Opposite.op j)

@[simp]

theorem CategoryTheory.Limits.π_comp_colimitOpIsoOpLimit_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J C) [HasLimit F] (j : J) {Z : Cᵒᵖ} (h : colimit F.op ⟶ Z) :

CategoryStruct.comp (limit.π F j).op (CategoryStruct.comp (colimitOpIsoOpLimit F).inv h) = CategoryStruct.comp (colimit.ι F.op (Opposite.op j)) h

noncomputable def CategoryTheory.Limits.colimitLeftOpIsoUnopLimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) [HasLimit F] :

colimit F.leftOp ≅ Opposite.unop (limit F)

The colimit of F.leftOp is the unopposite of limit F.

Instances For

@[simp]

theorem CategoryTheory.Limits.ι_comp_colimitLeftOpIsoUnopLimit_hom {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) [HasLimit F] (j : Jᵒᵖ) :

CategoryStruct.comp (colimit.ι F.leftOp j) (colimitLeftOpIsoUnopLimit F).hom = (limit.π F (Opposite.unop j)).unop

@[simp]

theorem CategoryTheory.Limits.ι_comp_colimitLeftOpIsoUnopLimit_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) [HasLimit F] (j : Jᵒᵖ) {Z : C} (h : Opposite.unop (limit F) ⟶ Z) :

CategoryStruct.comp (colimit.ι F.leftOp j) (CategoryStruct.comp (colimitLeftOpIsoUnopLimit F).hom h) = CategoryStruct.comp (limit.π F (Opposite.unop j)).unop h

@[simp]

theorem CategoryTheory.Limits.π_comp_colimitLeftOpIsoUnopLimit_inv {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) [HasLimit F] (j : J) :

CategoryStruct.comp (limit.π F j).unop (colimitLeftOpIsoUnopLimit F).inv = colimit.ι F.leftOp (Opposite.op j)

@[simp]

theorem CategoryTheory.Limits.π_comp_colimitLeftOpIsoUnopLimit_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J Cᵒᵖ) [HasLimit F] (j : J) {Z : C} (h : colimit F.leftOp ⟶ Z) :

CategoryStruct.comp (limit.π F j).unop (CategoryStruct.comp (colimitLeftOpIsoUnopLimit F).inv h) = CategoryStruct.comp (colimit.ι F.leftOp (Opposite.op j)) h

noncomputable def CategoryTheory.Limits.colimitRightOpIsoUnopLimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) [HasLimit F] :

colimit F.rightOp ≅ Opposite.op (limit F)

The colimit of F.rightOp is the opposite of limit F.

Instances For

@[simp]

theorem CategoryTheory.Limits.ι_comp_colimitRightOpIsoUnopLimit_hom {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) [HasLimit F] (j : J) :

CategoryStruct.comp (colimit.ι F.rightOp j) (colimitRightOpIsoUnopLimit F).hom = (limit.π F (Opposite.op j)).op

@[simp]

theorem CategoryTheory.Limits.ι_comp_colimitRightOpIsoUnopLimit_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) [HasLimit F] (j : J) {Z : Cᵒᵖ} (h : Opposite.op (limit F) ⟶ Z) :

CategoryStruct.comp (colimit.ι F.rightOp j) (CategoryStruct.comp (colimitRightOpIsoUnopLimit F).hom h) = CategoryStruct.comp (limit.π F (Opposite.op j)).op h

@[simp]

theorem CategoryTheory.Limits.π_comp_colimitRightOpIsoUnopLimit_inv {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) [HasLimit F] (j : Jᵒᵖ) :

CategoryStruct.comp (limit.π F j).op (colimitRightOpIsoUnopLimit F).inv = colimit.ι F.rightOp (Opposite.unop j)

@[simp]

theorem CategoryTheory.Limits.π_comp_colimitRightOpIsoUnopLimit_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ C) [HasLimit F] (j : Jᵒᵖ) {Z : Cᵒᵖ} (h : colimit F.rightOp ⟶ Z) :

CategoryStruct.comp (limit.π F j).op (CategoryStruct.comp (colimitRightOpIsoUnopLimit F).inv h) = CategoryStruct.comp (colimit.ι F.rightOp (Opposite.unop j)) h

noncomputable def CategoryTheory.Limits.colimitUnopIsoOpLimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) [HasLimit F] :

colimit F.unop ≅ Opposite.unop (limit F)

The colimit of F.unop is the unopposite of limit F.

Instances For

@[simp]

theorem CategoryTheory.Limits.ι_comp_colimitUnopIsoOpLimit_hom {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) [HasLimit F] (j : J) :

CategoryStruct.comp (colimit.ι F.unop j) (colimitUnopIsoOpLimit F).hom = (limit.π F (Opposite.op j)).unop

@[simp]

theorem CategoryTheory.Limits.ι_comp_colimitUnopIsoOpLimit_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) [HasLimit F] (j : J) {Z : C} (h : Opposite.unop (limit F) ⟶ Z) :

CategoryStruct.comp (colimit.ι F.unop j) (CategoryStruct.comp (colimitUnopIsoOpLimit F).hom h) = CategoryStruct.comp (limit.π F (Opposite.op j)).unop h

@[simp]

theorem CategoryTheory.Limits.π_comp_colimitUnopIsoOpLimit_inv {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) [HasLimit F] (j : Jᵒᵖ) :

CategoryStruct.comp (limit.π F j).unop (colimitUnopIsoOpLimit F).inv = colimit.ι F.unop (Opposite.unop j)

@[simp]

theorem CategoryTheory.Limits.π_comp_colimitUnopIsoOpLimit_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor Jᵒᵖ Cᵒᵖ) [HasLimit F] (j : Jᵒᵖ) {Z : C} (h : colimit F.unop ⟶ Z) :

CategoryStruct.comp (limit.π F j).unop (CategoryStruct.comp (colimitUnopIsoOpLimit F).inv h) = CategoryStruct.comp (colimit.ι F.unop (Opposite.unop j)) h

instance CategoryTheory.Limits.hasColimitsOfShape_op_of_hasLimitsOfShape {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] [HasLimitsOfShape Jᵒᵖ C] :

HasColimitsOfShape J Cᵒᵖ

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

theorem CategoryTheory.Limits.hasColimitsOfShape_of_hasLimitsOfShape_op {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] [HasLimitsOfShape Jᵒᵖ Cᵒᵖ] :

HasColimitsOfShape J C

HasColimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ

instance CategoryTheory.Limits.hasColimits_op_of_hasLimits {C : Type u₁} [Category.{v₁, u₁} C] [HasLimitsOfSize.{v₂, u₂, v₁, u₁} C] :

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

HasColimitsOfSize.{v₂, u₂, v₁, u₁} C

theorem CategoryTheory.Limits.hasColimits_of_hasLimits_op {C : Type u₁} [Category.{v₁, u₁} C] [HasLimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ] :

instance CategoryTheory.Limits.hasFiniteColimits_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasFiniteLimits C] :

HasFiniteColimits Cᵒᵖ

instance CategoryTheory.Limits.hasFiniteLimits_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasFiniteColimits C] :

HasFiniteLimits Cᵒᵖ

theorem CategoryTheory.Limits.hasColimit_op_iff_hasLimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] {F : Functor J C} :

HasColimit F.op ↔ HasLimit F

theorem CategoryTheory.Limits.hasColimit_leftOp_iff_hasLimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] {F : Functor J Cᵒᵖ} :

HasColimit F.leftOp ↔ HasLimit F

theorem CategoryTheory.Limits.hasColimit_rightOp_iff_hasLimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] {F : Functor Jᵒᵖ C} :

HasColimit F.rightOp ↔ HasLimit F

theorem CategoryTheory.Limits.hasLimit_op_iff_hasColimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] {F : Functor J C} :

HasLimit F.op ↔ HasColimit F

theorem CategoryTheory.Limits.hasLimit_leftOp_iff_hasColimit {C : Type u₁} [Category.{v₁, u₁} C] {J : Type u₂} [Category.{v₂, u₂} J] {F : Functor J Cᵒᵖ} :

HasLimit F.leftOp ↔ HasColimit F