Limits in C give colimits in Cᵒᵖ.

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

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

@[deprecated CategoryTheory.Limits.isColimitCoconeOfConeUnop (since := "2024-11-01")]

def CategoryTheory.Limits.isColimitConeOfCoconeUnop {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)

Alias of CategoryTheory.Limits.isColimitCoconeOfConeUnop.

---

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

Equations

• @CategoryTheory.Limits.isColimitConeOfCoconeUnop = @CategoryTheory.Limits.isColimitCoconeOfConeUnop

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

instance CategoryTheory.Limits.has_cofiltered_limits_op_of_has_filtered_colimits {C : Type u₁} [Category.{v₁, u₁} C] [HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} C] : HasCofilteredLimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ

theorem CategoryTheory.Limits.has_cofiltered_limits_of_has_filtered_colimits_op {C : Type u₁} [Category.{v₁, u₁} C] [HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ] : HasCofilteredLimitsOfSize.{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.has_filtered_colimits_op_of_has_cofiltered_limits {C : Type u₁} [Category.{v₁, u₁} C] [HasCofilteredLimitsOfSize.{v₂, u₂, v₁, u₁} C] : HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ

theorem CategoryTheory.Limits.has_filtered_colimits_of_has_cofiltered_limits_op {C : Type u₁} [Category.{v₁, u₁} C] [HasCofilteredLimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ] : HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} C

instance CategoryTheory.Limits.hasCoproductsOfShape_opposite {C : Type u₁} [Category.{v₁, u₁} C] (X : Type v₂) [HasProductsOfShape X C] : HasCoproductsOfShape X Cᵒᵖ

If C has products indexed by X, then Cᵒᵖ has coproducts indexed by X.

theorem CategoryTheory.Limits.hasCoproductsOfShape_of_opposite {C : Type u₁} [Category.{v₁, u₁} C] (X : Type v₂) [HasProductsOfShape X Cᵒᵖ] : HasCoproductsOfShape X C

instance CategoryTheory.Limits.hasProductsOfShape_opposite {C : Type u₁} [Category.{v₁, u₁} C] (X : Type v₂) [HasCoproductsOfShape X C] : HasProductsOfShape X Cᵒᵖ

If C has coproducts indexed by X, then Cᵒᵖ has products indexed by X.

theorem CategoryTheory.Limits.hasProductsOfShape_of_opposite {C : Type u₁} [Category.{v₁, u₁} C] (X : Type v₂) [HasCoproductsOfShape X Cᵒᵖ] : HasProductsOfShape X C

instance CategoryTheory.Limits.hasProducts_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasCoproducts C] : HasProducts Cᵒᵖ

theorem CategoryTheory.Limits.hasProducts_of_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasCoproducts Cᵒᵖ] : HasProducts C

instance CategoryTheory.Limits.hasCoproducts_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasProducts C] : HasCoproducts Cᵒᵖ

theorem CategoryTheory.Limits.hasCoproducts_of_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasProducts Cᵒᵖ] : HasCoproducts C

instance CategoryTheory.Limits.hasFiniteCoproducts_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasFiniteProducts C] : HasFiniteCoproducts Cᵒᵖ

theorem CategoryTheory.Limits.hasFiniteCoproducts_of_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasFiniteProducts Cᵒᵖ] : HasFiniteCoproducts C

instance CategoryTheory.Limits.hasFiniteProducts_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasFiniteCoproducts C] : HasFiniteProducts Cᵒᵖ

theorem CategoryTheory.Limits.hasFiniteProducts_of_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasFiniteCoproducts Cᵒᵖ] : HasFiniteProducts C

