# mathlibdocumentation

category_theory.limits.opposites

# Limits in C give colimits in Cᵒᵖ. #

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

def category_theory.limits.is_limit_cocone_op {C : Type u₁} {J : Type u₂} (F : J C)  :

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

Equations
@[simp]
theorem category_theory.limits.is_limit_cocone_op_lift {C : Type u₁} {J : Type u₂} (F : J C)  :
= (hc.desc s.unop).op
def category_theory.limits.is_colimit_cone_op {C : Type u₁} {J : Type u₂} (F : J C)  :

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

Equations
@[simp]
theorem category_theory.limits.is_colimit_cone_op_desc {C : Type u₁} {J : Type u₂} (F : J C)  :
= (hc.lift s.unop).op
def category_theory.limits.is_limit_cone_left_op_of_cocone {C : Type u₁} {J : Type u₂} (F : J Cᵒᵖ)  :

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

Equations
@[simp]
theorem category_theory.limits.is_limit_cone_left_op_of_cocone_lift {C : Type u₁} {J : Type u₂} (F : J Cᵒᵖ)  :
def category_theory.limits.is_colimit_cocone_left_op_of_cone {C : Type u₁} {J : Type u₂} (F : J Cᵒᵖ)  :

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

Equations
@[simp]
theorem category_theory.limits.is_colimit_cocone_left_op_of_cone_desc {C : Type u₁} {J : Type u₂} (F : J Cᵒᵖ)  :
@[simp]
theorem category_theory.limits.is_limit_cone_right_op_of_cocone_lift {C : Type u₁} {J : Type u₂} (F : Jᵒᵖ C)  :
def category_theory.limits.is_limit_cone_right_op_of_cocone {C : Type u₁} {J : Type u₂} (F : Jᵒᵖ C)  :

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

Equations
def category_theory.limits.is_colimit_cocone_right_op_of_cone {C : Type u₁} {J : Type u₂} (F : Jᵒᵖ C)  :

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

Equations
@[simp]
theorem category_theory.limits.is_colimit_cocone_right_op_of_cone_desc {C : Type u₁} {J : Type u₂} (F : Jᵒᵖ C)  :
def category_theory.limits.is_limit_cone_unop_of_cocone {C : Type u₁} {J : Type u₂} (F : Jᵒᵖ Cᵒᵖ)  :

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

Equations
@[simp]
theorem category_theory.limits.is_limit_cone_unop_of_cocone_lift {C : Type u₁} {J : Type u₂} (F : Jᵒᵖ Cᵒᵖ)  :
@[simp]
theorem category_theory.limits.is_colimit_cocone_unop_of_cone_desc {C : Type u₁} {J : Type u₂} (F : Jᵒᵖ Cᵒᵖ)  :
def category_theory.limits.is_colimit_cocone_unop_of_cone {C : Type u₁} {J : Type u₂} (F : Jᵒᵖ Cᵒᵖ)  :

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

Equations
def category_theory.limits.is_limit_cocone_unop {C : Type u₁} {J : Type u₂} (F : J C)  :

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

Equations
@[simp]
theorem category_theory.limits.is_limit_cocone_unop_lift {C : Type u₁} {J : Type u₂} (F : J C)  :
= (hc.desc s.op).unop
@[simp]
theorem category_theory.limits.is_colimit_cone_unop_desc {C : Type u₁} {J : Type u₂} (F : J C)  :
= (hc.lift s.op).unop
def category_theory.limits.is_colimit_cone_unop {C : Type u₁} {J : Type u₂} (F : J C)  :

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

Equations
@[simp]
theorem category_theory.limits.is_limit_cone_of_cocone_left_op_lift {C : Type u₁} {J : Type u₂} (F : J Cᵒᵖ)  :
def category_theory.limits.is_limit_cone_of_cocone_left_op {C : Type u₁} {J : Type u₂} (F : J Cᵒᵖ)  :

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

Equations
@[simp]
theorem category_theory.limits.is_colimit_cocone_of_cone_left_op_desc {C : Type u₁} {J : Type u₂} (F : J Cᵒᵖ)  :
def category_theory.limits.is_colimit_cocone_of_cone_left_op {C : Type u₁} {J : Type u₂} (F : J Cᵒᵖ)  :

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

Equations
def category_theory.limits.is_limit_cone_of_cocone_right_op {C : Type u₁} {J : Type u₂} (F : Jᵒᵖ C)  :

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

