Limits in C give colimits in Cᵒᵖ.

We construct limits and colimits in the opposite categories.

def CategoryTheory.Limits.isLimitConeLeftOpOfCocone {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 (coneLeftOpOfCocone c)

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.

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

Equations

• One or more equations did not get rendered due to their size.

@[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ᵒᵖ.

Equations

• One or more equations did not get rendered due to their size.

@[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ᵒᵖ.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CategoryTheory.Limits.isLimitConeUnopOfCocone F hc = { lift := fun (s : CategoryTheory.Limits.Cone F.unop) => (hc.desc (CategoryTheory.Limits.coconeOfConeUnop s)).unop, fac := ⋯, uniq := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.

@[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ᵒᵖ.

Equations

• CategoryTheory.Limits.isLimitConeOfCoconeLeftOp F hc = { lift := fun (s : CategoryTheory.Limits.Cone F) => (hc.desc (CategoryTheory.Limits.coconeLeftOpOfCone s)).op, fac := ⋯, uniq := ⋯ }

@[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ᵒᵖ.

Equations

• CategoryTheory.Limits.isColimitCoconeOfConeLeftOp F hc = { desc := fun (s : CategoryTheory.Limits.Cocone F) => (hc.lift (CategoryTheory.Limits.coneLeftOpOfCocone s)).op, fac := ⋯, uniq := ⋯ }

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

Equations

• CategoryTheory.Limits.isLimitConeOfCoconeRightOp F hc = { lift := fun (s : CategoryTheory.Limits.Cone F) => (hc.desc (CategoryTheory.Limits.coconeRightOpOfCone s)).unop, fac := ⋯, uniq := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.

@[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ᵒᵖ.

Equations

• CategoryTheory.Limits.isLimitConeOfCoconeUnop F hc = { lift := fun (s : CategoryTheory.Limits.Cone F) => (hc.desc (CategoryTheory.Limits.coconeUnopOfCone s)).op, fac := ⋯, uniq := ⋯ }

@[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ᵒᵖ.

Equations

• CategoryTheory.Limits.isColimitCoconeOfConeUnop F hc = { desc := fun (s : CategoryTheory.Limits.Cocone F) => (hc.lift (CategoryTheory.Limits.coneUnopOfCocone s)).op, fac := ⋯, uniq := ⋯ }

@[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)) : IsColimit c

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

Equations

• CategoryTheory.Limits.isColimitOfConeLeftOpOfCocone F hc = CategoryTheory.Limits.isColimitCoconeOfConeLeftOp F hc

@[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)) : IsLimit c

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

Equations

• CategoryTheory.Limits.isLimitOfCoconeLeftOpOfCone F hc = CategoryTheory.Limits.isLimitConeOfCoconeLeftOp F hc

@[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)) : IsColimit c

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

Equations

• CategoryTheory.Limits.isColimitOfConeRightOpOfCocone F hc = CategoryTheory.Limits.isColimitCoconeOfConeRightOp F hc

@[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)) : IsLimit c

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

Equations

• CategoryTheory.Limits.isLimitOfCoconeRightOpOfCone F hc = CategoryTheory.Limits.isLimitConeOfCoconeRightOp F hc

@[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)) : IsColimit c

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

Equations

• CategoryTheory.Limits.isColimitOfConeUnopOfCocone F hc = CategoryTheory.Limits.isColimitCoconeOfConeUnop F hc

@[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)) : IsLimit c

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

Equations

• CategoryTheory.Limits.isLimitOfCoconeUnopOfCone F hc = CategoryTheory.Limits.isLimitConeOfCoconeUnop F hc

@[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)) : IsColimit c

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

Equations

• CategoryTheory.Limits.isColimitOfConeOfCoconeLeftOp F hc = CategoryTheory.Limits.isColimitCoconeLeftOpOfCone F hc

@[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)) : IsLimit c

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

Equations

• CategoryTheory.Limits.isLimitOfCoconeOfConeLeftOp F hc = CategoryTheory.Limits.isLimitConeLeftOpOfCocone F hc

@[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)) : IsColimit c

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

Equations

• CategoryTheory.Limits.isColimitOfConeOfCoconeRightOp F hc = CategoryTheory.Limits.isColimitCoconeRightOpOfCone F hc

@[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)) : IsLimit c

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

Equations

• CategoryTheory.Limits.isLimitOfCoconeOfConeRightOp F hc = CategoryTheory.Limits.isLimitConeRightOpOfCocone F hc

@[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)) : IsColimit c

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

Equations

• CategoryTheory.Limits.isColimitOfConeOfCoconeUnop F hc = CategoryTheory.Limits.isColimitCoconeUnopOfCone F hc

@[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)) : IsLimit c

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

Equations

• CategoryTheory.Limits.isLimitOfCoconeOfConeUnop F hc = CategoryTheory.Limits.isLimitConeUnopOfCocone F hc

@[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] : HasLimit F

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] : HasLimit F

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] : HasLimit F

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] : HasLimit F

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

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.

Equations

• One or more equations did not get rendered due to their size.

@[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

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.

Equations

• One or more equations did not get rendered due to their size.

@[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

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.

Equations

• One or more equations did not get rendered due to their size.

@[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

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.

Equations

• One or more equations did not get rendered due to their size.

@[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

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

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

theorem CategoryTheory.Limits.hasLimits_of_hasColimits_op {C : Type u₁} [Category.{v₁, u₁} C] [HasColimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ] : HasLimitsOfSize.{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] : HasColimit F

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] : HasColimit F

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] : HasColimit F

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] : HasColimit F

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

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.

Equations

• One or more equations did not get rendered due to their size.

@[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

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.

Equations

• One or more equations did not get rendered due to their size.

@[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

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.

Equations

• One or more equations did not get rendered due to their size.

@[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

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.

Equations

• One or more equations did not get rendered due to their size.

@[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

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

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

theorem CategoryTheory.Limits.hasColimits_of_hasLimits_op {C : Type u₁} [Category.{v₁, u₁} C] [HasLimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ] : HasColimitsOfSize.{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ᵒᵖ