instance CategoryTheory.Limits.instHasLimitOppositeDiscreteOpFunctor {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [HasCoproduct Z] : HasLimit (Discrete.functor Z).op

instance CategoryTheory.Limits.instHasLimitDiscreteOppositeCompInverseOppositeOpFunctor {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [HasCoproduct Z] : HasLimit ((Discrete.opposite α).inverse.comp (Discrete.functor Z).op)

instance CategoryTheory.Limits.instHasProductOppositeOp {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [HasCoproduct Z] : HasProduct fun (x : α) => Opposite.op (Z x)

def CategoryTheory.Limits.Cofan.op {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} (c : Cofan Z) : Fan fun (x : α) => Opposite.op (Z x)

A Cofan gives a Fan in the opposite category.

Equations

• c.op = CategoryTheory.Limits.Fan.mk (Opposite.op c.pt) fun (a : α) => (c.inj a).op

noncomputable def CategoryTheory.Limits.Cofan.IsColimit.op {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : Cofan Z} (hc : IsColimit c) : IsLimit c.op

If a Cofan is colimit, then its opposite is limit.

Equations

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

def CategoryTheory.Limits.opCoproductIsoProduct' {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : Cofan Z} {f : Fan fun (x : α) => Opposite.op (Z x)} (hc : IsColimit c) (hf : IsLimit f) : Opposite.op c.pt ≅ f.pt

The canonical isomorphism from the opposite of an abstract coproduct to the corresponding product in the opposite category.

Equations

• CategoryTheory.Limits.opCoproductIsoProduct' hc hf = (CategoryTheory.Limits.Cofan.IsColimit.op hc).conePointUniqueUpToIso hf

def CategoryTheory.Limits.opCoproductIsoProduct {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} (Z : α → C) [HasCoproduct Z] : Opposite.op (∐ Z) ≅ ∏ᶜ fun (x : α) => Opposite.op (Z x)

The canonical isomorphism from the opposite of the coproduct to the product in the opposite category.

Equations

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

theorem CategoryTheory.Limits.opCoproductIsoProduct'_inv_comp_inj {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : Cofan Z} {f : Fan fun (x : α) => Opposite.op (Z x)} (hc : IsColimit c) (hf : IsLimit f) (b : α) : CategoryStruct.comp (opCoproductIsoProduct' hc hf).inv (c.inj b).op = f.proj b

theorem CategoryTheory.Limits.opCoproductIsoProduct'_comp_self {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c c' : Cofan Z} {f : Fan fun (x : α) => Opposite.op (Z x)} (hc : IsColimit c) (hc' : IsColimit c') (hf : IsLimit f) : CategoryStruct.comp (opCoproductIsoProduct' hc hf).hom (opCoproductIsoProduct' hc' hf).inv = (hc.coconePointUniqueUpToIso hc').op.inv

theorem CategoryTheory.Limits.opCoproductIsoProduct_inv_comp_ι {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} (Z : α → C) [HasCoproduct Z] (b : α) : CategoryStruct.comp (opCoproductIsoProduct Z).inv (Sigma.ι Z b).op = Pi.π (fun (x : α) => Opposite.op (Z x)) b

theorem CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct'_hom {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : Cofan Z} {f : Fan fun (x : α) => Opposite.op (Z x)} (hc : IsColimit c) (hf : IsLimit f) (c' : Cofan Z) : CategoryStruct.comp (hc.desc c').op (opCoproductIsoProduct' hc hf).hom = hf.lift c'.op

