mathlib documentation

category_theory.limits.opposites

Limits in C give colimits in Cᵒᵖ. #

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

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

Equations

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

Equations

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

Equations

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

Equations

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 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 products indexed by X, then Cᵒᵖ has coproducts indexed by X.

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₁} [category_theory.category C] {X Y Z : C} (f : X Z) (g : Y Z) (X_1 : category_theory.limits.walking_span) :
(category_theory.limits.span_op f g).inv.app X_1 = (option.rec (category_theory.iso.refl (opposite.op Z)) (category_theory.limits.walking_pair.rec (category_theory.iso.refl (opposite.op X)) (category_theory.iso.refl (opposite.op Y))) X_1).inv
@[simp]
theorem category_theory.limits.span_op_hom_app {C : Type u₁} [category_theory.category C] {X Y Z : C} (f : X Z) (g : Y Z) (X_1 : category_theory.limits.walking_span) :
(category_theory.limits.span_op f g).hom.app X_1 = (option.rec (category_theory.iso.refl (opposite.op Z)) (category_theory.limits.walking_pair.rec (category_theory.iso.refl (opposite.op X)) (category_theory.iso.refl (opposite.op Y))) X_1).hom
@[simp]
@[simp]
theorem category_theory.limits.cospan_op_inv_app {C : Type u₁} [category_theory.category C] {X Y Z : C} (f : X Y) (g : X Z) (X_1 : category_theory.limits.walking_cospan) :
@[simp]
theorem category_theory.limits.cospan_op_hom_app {C : Type u₁} [category_theory.category C] {X Y Z : C} (f : X Y) (g : X Z) (X_1 : category_theory.limits.walking_cospan) :
@[simp]
theorem category_theory.limits.op_span_hom_app {C : Type u₁} [category_theory.category C] {X Y Z : C} (f : X Y) (g : X Z) (X_1 : category_theory.limits.walking_spanᵒᵖ) :
@[simp]
@[simp]
theorem category_theory.limits.pushout_cocone.op_π_app {C : Type u₁} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} (c : category_theory.limits.pushout_cocone f g) (X_1 : category_theory.limits.walking_cospan) :
c.op.π.app X_1 = (c.ι.app X_1).op (option.rec (category_theory.iso.refl (opposite.op X)) (category_theory.limits.walking_pair.rec (category_theory.iso.refl (opposite.op Y)) (category_theory.iso.refl (opposite.op Z))) X_1).inv
theorem category_theory.limits.pushout_cocone.op_X {C : Type u₁} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} (c : category_theory.limits.pushout_cocone f g) :
@[simp]
theorem category_theory.limits.pushout_cocone.op_fst {C : Type u₁} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} (c : category_theory.limits.pushout_cocone f g) :
c.op.fst = c.inl.op
@[simp]
theorem category_theory.limits.pushout_cocone.op_snd {C : Type u₁} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} (c : category_theory.limits.pushout_cocone f g) :
c.op.snd = c.inr.op
@[simp]
theorem category_theory.limits.pullback_cone.unop_inl {C : Type u₁} [category_theory.category C] {X Y Z : Cᵒᵖ} {f : X Z} {g : Y Z} (c : category_theory.limits.pullback_cone f g) :
@[simp]
theorem category_theory.limits.pullback_cone.unop_inr {C : Type u₁} [category_theory.category C] {X Y Z : Cᵒᵖ} {f : X Z} {g : Y Z} (c : category_theory.limits.pullback_cone f g) :
theorem category_theory.limits.pullback_cone.op_ι_app {C : Type u₁} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} (c : category_theory.limits.pullback_cone f g) (X_1 : category_theory.limits.walking_span) :
c.op.ι.app X_1 = (option.rec (category_theory.iso.refl (opposite.op Z)) (category_theory.limits.walking_pair.rec (category_theory.iso.refl (opposite.op X)) (category_theory.iso.refl (opposite.op Y))) X_1).hom (c.π.app X_1).op
theorem category_theory.limits.pullback_cone.op_X {C : Type u₁} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} (c : category_theory.limits.pullback_cone f g) :
@[simp]
theorem category_theory.limits.pullback_cone.op_inl {C : Type u₁} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} (c : category_theory.limits.pullback_cone f g) :
c.op.inl = c.fst.op
@[simp]
theorem category_theory.limits.pullback_cone.op_inr {C : Type u₁} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} (c : category_theory.limits.pullback_cone f g) :
c.op.inr = c.snd.op
def category_theory.limits.pullback_cone.op_unop {C : Type u₁} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} (c : category_theory.limits.pullback_cone f g) :
c.op.unop c

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

Equations

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₁} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} (c : category_theory.limits.pushout_cocone f g) :
c.op.unop c

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

Equations

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

Equations

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

Equations

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

Equations

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

Equations