Equations
@[simp]
theorem category_theory.limits.is_limit_cone_of_cocone_right_op_lift {C : Type u₁} {J : Type u₂} (F : Jᵒᵖ C)  :
@[simp]
theorem category_theory.limits.is_colimit_cocone_of_cone_right_op_desc {C : Type u₁} {J : Type u₂} (F : Jᵒᵖ C)  :
def category_theory.limits.is_colimit_cocone_of_cone_right_op {C : Type u₁} {J : Type u₂} (F : Jᵒᵖ C)  :

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

Equations
@[simp]
theorem category_theory.limits.is_limit_cone_of_cocone_unop_lift {C : Type u₁} {J : Type u₂} (F : Jᵒᵖ Cᵒᵖ)  :
def category_theory.limits.is_limit_cone_of_cocone_unop {C : Type u₁} {J : Type u₂} (F : Jᵒᵖ Cᵒᵖ)  :

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

Equations
def category_theory.limits.is_colimit_cone_of_cocone_unop {C : Type u₁} {J : Type u₂} (F : Jᵒᵖ Cᵒᵖ)  :

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

Equations
@[simp]
theorem category_theory.limits.is_colimit_cone_of_cocone_unop_desc {C : Type u₁} {J : Type u₂} (F : Jᵒᵖ Cᵒᵖ)  :
theorem category_theory.limits.has_limit_of_has_colimit_left_op {C : Type u₁} {J : Type u₂} (F : J Cᵒᵖ)  :

If F.left_op : Jᵒᵖ ⥤ C has a colimit, we can construct a limit for F : J ⥤ Cᵒᵖ.

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

theorem category_theory.limits.has_colimit_of_has_limit_left_op {C : Type u₁} {J : Type u₂} (F : J Cᵒᵖ)  :

If F.left_op : Jᵒᵖ ⥤ C has a limit, we can construct a colimit for F : J ⥤ Cᵒᵖ.

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

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

theorem category_theory.limits.has_coproducts_opposite {C : Type u₁} (X : Type v₁)  :

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

theorem category_theory.limits.has_products_opposite {C : Type u₁} (X : Type v₁)  :

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