theorem CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct_hom {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [HasCoproduct Z] {X : C} (π : (a : α) → Z a ⟶ X) : CategoryStruct.comp (Sigma.desc π).op (opCoproductIsoProduct Z).hom = Pi.lift fun (a : α) => (π a).op

instance CategoryTheory.Limits.instHasColimitOppositeDiscreteOpFunctor {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [HasProduct Z] : HasColimit (Discrete.functor Z).op

instance CategoryTheory.Limits.instHasColimitDiscreteOppositeCompInverseOppositeOpFunctor {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [HasProduct Z] : HasColimit ((Discrete.opposite α).inverse.comp (Discrete.functor Z).op)

instance CategoryTheory.Limits.instHasCoproductOppositeOp {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [HasProduct Z] : HasCoproduct fun (x : α) => Opposite.op (Z x)

def CategoryTheory.Limits.Fan.op {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} (f : Fan Z) : Cofan fun (x : α) => Opposite.op (Z x)

A Fan gives a Cofan in the opposite category.

Equations

• f.op = CategoryTheory.Limits.Cofan.mk (Opposite.op f.pt) fun (a : α) => (f.proj a).op

noncomputable def CategoryTheory.Limits.Fan.IsLimit.op {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f : Fan Z} (hf : IsLimit f) : IsColimit f.op

If a Fan is limit, then its opposite is colimit.

Equations

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

def CategoryTheory.Limits.opProductIsoCoproduct' {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f : Fan Z} {c : Cofan fun (x : α) => Opposite.op (Z x)} (hf : IsLimit f) (hc : IsColimit c) : Opposite.op f.pt ≅ c.pt

The canonical isomorphism from the opposite of an abstract product to the corresponding coproduct in the opposite category.

Equations

• CategoryTheory.Limits.opProductIsoCoproduct' hf hc = (CategoryTheory.Limits.Fan.IsLimit.op hf).coconePointUniqueUpToIso hc

def CategoryTheory.Limits.opProductIsoCoproduct {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} (Z : α → C) [HasProduct Z] : Opposite.op (∏ᶜ Z) ≅ ∐ fun (x : α) => Opposite.op (Z x)

The canonical isomorphism from the opposite of the product to the coproduct in the opposite category.

Equations

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

theorem CategoryTheory.Limits.proj_comp_opProductIsoCoproduct'_hom {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f : Fan Z} {c : Cofan fun (x : α) => Opposite.op (Z x)} (hf : IsLimit f) (hc : IsColimit c) (b : α) : CategoryStruct.comp (f.proj b).op (opProductIsoCoproduct' hf hc).hom = c.inj b

theorem CategoryTheory.Limits.opProductIsoCoproduct'_comp_self {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f f' : Fan Z} {c : Cofan fun (x : α) => Opposite.op (Z x)} (hf : IsLimit f) (hf' : IsLimit f') (hc : IsColimit c) : CategoryStruct.comp (opProductIsoCoproduct' hf hc).hom (opProductIsoCoproduct' hf' hc).inv = (hf.conePointUniqueUpToIso hf').op.inv

theorem CategoryTheory.Limits.π_comp_opProductIsoCoproduct_hom {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} (Z : α → C) [HasProduct Z] (b : α) : CategoryStruct.comp (Pi.π Z b).op (opProductIsoCoproduct Z).hom = Sigma.ι (fun (x : α) => Opposite.op (Z x)) b

theorem CategoryTheory.Limits.opProductIsoCoproduct'_inv_comp_lift {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f : Fan Z} {c : Cofan fun (x : α) => Opposite.op (Z x)} (hf : IsLimit f) (hc : IsColimit c) (f' : Fan Z) : CategoryStruct.comp (opProductIsoCoproduct' hf hc).inv (hf.lift f').op = hc.desc f'.op

theorem CategoryTheory.Limits.opProductIsoCoproduct_inv_comp_lift {C : Type u₁} [Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [HasProduct Z] {X : C} (π : (a : α) → X ⟶ Z a) : CategoryStruct.comp (opProductIsoCoproduct Z).inv (Pi.lift π).op = Sigma.desc fun (a : α) => (π a).op

instance CategoryTheory.Limits.instHasBinaryCoproductOppositeOp {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] : HasBinaryCoproduct (Opposite.op A) (Opposite.op B)

def CategoryTheory.Limits.opProdIsoCoprod {C : Type u₁} [Category.{v₁, u₁} C] (A B : C) [HasBinaryProduct A B] : Opposite.op (A ⨯ B) ≅ Opposite.op A ⨿ Opposite.op B

The canonical isomorphism from the opposite of the binary product to the coproduct in the opposite category.

Equations

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

@[simp]

theorem CategoryTheory.Limits.fst_opProdIsoCoprod_hom {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] : CategoryStruct.comp prod.fst.op (opProdIsoCoprod A B).hom = coprod.inl

@[simp]

theorem CategoryTheory.Limits.fst_opProdIsoCoprod_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] {Z : Cᵒᵖ} (h : Opposite.op A ⨿ Opposite.op B ⟶ Z) : CategoryStruct.comp prod.fst.op (CategoryStruct.comp (opProdIsoCoprod A B).hom h) = CategoryStruct.comp coprod.inl h

@[simp]

theorem CategoryTheory.Limits.snd_opProdIsoCoprod_hom {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] : CategoryStruct.comp prod.snd.op (opProdIsoCoprod A B).hom = coprod.inr

@[simp]

theorem CategoryTheory.Limits.snd_opProdIsoCoprod_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] {Z : Cᵒᵖ} (h : Opposite.op A ⨿ Opposite.op B ⟶ Z) : CategoryStruct.comp prod.snd.op (CategoryStruct.comp (opProdIsoCoprod A B).hom h) = CategoryStruct.comp coprod.inr h

