# 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₁} [] {C : Type u} {F : } {t : } :

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
Instances For
@[deprecated CategoryTheory.Limits.IsLimit.op]
def CategoryTheory.Limits.isColimitConeOp {J : Type u₁} [] {C : Type u} {F : } {t : } :

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
Instances For
@[deprecated CategoryTheory.Limits.IsColimit.unop]
def CategoryTheory.Limits.isLimitCoconeUnop {J : Type u₁} [] {C : Type u} {F : } {t : } :

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
Instances For
@[deprecated CategoryTheory.Limits.IsLimit.unop]
def CategoryTheory.Limits.isColimitConeUnop {J : Type u₁} [] {C : Type u} {F : } {t : } :

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
Instances For
@[simp]
theorem CategoryTheory.Limits.isLimitConeLeftOpOfCocone_lift {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : } (hc : ) (s : CategoryTheory.Limits.Cone F.leftOp) :
.lift s = (hc.desc ).unop
def CategoryTheory.Limits.isLimitConeLeftOpOfCocone {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : } (hc : ) :

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.
Instances For
@[simp]
theorem CategoryTheory.Limits.isColimitCoconeLeftOpOfCone_desc {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : } (hc : ) (s : CategoryTheory.Limits.Cocone F.leftOp) :
s = (hc.lift ).unop
def CategoryTheory.Limits.isColimitCoconeLeftOpOfCone {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : } (hc : ) :

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.
Instances For
@[simp]
theorem CategoryTheory.Limits.isLimitConeRightOpOfCocone_lift {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : } (hc : ) (s : CategoryTheory.Limits.Cone F.rightOp) :
.lift s = (hc.desc ).op
def CategoryTheory.Limits.isLimitConeRightOpOfCocone {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : } (hc : ) :

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.
Instances For
@[simp]
theorem CategoryTheory.Limits.isColimitCoconeRightOpOfCone_desc {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : } (hc : ) (s : CategoryTheory.Limits.Cocone F.rightOp) :
s = (hc.lift ).op
def CategoryTheory.Limits.isColimitCoconeRightOpOfCone {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : } (hc : ) :

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.
Instances For
@[simp]
theorem CategoryTheory.Limits.isLimitConeUnopOfCocone_lift {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : } (hc : ) (s : ) :
.lift s = (hc.desc ).unop
def CategoryTheory.Limits.isLimitConeUnopOfCocone {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : } (hc : ) :

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

Equations
• = { lift := fun (s : ) => (hc.desc ).unop, fac := , uniq := }
Instances For
@[simp]
theorem CategoryTheory.Limits.isColimitCoconeUnopOfCone_desc {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : } (hc : ) (s : ) :
.desc s = (hc.lift ).unop
def CategoryTheory.Limits.isColimitCoconeUnopOfCone {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : } (hc : ) :

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.
Instances For
@[simp]
theorem CategoryTheory.Limits.isLimitConeOfCoconeLeftOp_lift {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : CategoryTheory.Limits.Cocone F.leftOp} (hc : ) (s : ) :
.lift s = (hc.desc ).op
def CategoryTheory.Limits.isLimitConeOfCoconeLeftOp {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : CategoryTheory.Limits.Cocone F.leftOp} (hc : ) :

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

Equations
• = { lift := fun (s : ) => (hc.desc ).op, fac := , uniq := }
Instances For
@[simp]
theorem CategoryTheory.Limits.isColimitCoconeOfConeLeftOp_desc {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : CategoryTheory.Limits.Cone F.leftOp} (hc : ) (s : ) :
s = (hc.lift ).op
def CategoryTheory.Limits.isColimitCoconeOfConeLeftOp {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : CategoryTheory.Limits.Cone F.leftOp} (hc : ) :

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.
Instances For
@[simp]
theorem CategoryTheory.Limits.isLimitConeOfCoconeRightOp_lift {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : CategoryTheory.Limits.Cocone F.rightOp} (hc : ) (s : ) :
.lift s = (hc.desc ).unop
def CategoryTheory.Limits.isLimitConeOfCoconeRightOp {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : CategoryTheory.Limits.Cocone F.rightOp} (hc : ) :

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.
Instances For
@[simp]
theorem CategoryTheory.Limits.isColimitCoconeOfConeRightOp_desc {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : CategoryTheory.Limits.Cone F.rightOp} (hc : ) (s : ) :
s = (hc.lift ).unop
def CategoryTheory.Limits.isColimitCoconeOfConeRightOp {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : CategoryTheory.Limits.Cone F.rightOp} (hc : ) :

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.
Instances For
@[simp]
theorem CategoryTheory.Limits.isLimitConeOfCoconeUnop_lift {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : } (hc : ) (s : ) :
.lift s = (hc.desc ).op
def CategoryTheory.Limits.isLimitConeOfCoconeUnop {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : } (hc : ) :

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