@[simp]
theorem category_theory.limits.span_op_inv_app {C : Type u₁} {X Y Z : C} (f : X Z) (g : Y Z)  :
X_1 = (option.rec (category_theory.limits.walking_pair.rec X_1).inv
@[simp]
theorem category_theory.limits.span_op_hom_app {C : Type u₁} {X Y Z : C} (f : X Z) (g : Y Z)  :
X_1 = (option.rec (category_theory.limits.walking_pair.rec X_1).hom
def category_theory.limits.span_op {C : Type u₁} {X Y Z : C} (f : X Z) (g : Y Z) :

The canonical isomorphism relating span f.op g.op and (cospan f g).op

Equations
@[simp]
theorem category_theory.limits.op_cospan_inv_app {C : Type u₁} {X Y Z : C} (f : X Z) (g : Y Z)  :
X_1 = (option.rec (category_theory.limits.walking_pair.rec (opposite.unop X_1)).hom (𝟙 .op).app X_1
@[simp]
theorem category_theory.limits.op_cospan_hom_app {C : Type u₁} {X Y Z : C} (f : X Z) (g : Y Z)  :
X_1 = (option.rec (category_theory.limits.walking_pair.rec (opposite.unop X_1)).inv
def category_theory.limits.op_cospan {C : Type u₁} {X Y Z : C} (f : X Z) (g : Y Z) :

The canonical isomorphism relating (cospan f g).op and span f.op g.op

Equations
def category_theory.limits.cospan_op {C : Type u₁} {X Y Z : C} (f : X Y) (g : X Z) :

The canonical isomorphism relating cospan f.op g.op and (span f g).op

Equations
@[simp]
theorem category_theory.limits.cospan_op_inv_app {C : Type u₁} {X Y Z : C} (f : X Y) (g : X Z)  :
X_1 = (option.rec (category_theory.limits.walking_pair.rec X_1).inv
@[simp]
theorem category_theory.limits.cospan_op_hom_app {C : Type u₁} {X Y Z : C} (f : X Y) (g : X Z)  :
X_1 = (option.rec (category_theory.limits.walking_pair.rec X_1).hom
def category_theory.limits.op_span {C : Type u₁} {X Y Z : C} (f : X Y) (g : X Z) :

The canonical isomorphism relating (span f g).op and cospan f.op g.op

Equations
@[simp]
theorem category_theory.limits.op_span_inv_app {C : Type u₁} {X Y Z : C} (f : X Y) (g : X Z)  :
X_1 = (option.rec (category_theory.limits.walking_pair.rec (opposite.unop X_1)).hom (𝟙 .op).app X_1
@[simp]
theorem category_theory.limits.op_span_hom_app {C : Type u₁} {X Y Z : C} (f : X Y) (g : X Z)  :
X_1 = (option.rec (category_theory.limits.walking_pair.rec (opposite.unop X_1)).inv
theorem category_theory.limits.pushout_cocone.unop_π_app {C : Type u₁} {X Y Z : Cᵒᵖ} {f : X Y} {g : X Z}  :
c.unop.π.app X_1 = (c.ι.app X_1).unop (option.rec (category_theory.limits.walking_pair.rec (opposite.unop (opposite.op X_1))).inv.unop
def category_theory.limits.pushout_cocone.unop {C : Type u₁} {X Y Z : Cᵒᵖ} {f : X Y} {g : X Z}  :

The obvious map pushout_cocone f g → pullback_cone f.unop g.unop

Equations
theorem category_theory.limits.pushout_cocone.unop_X {C : Type u₁} {X Y Z : Cᵒᵖ} {f : X Y} {g : X Z}  :
c.unop.X =
@[simp]
theorem category_theory.limits.pushout_cocone.unop_fst {C : Type u₁} {X Y Z : Cᵒᵖ} {f : X Y} {g : X Z}  :
@[simp]
theorem category_theory.limits.pushout_cocone.unop_snd {C : Type u₁} {X Y Z : Cᵒᵖ} {f : X Y} {g : X Z}  :
theorem category_theory.limits.pushout_cocone.op_π_app {C : Type u₁} {X Y Z : C} {f : X Y} {g : X Z}  :
c.op.π.app X_1 = (c.ι.app X_1).op (option.rec (category_theory.limits.walking_pair.rec X_1).inv
theorem category_theory.limits.pushout_cocone.op_X {C : Type u₁} {X Y Z : C} {f : X Y} {g : X Z}  :
c.op.X =
def category_theory.limits.pushout_cocone.op {C : Type u₁} {X Y Z : C} {f : X Y} {g : X Z}  :

The obvious map pushout_cocone f.op g.op → pullback_cone f g

Equations
@[simp]
theorem category_theory.limits.pushout_cocone.op_fst {C : Type u₁} {X Y Z : C} {f : X Y} {g : X Z}  :
c.op.fst = c.inl.op
@[simp]
theorem category_theory.limits.pushout_cocone.op_snd {C : Type u₁} {X Y Z : C} {f : X Y} {g : X Z}  :
c.op.snd = c.inr.op
def category_theory.limits.pullback_cone.unop {C : Type u₁} {X Y Z : Cᵒᵖ} {f : X Z} {g : Y Z}  :

The obvious map pullback_cone f g → pushout_cocone f.unop g.unop

Equations
theorem category_theory.limits.pullback_cone.unop_X {C : Type u₁} {X Y Z : Cᵒᵖ} {f : X Z} {g : Y Z}  :
c.unop.X =
theorem category_theory.limits.pullback_cone.unop_ι_app {C : Type u₁} {X Y Z : Cᵒᵖ} {f : X Z} {g : Y Z}  :
c.unop.ι.app X_1 = ((𝟙 .op).app (opposite.op X_1)).unop (option.rec (category_theory.limits.walking_pair.rec (opposite.unop (opposite.op X_1))).hom.unop (c.π.app X_1).unop
@[simp]
theorem category_theory.limits.pullback_cone.unop_inl {C : Type u₁} {X Y Z : Cᵒᵖ} {f : X Z} {g : Y Z}  :
@[simp]
theorem category_theory.limits.pullback_cone.unop_inr {C : Type u₁} {X Y Z : Cᵒᵖ} {f : X Z} {g : Y Z}  :
def category_theory.limits.pullback_cone.op {C : Type u₁} {X Y Z : C} {f : X Z} {g : Y Z}  :

The obvious map pullback_cone f g → pushout_cocone f.op g.op

Equations
theorem category_theory.limits.pullback_cone.op_ι_app {C : Type u₁} {X Y Z : C} {f : X Z} {g : Y Z}  :
c.op.ι.app X_1 = (option.rec (category_theory.limits.walking_pair.rec X_1).hom (c.π.app X_1).op
theorem category_theory.limits.pullback_cone.op_X {C : Type u₁} {X Y Z : C} {f : X Z} {g : Y Z}  :
c.op.X =
@[simp]
theorem category_theory.limits.pullback_cone.op_inl {C : Type u₁} {X Y Z : C} {f : X Z} {g : Y Z}  :
c.op.inl = c.fst.op
@[simp]
theorem category_theory.limits.pullback_cone.op_inr {C : Type u₁} {X Y Z : C} {f : X Z} {g : Y Z}  :
c.op.inr = c.snd.op
def category_theory.limits.pullback_cone.op_unop {C : Type u₁} {X Y Z : C} {f : X Z} {g : Y Z}  :
c.op.unop c

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

Equations
def category_theory.limits.pullback_cone.unop_op {C : Type u₁} {X Y Z : Cᵒᵖ} {f : X Z} {g : Y Z}  :
c.unop.op c

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

Equations
def category_theory.limits.pushout_cocone.op_unop {C : Type u₁} {X Y Z : C} {f : X Y} {g : X Z}  :
c.op.unop c

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

Equations
def category_theory.limits.pushout_cocone.unop_op {C : Type u₁} {X Y Z : Cᵒᵖ} {f : X Y} {g : X Z}  :
c.unop.op c

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

Equations
def category_theory.limits.pushout_cocone.is_colimit_equiv_is_limit_op {C : Type u₁} {X Y Z : C} {f : X Y} {g : X Z}  :

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

Equations
def category_theory.limits.pushout_cocone.is_colimit_equiv_is_limit_unop {C : Type u₁} {X Y Z : Cᵒᵖ} {f : X Y} {g : X Z}  :

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

Equations
def category_theory.limits.pullback_cone.is_limit_equiv_is_colimit_op {C : Type u₁} {X Y Z : C} {f : X Z} {g : Y Z}  :

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

Equations
def category_theory.limits.pullback_cone.is_limit_equiv_is_colimit_unop {C : Type u₁} {X Y Z : Cᵒᵖ} {f : X Z} {g : Y Z}  :

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

Equations
noncomputable def category_theory.limits.pullback_iso_unop_pushout {C : Type u₁} {X Y Z : C} (f : X Z) (g : Y Z)  :

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

Equations
@[simp]
theorem category_theory.limits.pullback_iso_unop_pushout_inv_fst_assoc {C : Type u₁} {X Y Z : C} (f : X Z) (g : Y Z) {X' : C} (f' : X X') :
@[simp]
theorem category_theory.limits.pullback_iso_unop_pushout_inv_fst {C : Type u₁} {X Y Z : C} (f : X Z) (g : Y Z)  :
@[simp]
theorem category_theory.limits.pullback_iso_unop_pushout_inv_snd {C : Type u₁} {X Y Z : C} (f : X Z) (g : Y Z)  :
@[simp]
theorem category_theory.limits.pullback_iso_unop_pushout_inv_snd_assoc {C : Type u₁} {X Y Z : C} (f : X Z) (g : Y Z) {X' : C} (f' : Y X') :
@[simp]
theorem category_theory.limits.pullback_iso_unop_pushout_hom_inl {C : Type u₁} {X Y Z : C} (f : X Z) (g : Y Z)  :
@[simp]
theorem category_theory.limits.pullback_iso_unop_pushout_hom_inl_assoc {C : Type u₁} {X Y Z : C} (f : X Z) (g : Y Z) {X' : Cᵒᵖ} (f' : X') :
@[simp]
theorem category_theory.limits.pullback_iso_unop_pushout_hom_inr_assoc {C : Type u₁} {X Y Z : C} (f : X Z) (g : Y Z) {X' : Cᵒᵖ} (f' : X') :
@[simp]
theorem category_theory.limits.pullback_iso_unop_pushout_hom_inr {C : Type u₁} {X Y Z : C} (f : X Z) (g : Y Z)  :
noncomputable def category_theory.limits.pushout_iso_unop_pullback {C : Type u₁} {X Y Z : C} (f : X Z) (g : X Y)  :

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

Equations
@[simp]
theorem category_theory.limits.pushout_iso_unop_pullback_inl_hom_assoc {C : Type u₁} {X Y Z : C} (f : X Z) (g : X Y) {X' : C} (f' : X') :
@[simp]
theorem category_theory.limits.pushout_iso_unop_pullback_inl_hom {C : Type u₁} {X Y Z : C} (f : X Z) (g : X Y)  :
@[simp]
theorem category_theory.limits.pushout_iso_unop_pullback_inr_hom {C : Type u₁} {X Y Z : C} (f : X Z) (g : X Y)  :
@[simp]
theorem category_theory.limits.pushout_iso_unop_pullback_inr_hom_assoc {C : Type u₁} {X Y Z : C} (f : X Z) (g : X Y) {X' : C} (f' : X') :
@[simp]
theorem category_theory.limits.pushout_iso_unop_pullback_inv_fst {C : Type u₁} {X Y Z : C} (f : X Z) (g : X Y)  :
@[simp]
theorem category_theory.limits.pushout_iso_unop_pullback_inv_snd {C : Type u₁} {X Y Z : C} (f : X Z) (g : X Y)  :