Limits in C give colimits in Cᵒᵖ.

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

@[deprecated CategoryTheory.Limits.IsColimit.op]

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

Alias of CategoryTheory.Limits.IsColimit.op.

---

If t : Cocone F is a colimit cocone, then t.op : Cone F.op is a limit cone.

Equations

• @CategoryTheory.Limits.isLimitCoconeOp = @CategoryTheory.Limits.IsColimit.op

@[deprecated CategoryTheory.Limits.IsLimit.op]

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

Alias of CategoryTheory.Limits.IsLimit.op.

---

If t : Cone F is a limit cone, then t.op : Cocone F.op is a colimit cocone.

Equations

• @CategoryTheory.Limits.isColimitConeOp = @CategoryTheory.Limits.IsLimit.op

@[deprecated CategoryTheory.Limits.IsColimit.unop]

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

Alias of CategoryTheory.Limits.IsColimit.unop.

---

If t : Cocone F.op is a colimit cocone, then t.unop : Cone F. is a limit cone.

Equations

• @CategoryTheory.Limits.isLimitCoconeUnop = @CategoryTheory.Limits.IsColimit.unop

@[deprecated CategoryTheory.Limits.IsLimit.unop]

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

Alias of CategoryTheory.Limits.IsLimit.unop.

---

If t : Cone F.op is a limit cone, then t.unop : Cocone F is a colimit cocone.

Equations

• @CategoryTheory.Limits.isColimitConeUnop = @CategoryTheory.Limits.IsLimit.unop

@[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 F.unop) : (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

• 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.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 F.unop) : (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.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

• 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.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

• 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.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 F.unop} (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 F.unop} (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 F.unop} (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 F.unop} (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.instHasLimitOppositeDiscreteOpFunctor {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.instHasLimitDiscreteOppositeCompInverseOppositeOpFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [CategoryTheory.Limits.HasCoproduct Z] : CategoryTheory.Limits.HasLimit ((CategoryTheory.Discrete.opposite α).inverse.comp (CategoryTheory.Discrete.functor Z).op)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.instHasProductOppositeOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [CategoryTheory.Limits.HasCoproduct Z] : CategoryTheory.Limits.HasProduct fun (x : α) => { unop := 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 : α) => { unop := Z x }

A Cofan gives a Fan in the opposite category.

Equations

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

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

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 : α) => { unop := 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 : α) => { unop := 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 c'.op

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.instHasColimitOppositeDiscreteOpFunctor {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.instHasColimitDiscreteOppositeCompInverseOppositeOpFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [CategoryTheory.Limits.HasProduct Z] : CategoryTheory.Limits.HasColimit ((CategoryTheory.Discrete.opposite α).inverse.comp (CategoryTheory.Discrete.functor Z).op)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.instHasCoproductOppositeOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C} [CategoryTheory.Limits.HasProduct Z] : CategoryTheory.Limits.HasCoproduct fun (x : α) => { unop := 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 : α) => { unop := Z x }

A Fan gives a Cofan in the opposite category.

Equations

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

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

theorem CategoryTheory.Limits.π_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 : α) => { unop := 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 : α) => { unop := 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 f'.op

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 { unop := Z }) (fun (val : CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl { unop := X✝ }) (CategoryTheory.Iso.refl { unop := 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 { unop := Z }) (fun (val : CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl { unop := X✝ }) (CategoryTheory.Iso.refl { unop := 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.Limits.walkingCospanOpEquiv.inverse.comp (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_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 { unop := Z }) (fun (val : CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl { unop := X✝ }) (CategoryTheory.Iso.refl { unop := Y }) val) X.unop).inv

@[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 { unop := Z }) (fun (val : CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl { unop := X✝ }) (CategoryTheory.Iso.refl { unop := Y }) val) X.unop).hom

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.Limits.walkingCospanOpEquiv.functor.comp (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_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 { unop := X✝ }) (fun (val : CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl { unop := Y }) (CategoryTheory.Iso.refl { unop := Z }) val) X).inv

@[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 { unop := X✝ }) (fun (val : CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl { unop := Y }) (CategoryTheory.Iso.refl { unop := Z }) val) X).hom

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.Limits.walkingSpanOpEquiv.inverse.comp (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_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 { unop := X✝ }) (fun (val : CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl { unop := Y }) (CategoryTheory.Iso.refl { unop := Z }) val) X.unop).inv

@[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 { unop := X✝ }) (fun (val : CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl { unop := Y }) (CategoryTheory.Iso.refl { unop := Z }) val) X.unop).hom

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.Limits.walkingSpanOpEquiv.functor.comp (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) : c.unop.π.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) : c.unop.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) : c.unop.fst = c.inl.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) : c.unop.snd = c.inr.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) : c.op.pt = { unop := 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) : c.op.π.app X = CategoryTheory.CategoryStruct.comp (c.ι.app X).op (Option.rec (CategoryTheory.Iso.refl { unop := X✝ }) (fun (val : CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl { unop := Y }) (CategoryTheory.Iso.refl { unop := 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) : c.op.fst = c.inl.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) : c.op.snd = c.inr.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) : c.unop.ι.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) : c.unop.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) : c.unop.inl = c.fst.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) : c.unop.inr = c.snd.unop

@[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) : c.op.ι.app X = CategoryTheory.CategoryStruct.comp (Option.rec (CategoryTheory.Iso.refl { unop := Z }) (fun (val : CategoryTheory.Limits.WalkingPair) => CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl { unop := X✝ }) (CategoryTheory.Iso.refl { unop := Y }) val) X).hom (c.π.app X).op

@[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) : c.op.pt = { unop := c.pt }

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) : c.op.inl = c.fst.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) : c.op.inr = c.snd.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) : 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₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : CategoryTheory.Limits.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₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : CategoryTheory.Limits.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) ⋯ ⋯

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

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 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₁} [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 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₁} [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 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₁} [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 : { unop := 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 : { unop := 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.