Equations
• = { lift := fun (s : ) => (hc.desc ).op, fac := , uniq := }
Instances For
@[simp]
theorem CategoryTheory.Limits.isColimitConeOfCoconeUnop_desc {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : } (hc : ) (s : ) :
.desc s = (hc.lift ).op
def CategoryTheory.Limits.isColimitConeOfCoconeUnop {C : Type u₁} [] {J : Type u₂} [] (F : ) {c : } (hc : ) :

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

Equations
• = { desc := fun (s : ) => (hc.lift ).op, fac := , uniq := }
Instances For

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₁} [] {J : Type u₂} [] (F : ) :
theorem CategoryTheory.Limits.hasLimit_op_of_hasColimit {C : Type u₁} [] {J : Type u₂} [] (F : ) :

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

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

Equations
• =
Equations
• =

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₁} [] {J : Type u₂} [] (F : ) :
theorem CategoryTheory.Limits.hasColimit_op_of_hasLimit {C : Type u₁} [] {J : Type u₂} [] (F : ) :

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

Equations
• =

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

Equations
• =
Equations
• =

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

Equations
• =
instance CategoryTheory.Limits.hasProductsOfShape_opposite {C : Type u₁} [] (X : Type v₂) :

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

Equations
• =
Equations
• =
Equations
• =
Equations
• =
Equations
• =
instance CategoryTheory.Limits.instHasLimitOppositeDiscreteOpFunctor {C : Type u₁} [] {α : Type u_1} {Z : αC} :
Equations
• =
Equations
• =
instance CategoryTheory.Limits.instHasProductOppositeOp {C : Type u₁} [] {α : Type u_1} {Z : αC} :
CategoryTheory.Limits.HasProduct fun (x : α) => { unop := Z x }
Equations
• =
def CategoryTheory.Limits.Cofan.op {C : Type u₁} [] {α : Type u_1} {Z : αC} (c : ) :
CategoryTheory.Limits.Fan fun (x : α) => { unop := Z x }

A Cofan gives a Fan in the opposite category.