@[simp]

theorem CategoryTheory.Limits.inl_opProdIsoCoprod_inv {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] : CategoryStruct.comp coprod.inl (opProdIsoCoprod A B).inv = prod.fst.op

@[simp]

theorem CategoryTheory.Limits.inl_opProdIsoCoprod_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] {Z : Cᵒᵖ} (h : Opposite.op (A ⨯ B) ⟶ Z) : CategoryStruct.comp coprod.inl (CategoryStruct.comp (opProdIsoCoprod A B).inv h) = CategoryStruct.comp prod.fst.op h

@[simp]

theorem CategoryTheory.Limits.inr_opProdIsoCoprod_inv {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] : CategoryStruct.comp coprod.inr (opProdIsoCoprod A B).inv = prod.snd.op

@[simp]

theorem CategoryTheory.Limits.inr_opProdIsoCoprod_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] {Z : Cᵒᵖ} (h : Opposite.op (A ⨯ B) ⟶ Z) : CategoryStruct.comp coprod.inr (CategoryStruct.comp (opProdIsoCoprod A B).inv h) = CategoryStruct.comp prod.snd.op h

@[simp]

theorem CategoryTheory.Limits.opProdIsoCoprod_hom_fst {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] : CategoryStruct.comp (opProdIsoCoprod A B).hom.unop prod.fst = coprod.inl.unop

@[simp]

theorem CategoryTheory.Limits.opProdIsoCoprod_hom_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] {Z : C} (h : A ⟶ Z) : CategoryStruct.comp (opProdIsoCoprod A B).hom.unop (CategoryStruct.comp prod.fst h) = CategoryStruct.comp coprod.inl.unop h

@[simp]

theorem CategoryTheory.Limits.opProdIsoCoprod_hom_snd {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] : CategoryStruct.comp (opProdIsoCoprod A B).hom.unop prod.snd = coprod.inr.unop

@[simp]

theorem CategoryTheory.Limits.opProdIsoCoprod_hom_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] {Z : C} (h : B ⟶ Z) : CategoryStruct.comp (opProdIsoCoprod A B).hom.unop (CategoryStruct.comp prod.snd h) = CategoryStruct.comp coprod.inr.unop h

@[simp]

theorem CategoryTheory.Limits.opProdIsoCoprod_inv_inl {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] : CategoryStruct.comp (opProdIsoCoprod A B).inv.unop coprod.inl.unop = prod.fst

@[simp]

theorem CategoryTheory.Limits.opProdIsoCoprod_inv_inl_assoc {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] {Z : C} (h : A ⟶ Z) : CategoryStruct.comp (opProdIsoCoprod A B).inv.unop (CategoryStruct.comp coprod.inl.unop h) = CategoryStruct.comp prod.fst h

@[simp]

theorem CategoryTheory.Limits.opProdIsoCoprod_inv_inr {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] : CategoryStruct.comp (opProdIsoCoprod A B).inv.unop coprod.inr.unop = prod.snd

@[simp]

theorem CategoryTheory.Limits.opProdIsoCoprod_inv_inr_assoc {C : Type u₁} [Category.{v₁, u₁} C] {A B : C} [HasBinaryProduct A B] {Z : C} (h : B ⟶ Z) : CategoryStruct.comp (opProdIsoCoprod A B).inv.unop (CategoryStruct.comp coprod.inr.unop h) = CategoryStruct.comp prod.snd h

