Limits in C give colimits in Cᵒᵖ.

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

@[simp]

theorem CategoryTheory.Limits.isLimitCoconeOp_lift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J C) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone F.op) : (CategoryTheory.Limits.isLimitCoconeOp F hc).lift s = (hc.desc (CategoryTheory.Limits.Cone.unop s)).op

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

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

Equations

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

@[simp]

theorem CategoryTheory.Limits.isColimitConeOp_desc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J C) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F.op) : (CategoryTheory.Limits.isColimitConeOp F hc).desc s = (hc.lift (CategoryTheory.Limits.Cocone.unop s)).op

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

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

Equations

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

@[simp]

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

def CategoryTheory.Limits.isLimitConeLeftOpOfCocone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.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.isColimitCoconeLeftOpOfCone_desc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F.leftOp) : (CategoryTheory.Limits.isColimitCoconeLeftOpOfCone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeLeftOp s)).unop

def CategoryTheory.Limits.isColimitCoconeLeftOpOfCone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.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.isLimitConeRightOpOfCocone_lift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone F.rightOp) : (CategoryTheory.Limits.isLimitConeRightOpOfCocone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeRightOp s)).op

def CategoryTheory.Limits.isLimitConeRightOpOfCocone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.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.isColimitCoconeRightOpOfCone_desc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F.rightOp) : (CategoryTheory.Limits.isColimitCoconeRightOpOfCone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeRightOp s)).op

def CategoryTheory.Limits.isColimitCoconeRightOpOfCone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.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.isLimitConeUnopOfCocone_lift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.unop F)) : (CategoryTheory.Limits.isLimitConeUnopOfCocone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeUnop s)).unop

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

Turn a colimit for F : Jᵒᵖ ⥤ Cᵒᵖ into a limit for 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₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.unop F)) : (CategoryTheory.Limits.isColimitCoconeUnopOfCone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeUnop s)).unop

def CategoryTheory.Limits.isColimitCoconeUnopOfCone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.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.isLimitCoconeUnop_lift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J C) {c : CategoryTheory.Limits.Cocone F.op} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.isLimitCoconeUnop F hc).lift s = (hc.desc (CategoryTheory.Limits.Cone.op s)).unop

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

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

Equations

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

@[simp]

theorem CategoryTheory.Limits.isColimitConeUnop_desc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J C) {c : CategoryTheory.Limits.Cone F.op} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.isColimitConeUnop F hc).desc s = (hc.lift (CategoryTheory.Limits.Cocone.op s)).unop

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

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

Equations

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

@[simp]

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

def CategoryTheory.Limits.isLimitConeOfCoconeLeftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F.leftOp} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.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.isColimitCoconeOfConeLeftOp_desc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cone F.leftOp} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.isColimitCoconeOfConeLeftOp F hc).desc s = (hc.lift (CategoryTheory.Limits.coneLeftOpOfCocone s)).op

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

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

Equations

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

@[simp]

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

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

Turn a colimit for F.rightOp : J ⥤ Cᵒᵖ into a limit 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₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cone F.rightOp} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.isColimitCoconeOfConeRightOp F hc).desc s = (hc.lift (CategoryTheory.Limits.coneRightOpOfCocone s)).unop

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

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

Equations

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

@[simp]

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

def CategoryTheory.Limits.isLimitConeOfCoconeUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.unop F)} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.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.isColimitConeOfCoconeUnop_desc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.unop F)} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.isColimitConeOfCoconeUnop F hc).desc s = (hc.lift (CategoryTheory.Limits.coneUnopOfCocone s)).op

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

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

Equations

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

theorem CategoryTheory.Limits.hasLimit_of_hasColimit_leftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) [CategoryTheory.Limits.HasColimit F.leftOp] : CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit F.op] : CategoryTheory.Limits.HasLimit F

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

theorem CategoryTheory.Limits.hasLimitsOfShape_op_of_hasColimitsOfShape {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] [CategoryTheory.Limits.HasColimitsOfShape Jᵒᵖ C] : CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] [CategoryTheory.Limits.HasColimitsOfShape Jᵒᵖ Cᵒᵖ] : CategoryTheory.Limits.HasLimitsOfShape J C

instance CategoryTheory.Limits.hasLimits_op_of_hasColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasColimits C] : CategoryTheory.Limits.HasLimits Cᵒᵖ

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

theorem CategoryTheory.Limits.hasColimit_of_hasLimit_leftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J Cᵒᵖ) [CategoryTheory.Limits.HasLimit F.leftOp] : CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasLimit F.op] : CategoryTheory.Limits.HasColimit F

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

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

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

Equations

• ⋯ = ⋯

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

instance CategoryTheory.Limits.hasColimits_op_of_hasLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasLimits C] : CategoryTheory.Limits.HasColimits Cᵒᵖ

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

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

Equations

• ⋯ = ⋯

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

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

A Cofan gives a Fan in the opposite category.