Equations
Instances For
def CategoryTheory.Limits.Cofan.IsColimit.op {C : Type u₁} [] {α : Type u_1} {Z : αC} {c : } (hc : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.opCoproductIsoProduct' {C : Type u₁} [] {α : Type u_1} {Z : αC} {c : } {f : CategoryTheory.Limits.Fan fun (x : α) => { unop := Z x }} (hc : ) (hf : ) :
{ unop := c.pt } f.pt

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

Equations
• = .conePointUniqueUpToIso hf
Instances For
def CategoryTheory.Limits.opCoproductIsoProduct {C : Type u₁} [] {α : Type u_1} (Z : αC) :
{ 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.
Instances For
theorem CategoryTheory.Limits.opCoproductIsoProduct'_inv_comp_inj {C : Type u₁} [] {α : Type u_1} {Z : αC} {c : } {f : CategoryTheory.Limits.Fan fun (x : α) => { unop := Z x }} (hc : ) (hf : ) (b : α) :
CategoryTheory.CategoryStruct.comp .inv (c.inj b).op = f.proj b
theorem CategoryTheory.Limits.opCoproductIsoProduct'_comp_self {C : Type u₁} [] {α : Type u_1} {Z : αC} {c : } {c' : } {f : CategoryTheory.Limits.Fan fun (x : α) => { unop := Z x }} (hc : ) (hc' : ) (hf : ) :
= (hc.coconePointUniqueUpToIso hc').op.inv
theorem CategoryTheory.Limits.opCoproductIsoProduct_inv_comp_ι {C : Type u₁} [] {α : Type u_1} (Z : αC) (b : α) :
= CategoryTheory.Limits.Pi.π (fun (x : α) => { unop := Z x }) b
theorem CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct'_hom {C : Type u₁} [] {α : Type u_1} {Z : αC} {c : } {f : CategoryTheory.Limits.Fan fun (x : α) => { unop := Z x }} (hc : ) (hf : ) (c' : ) :
CategoryTheory.CategoryStruct.comp (hc.desc c').op .hom = hf.lift c'.op
theorem CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct_hom {C : Type u₁} [] {α : Type u_1} {Z : αC} {X : C} (π : (a : α) → Z a X) :
= CategoryTheory.Limits.Pi.lift fun (a : α) => (π a).op
instance CategoryTheory.Limits.instHasColimitOppositeDiscreteOpFunctor {C : Type u₁} [] {α : Type u_1} {Z : αC} :
Equations
• =
Equations
• =
instance CategoryTheory.Limits.instHasCoproductOppositeOp {C : Type u₁} [] {α : Type u_1} {Z : αC} :
CategoryTheory.Limits.HasCoproduct fun (x : α) => { unop := Z x }
Equations
• =
def CategoryTheory.Limits.Fan.op {C : Type u₁} [] {α : Type u_1} {Z : αC} (f : ) :
CategoryTheory.Limits.Cofan fun (x : α) => { unop := Z x }

A Fan gives a Cofan in the opposite category.

Equations
Instances For
def CategoryTheory.Limits.Fan.IsLimit.op {C : Type u₁} [] {α : Type u_1} {Z : αC} {f : } (hf : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.opProductIsoCoproduct' {C : Type u₁} [] {α : Type u_1} {Z : αC} {f : } {c : CategoryTheory.Limits.Cofan fun (x : α) => { unop := Z x }} (hf : ) (hc : ) :
{ unop := f.pt } c.pt

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

Equations
• = .coconePointUniqueUpToIso hc
Instances For
def CategoryTheory.Limits.opProductIsoCoproduct {C : Type u₁} [] {α : Type u_1} (Z : αC) :
{ 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.
Instances For
theorem CategoryTheory.Limits.proj_comp_opProductIsoCoproduct'_hom {C : Type u₁} [] {α : Type u_1} {Z : αC} {f : } {c : CategoryTheory.Limits.Cofan fun (x : α) => { unop := Z x }} (hf : ) (hc : ) (b : α) :
CategoryTheory.CategoryStruct.comp (f.proj b).op .hom = c.inj b
theorem CategoryTheory.Limits.opProductIsoCoproduct'_comp_self {C : Type u₁} [] {α : Type u_1} {Z : αC} {f : } {f' : } {c : CategoryTheory.Limits.Cofan fun (x : α) => { unop := Z x }} (hf : ) (hf' : ) (hc : ) :
= (hf.conePointUniqueUpToIso hf').op.inv
theorem CategoryTheory.Limits.π_comp_opProductIsoCoproduct_hom {C : Type u₁} [] {α : Type u_1} (Z : αC) (b : α) :
= CategoryTheory.Limits.Sigma.ι (fun (x : α) => { unop := Z x }) b
theorem CategoryTheory.Limits.opProductIsoCoproduct'_inv_comp_lift {C : Type u₁} [] {α : Type u_1} {Z : αC} {f : } {c : CategoryTheory.Limits.Cofan fun (x : α) => { unop := Z x }} (hf : ) (hc : ) (f' : ) :
CategoryTheory.CategoryStruct.comp .inv (hf.lift f').op = hc.desc f'.op
theorem CategoryTheory.Limits.opProductIsoCoproduct_inv_comp_lift {C : Type u₁} [] {α : Type u_1} {Z : αC} {X : C} (π : (a : α) → X Z a) :
= CategoryTheory.Limits.Sigma.desc fun (a : α) => (π a).op
Equations
• =
Equations
• =
Equations
• =
Equations
• =
Equations
• =
Equations
• =
@[simp]
theorem CategoryTheory.Limits.spanOp_inv_app {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X✝ Z) (g : Y Z) :
@[simp]
theorem CategoryTheory.Limits.spanOp_hom_app {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X✝ Z) (g : Y Z) :
def CategoryTheory.Limits.spanOp {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) :
CategoryTheory.Limits.span f.op g.op .comp .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.
Instances For
@[simp]
theorem CategoryTheory.Limits.opCospan_hom_app {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X✝ Z) (g : Y Z) :
.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₁} [] {X : C} {Y : C} {Z : C} (f : X✝ Z) (g : Y Z) :
.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₁} [] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) :
.op .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.
Instances For
@[simp]
theorem CategoryTheory.Limits.cospanOp_inv_app {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X✝ Y) (g : X✝ Z) :
@[simp]
theorem CategoryTheory.Limits.cospanOp_hom_app {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X✝ Y) (g : X✝ Z) :
def CategoryTheory.Limits.cospanOp {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) :
CategoryTheory.Limits.cospan f.op g.op .comp .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.
Instances For
@[simp]
theorem CategoryTheory.Limits.opSpan_hom_app {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X✝ Y) (g : X✝ Z) :
.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₁} [] {X : C} {Y : C} {Z : C} (f : X✝ Y) (g : X✝ Z) :
.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₁} [] {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) :
.op .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.
Instances For
@[simp]
theorem CategoryTheory.Limits.PushoutCocone.unop_π_app {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X✝ Y} {g : X✝ Z} (c : ) :
c.unop.app X = CategoryTheory.CategoryStruct.comp (c.app X).unop (Option.rec () X).inv.unop
@[simp]
theorem CategoryTheory.Limits.PushoutCocone.unop_pt {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X Y} {g : X Z} (c : ) :
c.unop.pt = c.pt.unop
def CategoryTheory.Limits.PushoutCocone.unop {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X Y} {g : X Z} (c : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.PushoutCocone.unop_fst {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X Y} {g : X Z} (c : ) :
c.unop.fst = c.inl.unop
theorem CategoryTheory.Limits.PushoutCocone.unop_snd {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X Y} {g : X Z} (c : ) :
c.unop.snd = c.inr.unop
@[simp]
theorem CategoryTheory.Limits.PushoutCocone.op_pt {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} (c : ) :
c.op.pt = { unop := c.pt }
@[simp]
theorem CategoryTheory.Limits.PushoutCocone.op_π_app {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : X✝ Y} {g : X✝ Z} (c : ) :
def CategoryTheory.Limits.PushoutCocone.op {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} (c : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.PushoutCocone.op_fst {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} (c : ) :
c.op.fst = c.inl.op
theorem CategoryTheory.Limits.PushoutCocone.op_snd {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} (c : ) :
c.op.snd = c.inr.op
@[simp]
theorem CategoryTheory.Limits.PullbackCone.unop_ι_app {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X✝ Z} {g : Y Z} (c : ) :
c.unop.app X = CategoryTheory.CategoryStruct.comp (Option.rec () X).hom.unop (c.app X).unop
@[simp]
theorem CategoryTheory.Limits.PullbackCone.unop_pt {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X Z} {g : Y Z} (c : ) :
c.unop.pt = c.pt.unop
def CategoryTheory.Limits.PullbackCone.unop {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X Z} {g : Y Z} (c : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.PullbackCone.unop_inl {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X Z} {g : Y Z} (c : ) :
c.unop.inl = c.fst.unop
theorem CategoryTheory.Limits.PullbackCone.unop_inr {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X Z} {g : Y Z} (c : ) :
c.unop.inr = c.snd.unop
@[simp]
theorem CategoryTheory.Limits.PullbackCone.op_ι_app {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : X✝ Z} {g : Y Z} (c : ) :
@[simp]
theorem CategoryTheory.Limits.PullbackCone.op_pt {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} (c : ) :
c.op.pt = { unop := c.pt }
def CategoryTheory.Limits.PullbackCone.op {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} (c : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.PullbackCone.op_inl {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} (c : ) :
c.op.inl = c.fst.op
theorem CategoryTheory.Limits.PullbackCone.op_inr {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} (c : ) :
c.op.inr = c.snd.op
def CategoryTheory.Limits.PullbackCone.opUnop {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} (c : ) :
c.op.unop c

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

Equations
Instances For
def CategoryTheory.Limits.PullbackCone.unopOp {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X Z} {g : Y Z} (c : ) :
c.unop.op c

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

Equations
Instances For
def CategoryTheory.Limits.PushoutCocone.opUnop {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} (c : ) :
c.op.unop c

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

Equations
Instances For
def CategoryTheory.Limits.PushoutCocone.unopOp {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X Y} {g : X Z} (c : ) :
c.unop.op c

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

Equations
Instances For
def CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitOp {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} (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.
Instances For
def CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitUnop {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X Y} {g : X Z} (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.
Instances For
def CategoryTheory.Limits.PullbackCone.isLimitEquivIsColimitOp {C : Type u₁} [] {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} (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
• c.isLimitEquivIsColimitOp = ().symm.trans c.op.isColimitEquivIsLimitUnop.symm
Instances For
def CategoryTheory.Limits.PullbackCone.isLimitEquivIsColimitUnop {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X Z} {g : Y Z} (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
• c.isLimitEquivIsColimitUnop = ().symm.trans c.unop.isColimitEquivIsLimitOp.symm
Instances For
noncomputable def CategoryTheory.Limits.pullbackIsoUnopPushout {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [h : ] [CategoryTheory.Limits.HasPushout f.op g.op] :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst_assoc {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Z✝) (g : Y Z✝) [CategoryTheory.Limits.HasPushout f.op g.op] {Z : C} (h : X Z) :
CategoryTheory.CategoryStruct.comp (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₁} [] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPushout f.op g.op] :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst = CategoryTheory.Limits.pushout.inl.unop
@[simp]
theorem CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd_assoc {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Z✝) (g : Y Z✝) [CategoryTheory.Limits.HasPushout f.op g.op] {Z : C} (h : Y Z) :
CategoryTheory.CategoryStruct.comp (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₁} [] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPushout f.op g.op] :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd = CategoryTheory.Limits.pushout.inr.unop
@[simp]
theorem CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl_assoc {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Z✝) (g : Y Z✝) [CategoryTheory.Limits.HasPushout f.op g.op] {Z : Cᵒᵖ} (h : { unop := } Z) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst.op h
@[simp]
theorem CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPushout f.op g.op] :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl .op = CategoryTheory.Limits.pullback.fst.op
@[simp]
theorem CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr_assoc {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Z✝) (g : Y Z✝) [CategoryTheory.Limits.HasPushout f.op g.op] {Z : Cᵒᵖ} (h : { unop := } Z) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd.op h
@[simp]
theorem CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPushout f.op g.op] :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr .op = CategoryTheory.Limits.pullback.snd.op
noncomputable def CategoryTheory.Limits.pushoutIsoUnopPullback {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Z) (g : X Y) [h : ] [] :

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.
Instances For
@[simp]
theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom_assoc {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Z✝) (g : X Y) [] {Z : C} (h : (CategoryTheory.Limits.pullback f.op g.op).unop Z) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst.unop h
@[simp]
theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Z) (g : X Y) [] :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl = CategoryTheory.Limits.pullback.fst.unop
@[simp]
theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom_assoc {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Z✝) (g : X Y) [] {Z : C} (h : (CategoryTheory.Limits.pullback f.op g.op).unop Z) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd.unop h
@[simp]
theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Z) (g : X Y) [] :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr = CategoryTheory.Limits.pullback.snd.unop
@[simp]
theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inv_fst {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Z) (g : X Y) [] :
CategoryTheory.CategoryStruct.comp .op CategoryTheory.Limits.pullback.fst = CategoryTheory.Limits.pushout.inl.op
@[simp]
theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inv_snd {C : Type u₁} [] {X : C} {Y : C} {Z : C} (f : X Z) (g : X Y) [] :
CategoryTheory.CategoryStruct.comp .op CategoryTheory.Limits.pullback.snd = CategoryTheory.Limits.pushout.inr.op
def CategoryTheory.Limits.CokernelCofork.IsColimit.ofπOp {C : Type u₁} [] {X : C} {Y : C} {Q : C} (p : Y Q) {f : X Y} (w : ) :

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.
Instances For
def CategoryTheory.Limits.CokernelCofork.IsColimit.ofπUnop {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Q : Cᵒᵖ} (p : Y Q) {f : X Y} (w : ) :

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.
Instances For
def CategoryTheory.Limits.KernelFork.IsLimit.ofιOp {C : Type u₁} [] {K : C} {X : C} {Y : C} (i : K X) {f : X Y} (w : ) :

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.
Instances For
def CategoryTheory.Limits.KernelFork.IsLimit.ofιUnop {C : Type u₁} [] {K : Cᵒᵖ} {X : Cᵒᵖ} {Y : Cᵒᵖ} (i : K X) {f : X Y} (w : ) :

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