instance CategoryTheory.Limits.hasEqualizers_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasCoequalizers C] : HasEqualizers Cᵒᵖ

instance CategoryTheory.Limits.hasCoequalizers_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasEqualizers C] : HasCoequalizers 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ᵒᵖ

instance CategoryTheory.Limits.hasPullbacks_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasPushouts C] : HasPullbacks Cᵒᵖ

instance CategoryTheory.Limits.hasPushouts_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasPullbacks C] : HasPushouts Cᵒᵖ

def CategoryTheory.Limits.spanOp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : span f.op g.op ≅ walkingCospanOpEquiv.inverse.comp (cospan f g).op

The canonical isomorphism relating Span f.op g.op and (Cospan f g).op

Equations

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

@[simp]

theorem CategoryTheory.Limits.spanOp_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (X✝ : WalkingSpan) : (spanOp f g).hom.app X✝ = (Option.rec (Iso.refl (Opposite.op Z)) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op X)) (Iso.refl (Opposite.op Y)) val) X✝).hom

@[simp]

theorem CategoryTheory.Limits.spanOp_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (X✝ : WalkingSpan) : (spanOp f g).inv.app X✝ = (Option.rec (Iso.refl (Opposite.op Z)) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op X)) (Iso.refl (Opposite.op Y)) val) X✝).inv

def CategoryTheory.Limits.opCospan {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospan f g).op ≅ walkingCospanOpEquiv.functor.comp (span f.op g.op)

The canonical isomorphism relating (Cospan f g).op and Span f.op g.op

Equations

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

@[simp]

theorem CategoryTheory.Limits.opCospan_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (X✝ : WalkingCospanᵒᵖ) : (opCospan f g).inv.app X✝ = (Option.rec (Iso.refl (Opposite.op Z)) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op X)) (Iso.refl (Opposite.op Y)) val) (Opposite.unop X✝)).hom

@[simp]

theorem CategoryTheory.Limits.opCospan_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (X✝ : WalkingCospanᵒᵖ) : (opCospan f g).hom.app X✝ = (Option.rec (Iso.refl (Opposite.op Z)) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op X)) (Iso.refl (Opposite.op Y)) val) (Opposite.unop X✝)).inv

def CategoryTheory.Limits.cospanOp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : cospan f.op g.op ≅ walkingSpanOpEquiv.inverse.comp (span f g).op

The canonical isomorphism relating Cospan f.op g.op and (Span f g).op

Equations

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

@[simp]

theorem CategoryTheory.Limits.cospanOp_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (X✝ : WalkingCospan) : (cospanOp f g).inv.app X✝ = (Option.rec (Iso.refl (Opposite.op X)) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op Y)) (Iso.refl (Opposite.op Z)) val) X✝).inv

@[simp]

theorem CategoryTheory.Limits.cospanOp_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (X✝ : WalkingCospan) : (cospanOp f g).hom.app X✝ = (Option.rec (Iso.refl (Opposite.op X)) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op Y)) (Iso.refl (Opposite.op Z)) val) X✝).hom

def CategoryTheory.Limits.opSpan {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (span f g).op ≅ walkingSpanOpEquiv.functor.comp (cospan f.op g.op)

The canonical isomorphism relating (Span f g).op and Cospan f.op g.op

Equations

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

@[simp]

theorem CategoryTheory.Limits.opSpan_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (X✝ : WalkingSpanᵒᵖ) : (opSpan f g).hom.app X✝ = (Option.rec (Iso.refl (Opposite.op X)) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op Y)) (Iso.refl (Opposite.op Z)) val) (Opposite.unop X✝)).inv

@[simp]

theorem CategoryTheory.Limits.opSpan_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (X✝ : WalkingSpanᵒᵖ) : (opSpan f g).inv.app X✝ = (Option.rec (Iso.refl (Opposite.op X)) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op Y)) (Iso.refl (Opposite.op Z)) val) (Opposite.unop X✝)).hom