Equations

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

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

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₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {c : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun (x : α) => Opposite.op (Z x)} (hc : CategoryTheory.Limits.IsColimit c) (hf : CategoryTheory.Limits.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.IsLimit.conePointUniqueUpToIso (CategoryTheory.Limits.Cofan.IsColimit.op hc) hf

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

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

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

A Fan gives a Cofan in the opposite category.

Equations

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

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

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₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f : CategoryTheory.Limits.Fan Z} {c : CategoryTheory.Limits.Cofan fun (x : α) => Opposite.op (Z x)} (hf : CategoryTheory.Limits.IsLimit f) (hc : CategoryTheory.Limits.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.IsColimit.coconePointUniqueUpToIso (CategoryTheory.Limits.Fan.IsLimit.op hf) hc

def CategoryTheory.Limits.opProductIsoCoproduct {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} (Z : α → C) [CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} {f : CategoryTheory.Limits.Fan Z} {c : CategoryTheory.Limits.Cofan fun (x : α) => Opposite.op (Z x)} (hf : CategoryTheory.Limits.IsLimit f) (hc : CategoryTheory.Limits.IsColimit c) (b : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.proj f b).op (CategoryTheory.Limits.opProductIsoCoproduct' hf hc).hom = CategoryTheory.Limits.Cofan.inj c b

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

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.spanOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.Limits.span f.op g.op ≅ CategoryTheory.Functor.comp CategoryTheory.Limits.walkingCospanOpEquiv.inverse (CategoryTheory.Limits.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.opCospan_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : X✝ ⟶ Z) (g : Y ⟶ Z) (X : CategoryTheory.Limits.WalkingCospanᵒᵖ) : (CategoryTheory.Limits.opCospan f g).inv.app X = (Option.rec (CategoryTheory.Iso.refl (Opposite.op Z)) (fun (val : CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op X✝)) (CategoryTheory.Iso.refl (Opposite.op Y)) val) X.unop).hom

@[simp]

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

def CategoryTheory.Limits.opCospan {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (CategoryTheory.Limits.cospan f g).op ≅ CategoryTheory.Functor.comp CategoryTheory.Limits.walkingCospanOpEquiv.functor (CategoryTheory.Limits.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.cospanOp_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : X✝ ⟶ Y) (g : X✝ ⟶ Z) (X : CategoryTheory.Limits.WalkingCospan) : (CategoryTheory.Limits.cospanOp f g).hom.app X = (Option.rec (CategoryTheory.Iso.refl (Opposite.op X✝)) (fun (val : CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op Y)) (CategoryTheory.Iso.refl (Opposite.op Z)) val) X).hom

@[simp]

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

def CategoryTheory.Limits.cospanOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : CategoryTheory.Limits.cospan f.op g.op ≅ CategoryTheory.Functor.comp CategoryTheory.Limits.walkingSpanOpEquiv.inverse (CategoryTheory.Limits.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.opSpan_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : X✝ ⟶ Y) (g : X✝ ⟶ Z) (X : CategoryTheory.Limits.WalkingSpanᵒᵖ) : (CategoryTheory.Limits.opSpan f g).inv.app X = (Option.rec (CategoryTheory.Iso.refl (Opposite.op X✝)) (fun (val : CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op Y)) (CategoryTheory.Iso.refl (Opposite.op Z)) val) X.unop).hom

@[simp]

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

def CategoryTheory.Limits.opSpan {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (CategoryTheory.Limits.span f g).op ≅ CategoryTheory.Functor.comp CategoryTheory.Limits.walkingSpanOpEquiv.functor (CategoryTheory.Limits.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.PushoutCocone.unop_π_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X✝ ⟶ Y} {g : X✝ ⟶ Z} (c : CategoryTheory.Limits.PushoutCocone f g) (X : CategoryTheory.Limits.WalkingCospan) : (CategoryTheory.Limits.PushoutCocone.unop c).π.app X = CategoryTheory.CategoryStruct.comp (c.ι.app X).unop (Option.rec (CategoryTheory.Iso.refl X✝) (fun (val : CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl Y) (CategoryTheory.Iso.refl Z) val) X).inv.unop

@[simp]

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

def CategoryTheory.Limits.PushoutCocone.unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : CategoryTheory.Limits.PushoutCocone f g) : CategoryTheory.Limits.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.

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

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.PushoutCocone.op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : CategoryTheory.Limits.PushoutCocone f g) : CategoryTheory.Limits.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.

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

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.PullbackCone.unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : CategoryTheory.Limits.PullbackCone f g) : CategoryTheory.Limits.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.

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

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.PullbackCone.op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : CategoryTheory.Limits.PullbackCone f g) : CategoryTheory.Limits.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.

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

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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.

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

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₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : CategoryTheory.Limits.PullbackCone f g) : CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PullbackCone.op c)

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

Equations

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

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

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

Equations

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

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

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_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Z✝) (g : Y ⟶ Z✝) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPushout f.op g.op] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackIsoUnopPushout f g).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl.unop h

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Z✝) (g : X ⟶ Y) [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPullback f.op g.op] {Z : C} (h : (CategoryTheory.Limits.pullback f.op g.op).unop ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutIsoUnopPullback f g).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst.unop h

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.CokernelCofork.IsColimit.ofπOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} {Y : C} {Q : C} (p : Y ⟶ Q) {f : X ⟶ Y} (w : CategoryTheory.CategoryStruct.comp f p = 0) (h : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ p w)) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Q : Cᵒᵖ} (p : Y ⟶ Q) {f : X ⟶ Y} (w : CategoryTheory.CategoryStruct.comp f p = 0) (h : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ p w)) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : C} {X : C} {Y : C} (i : K ⟶ X) {f : X ⟶ Y} (w : CategoryTheory.CategoryStruct.comp i f = 0) (h : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι i w)) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {K : Cᵒᵖ} {X : Cᵒᵖ} {Y : Cᵒᵖ} (i : K ⟶ X) {f : X ⟶ Y} (w : CategoryTheory.CategoryStruct.comp i f = 0) (h : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι i w)) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.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.