def CategoryTheory.Limits.PushoutCocone.unop {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : PullbackCone f.unop g.unop

The obvious map PushoutCocone f g → PullbackCone f.unop g.unop

Equations

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

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.unop_π_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) (X✝ : WalkingCospan) : c.unop.π.app X✝ = CategoryStruct.comp (c.ι.app X✝).unop (Option.rec (Iso.refl X) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl Y) (Iso.refl Z) val) X✝).inv.unop

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.unop_pt {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.unop.pt = Opposite.unop c.pt

theorem CategoryTheory.Limits.PushoutCocone.unop_fst {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.unop.fst = c.inl.unop

theorem CategoryTheory.Limits.PushoutCocone.unop_snd {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.unop.snd = c.inr.unop

def CategoryTheory.Limits.PushoutCocone.op {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : PullbackCone f.op g.op

The obvious map PushoutCocone f.op g.op → PullbackCone f g

Equations

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

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.op_pt {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.op.pt = Opposite.op c.pt

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.op_π_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) (X✝ : WalkingCospan) : c.op.π.app X✝ = CategoryStruct.comp (c.ι.app X✝).op (Option.rec (Iso.refl (Opposite.op X)) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op Y)) (Iso.refl (Opposite.op Z)) val) X✝).inv

theorem CategoryTheory.Limits.PushoutCocone.op_fst {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.op.fst = c.inl.op

theorem CategoryTheory.Limits.PushoutCocone.op_snd {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.op.snd = c.inr.op

def CategoryTheory.Limits.PullbackCone.unop {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : PushoutCocone f.unop g.unop

The obvious map PullbackCone f g → PushoutCocone f.unop g.unop

Equations

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

@[simp]

theorem CategoryTheory.Limits.PullbackCone.unop_ι_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) (X✝ : WalkingSpan) : c.unop.ι.app X✝ = CategoryStruct.comp (Option.rec (Iso.refl Z) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl X) (Iso.refl Y) val) X✝).hom.unop (c.π.app X✝).unop

@[simp]

theorem CategoryTheory.Limits.PullbackCone.unop_pt {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.unop.pt = Opposite.unop c.pt

theorem CategoryTheory.Limits.PullbackCone.unop_inl {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.unop.inl = c.fst.unop

theorem CategoryTheory.Limits.PullbackCone.unop_inr {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.unop.inr = c.snd.unop

def CategoryTheory.Limits.PullbackCone.op {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : PushoutCocone f.op g.op

The obvious map PullbackCone f g → PushoutCocone f.op g.op

Equations

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

@[simp]

theorem CategoryTheory.Limits.PullbackCone.op_pt {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.op.pt = Opposite.op c.pt

@[simp]

theorem CategoryTheory.Limits.PullbackCone.op_ι_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) (X✝ : WalkingSpan) : c.op.ι.app X✝ = CategoryStruct.comp (Option.rec (Iso.refl (Opposite.op Z)) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op X)) (Iso.refl (Opposite.op Y)) val) X✝).hom (c.π.app X✝).op

theorem CategoryTheory.Limits.PullbackCone.op_inl {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.op.inl = c.fst.op

theorem CategoryTheory.Limits.PullbackCone.op_inr {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.op.inr = c.snd.op

def CategoryTheory.Limits.PullbackCone.opUnop {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.op.unop ≅ c

If c is a pullback cone, then c.op.unop is isomorphic to c.

Equations

• c.opUnop = CategoryTheory.Limits.PullbackCone.ext (CategoryTheory.Iso.refl c.op.unop.pt) ⋯ ⋯

def CategoryTheory.Limits.PullbackCone.unopOp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.unop.op ≅ c

If c is a pullback cone in Cᵒᵖ, then c.unop.op is isomorphic to c.

Equations

• c.unopOp = CategoryTheory.Limits.PullbackCone.ext (CategoryTheory.Iso.refl c.unop.op.pt) ⋯ ⋯

def CategoryTheory.Limits.PushoutCocone.opUnop {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.op.unop ≅ c

If c is a pushout cocone, then c.op.unop is isomorphic to c.

Equations

• c.opUnop = CategoryTheory.Limits.PushoutCocone.ext (CategoryTheory.Iso.refl c.op.unop.pt) ⋯ ⋯

def CategoryTheory.Limits.PushoutCocone.unopOp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.unop.op ≅ c

If c is a pushout cocone in Cᵒᵖ, then c.unop.op is isomorphic to c.

Equations

• c.unopOp = CategoryTheory.Limits.PushoutCocone.ext (CategoryTheory.Iso.refl c.unop.op.pt) ⋯ ⋯

noncomputable def CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitOp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : IsColimit c ≃ IsLimit c.op

A pushout cone is a colimit cocone if and only if the corresponding pullback cone in the opposite category is a limit cone.

Equations

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

noncomputable def CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitUnop {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : IsColimit c ≃ IsLimit c.unop

A pushout cone is a colimit cocone in Cᵒᵖ if and only if the corresponding pullback cone in C is a limit cone.

Equations

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

def CategoryTheory.Limits.PullbackCone.isLimitEquivIsColimitOp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : IsLimit c ≃ IsColimit c.op

A pullback cone is a limit cone if and only if the corresponding pushout cocone in the opposite category is a colimit cocone.

Equations

• c.isLimitEquivIsColimitOp = (CategoryTheory.Limits.IsLimit.equivIsoLimit c.opUnop).symm.trans c.op.isColimitEquivIsLimitUnop.symm

def CategoryTheory.Limits.PullbackCone.isLimitEquivIsColimitUnop {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : IsLimit c ≃ IsColimit c.unop

A pullback cone is a limit cone in Cᵒᵖ if and only if the corresponding pushout cocone in C is a colimit cocone.

Equations

• c.isLimitEquivIsColimitUnop = (CategoryTheory.Limits.IsLimit.equivIsoLimit c.unopOp).symm.trans c.unop.isColimitEquivIsLimitOp.symm

noncomputable def CategoryTheory.Limits.pullbackIsoUnopPushout {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [h : HasPullback f g] [HasPushout f.op g.op] : pullback f g ≅ Opposite.unop (pushout f.op g.op)

The pullback of f and g in C is isomorphic to the pushout of f.op and g.op in Cᵒᵖ.

Equations

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

@[simp]

theorem CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPushout f.op g.op] : CategoryStruct.comp (pullbackIsoUnopPushout f g).inv (pullback.fst f g) = (pushout.inl f.op g.op).unop

@[simp]

theorem CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPushout f.op g.op] {Z✝ : C} (h : X ⟶ Z✝) : CategoryStruct.comp (pullbackIsoUnopPushout f g).inv (CategoryStruct.comp (pullback.fst f g) h) = CategoryStruct.comp (pushout.inl f.op g.op).unop h

@[simp]

theorem CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPushout f.op g.op] : CategoryStruct.comp (pullbackIsoUnopPushout f g).inv (pullback.snd f g) = (pushout.inr f.op g.op).unop

@[simp]

theorem CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPushout f.op g.op] {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp (pullbackIsoUnopPushout f g).inv (CategoryStruct.comp (pullback.snd f g) h) = CategoryStruct.comp (pushout.inr f.op g.op).unop h

@[simp]

theorem CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPushout f.op g.op] : CategoryStruct.comp (pushout.inl f.op g.op) (pullbackIsoUnopPushout f g).hom.op = (pullback.fst f g).op

@[simp]

theorem CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPushout f.op g.op] {Z✝ : Cᵒᵖ} (h : Opposite.op (pullback f g) ⟶ Z✝) : CategoryStruct.comp (pushout.inl f.op g.op) (CategoryStruct.comp (pullbackIsoUnopPushout f g).hom.op h) = CategoryStruct.comp (pullback.fst f g).op h

@[simp]

theorem CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPushout f.op g.op] : CategoryStruct.comp (pushout.inr f.op g.op) (pullbackIsoUnopPushout f g).hom.op = (pullback.snd f g).op

@[simp]

theorem CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPushout f.op g.op] {Z✝ : Cᵒᵖ} (h : Opposite.op (pullback f g) ⟶ Z✝) : CategoryStruct.comp (pushout.inr f.op g.op) (CategoryStruct.comp (pullbackIsoUnopPushout f g).hom.op h) = CategoryStruct.comp (pullback.snd f g).op h

noncomputable def CategoryTheory.Limits.pushoutIsoUnopPullback {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [h : HasPushout f g] [HasPullback f.op g.op] : pushout f g ≅ Opposite.unop (pullback f.op g.op)

The pushout of f and g in C is isomorphic to the pullback of f.op and g.op in Cᵒᵖ.

Equations

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

@[simp]

theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g] [HasPullback f.op g.op] : CategoryStruct.comp (pushout.inl f g) (pushoutIsoUnopPullback f g).hom = (pullback.fst f.op g.op).unop

@[simp]

theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g] [HasPullback f.op g.op] {Z✝ : C} (h : Opposite.unop (pullback f.op g.op) ⟶ Z✝) : CategoryStruct.comp (pushout.inl f g) (CategoryStruct.comp (pushoutIsoUnopPullback f g).hom h) = CategoryStruct.comp (pullback.fst f.op g.op).unop h

@[simp]

theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g] [HasPullback f.op g.op] : CategoryStruct.comp (pushout.inr f g) (pushoutIsoUnopPullback f g).hom = (pullback.snd f.op g.op).unop

@[simp]

theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g] [HasPullback f.op g.op] {Z✝ : C} (h : Opposite.unop (pullback f.op g.op) ⟶ Z✝) : CategoryStruct.comp (pushout.inr f g) (CategoryStruct.comp (pushoutIsoUnopPullback f g).hom h) = CategoryStruct.comp (pullback.snd f.op g.op).unop h

@[simp]

theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inv_fst {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g] [HasPullback f.op g.op] : CategoryStruct.comp (pushoutIsoUnopPullback f g).inv.op (pullback.fst f.op g.op) = (pushout.inl f g).op

@[simp]

theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inv_snd {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g] [HasPullback f.op g.op] : CategoryStruct.comp (pushoutIsoUnopPullback f g).inv.op (pullback.snd f.op g.op) = (pushout.inr f g).op

def CategoryTheory.Limits.CokernelCofork.IsColimit.ofπOp {C : Type u₁} [Category.{v₁, u₁} C] [HasZeroMorphisms C] {X Y Q : C} (p : Y ⟶ Q) {f : X ⟶ Y} (w : CategoryStruct.comp f p = 0) (h : IsColimit (CokernelCofork.ofπ p w)) : IsLimit (KernelFork.ofι p.op ⋯)

A colimit cokernel cofork gives a limit kernel fork in the opposite category

Equations

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

def CategoryTheory.Limits.CokernelCofork.IsColimit.ofπUnop {C : Type u₁} [Category.{v₁, u₁} C] [HasZeroMorphisms C] {X Y Q : Cᵒᵖ} (p : Y ⟶ Q) {f : X ⟶ Y} (w : CategoryStruct.comp f p = 0) (h : IsColimit (CokernelCofork.ofπ p w)) : IsLimit (KernelFork.ofι p.unop ⋯)

A colimit cokernel cofork in the opposite category gives a limit kernel fork in the original category

Equations

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

def CategoryTheory.Limits.KernelFork.IsLimit.ofιOp {C : Type u₁} [Category.{v₁, u₁} C] [HasZeroMorphisms C] {K X Y : C} (i : K ⟶ X) {f : X ⟶ Y} (w : CategoryStruct.comp i f = 0) (h : IsLimit (KernelFork.ofι i w)) : IsColimit (CokernelCofork.ofπ i.op ⋯)

A limit kernel fork gives a colimit cokernel cofork in the opposite category

Equations

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

def CategoryTheory.Limits.KernelFork.IsLimit.ofιUnop {C : Type u₁} [Category.{v₁, u₁} C] [HasZeroMorphisms C] {K X Y : Cᵒᵖ} (i : K ⟶ X) {f : X ⟶ Y} (w : CategoryStruct.comp i f = 0) (h : IsLimit (KernelFork.ofι i w)) : IsColimit (CokernelCofork.ofπ i.unop ⋯)

A limit kernel fork in the opposite category gives a colimit cokernel cofork in the original category

Equations

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