# Documentation

Mathlib.CategoryTheory.Limits.Preserves.Opposites

# Limit preservation properties of functor.op and related constructions #

We formulate conditions about F which imply that F.op, F.unop, F.left_op and F.right_op preserve certain (co)limits.

## Future work #

• Dually, it is possible to formulate conditions about F.op ec. for F to preserve certain (co)limits.
def CategoryTheory.Limits.preservesLimitOp {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) [] :

If F : C ⥤ D preserves colimits of K.left_op : Jᵒᵖ ⥤ C, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves limits of K : J ⥤ Cᵒᵖ.

Instances For
def CategoryTheory.Limits.preservesLimitLeftOp {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) [] :

If F : C ⥤ Dᵒᵖ preserves colimits of K.left_op : Jᵒᵖ ⥤ C, then F.left_op : Cᵒᵖ ⥤ D preserves limits of K : J ⥤ Cᵒᵖ.

Instances For
def CategoryTheory.Limits.preservesLimitRightOp {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :

If F : Cᵒᵖ ⥤ D preserves colimits of K.op : Jᵒᵖ ⥤ Cᵒᵖ, then F.right_op : C ⥤ Dᵒᵖ preserves limits of K : J ⥤ C.

Instances For
def CategoryTheory.Limits.preservesLimitUnop {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) :

If F : Cᵒᵖ ⥤ Dᵒᵖ preserves colimits of K.op : Jᵒᵖ ⥤ Cᵒᵖ, then F.unop : C ⥤ D preserves limits of K : J ⥤ C.

Instances For
def CategoryTheory.Limits.preservesColimitOp {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) [CategoryTheory.Limits.PreservesLimit K.leftOp F] :

If F : C ⥤ D preserves limits of K.left_op : Jᵒᵖ ⥤ C, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves colimits of K : J ⥤ Cᵒᵖ.

Instances For
def CategoryTheory.Limits.preservesColimitLeftOp {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) [CategoryTheory.Limits.PreservesLimit K.leftOp F] :

If F : C ⥤ Dᵒᵖ preserves limits of K.left_op : Jᵒᵖ ⥤ C, then F.left_op : Cᵒᵖ ⥤ D preserves colimits of K : J ⥤ Cᵒᵖ.

Instances For
def CategoryTheory.Limits.preservesColimitRightOp {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) [] :

If F : Cᵒᵖ ⥤ D preserves limits of K.op : Jᵒᵖ ⥤ Cᵒᵖ, then F.right_op : C ⥤ Dᵒᵖ preserves colimits of K : J ⥤ C.

Instances For
def CategoryTheory.Limits.preservesColimitUnop {C : Type u₁} [] {D : Type u₂} [] {J : Type w} (K : ) (F : ) [] :

If F : Cᵒᵖ ⥤ Dᵒᵖ preserves limits of K.op : Jᵒᵖ ⥤ Cᵒᵖ, then F.unop : C ⥤ D preserves colimits of K : J ⥤ C.

Instances For
def CategoryTheory.Limits.preservesLimitsOfShapeOp {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) :

If F : C ⥤ D preserves colimits of shape Jᵒᵖ, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves limits of shape J.

Instances For
def CategoryTheory.Limits.preservesLimitsOfShapeLeftOp {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) :

If F : C ⥤ Dᵒᵖ preserves colimits of shape Jᵒᵖ, then F.left_op : Cᵒᵖ ⥤ D preserves limits of shape J.

Instances For
def CategoryTheory.Limits.preservesLimitsOfShapeRightOp {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) :

If F : Cᵒᵖ ⥤ D preserves colimits of shape Jᵒᵖ, then F.right_op : C ⥤ Dᵒᵖ preserves limits of shape J.

Instances For
def CategoryTheory.Limits.preservesLimitsOfShapeUnop {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) :

If F : Cᵒᵖ ⥤ Dᵒᵖ preserves colimits of shape Jᵒᵖ, then F.unop : C ⥤ D preserves limits of shape J.

Instances For
def CategoryTheory.Limits.preservesColimitsOfShapeOp {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) :

If F : C ⥤ D preserves limits of shape Jᵒᵖ, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves colimits of shape J.

Instances For
def CategoryTheory.Limits.preservesColimitsOfShapeLeftOp {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) :

If F : C ⥤ Dᵒᵖ preserves limits of shape Jᵒᵖ, then F.left_op : Cᵒᵖ ⥤ D preserves colimits of shape J.

Instances For
def CategoryTheory.Limits.preservesColimitsOfShapeRightOp {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) :

If F : Cᵒᵖ ⥤ D preserves limits of shape Jᵒᵖ, then F.right_op : C ⥤ Dᵒᵖ preserves colimits of shape J.

Instances For
def CategoryTheory.Limits.preservesColimitsOfShapeUnop {C : Type u₁} [] {D : Type u₂} [] (J : Type w) (F : ) :

If F : Cᵒᵖ ⥤ Dᵒᵖ preserves limits of shape Jᵒᵖ, then F.unop : C ⥤ D preserves colimits of shape J.

Instances For
def CategoryTheory.Limits.preservesLimitsOp {C : Type u₁} [] {D : Type u₂} [] (F : ) :

If F : C ⥤ D preserves colimits, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves limits.

Instances For
def CategoryTheory.Limits.preservesLimitsLeftOp {C : Type u₁} [] {D : Type u₂} [] (F : ) :

If F : C ⥤ Dᵒᵖ preserves colimits, then F.left_op : Cᵒᵖ ⥤ D preserves limits.

Instances For
def CategoryTheory.Limits.preservesLimitsRightOp {C : Type u₁} [] {D : Type u₂} [] (F : ) :

If F : Cᵒᵖ ⥤ D preserves colimits, then F.right_op : C ⥤ Dᵒᵖ preserves limits.

Instances For

If F : Cᵒᵖ ⥤ Dᵒᵖ preserves colimits, then F.unop : C ⥤ D preserves limits.

Instances For
def CategoryTheory.Limits.perservesColimitsOp {C : Type u₁} [] {D : Type u₂} [] (F : ) :

If F : C ⥤ D preserves limits, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves colimits.

Instances For
def CategoryTheory.Limits.preservesColimitsLeftOp {C : Type u₁} [] {D : Type u₂} [] (F : ) :

If F : C ⥤ Dᵒᵖ preserves limits, then F.left_op : Cᵒᵖ ⥤ D preserves colimits.

Instances For
def CategoryTheory.Limits.preservesColimitsRightOp {C : Type u₁} [] {D : Type u₂} [] (F : ) :

If F : Cᵒᵖ ⥤ D preserves limits, then F.right_op : C ⥤ Dᵒᵖ preserves colimits.

Instances For

If F : Cᵒᵖ ⥤ Dᵒᵖ preserves limits, then F.unop : C ⥤ D preserves colimits.

Instances For
def CategoryTheory.Limits.preservesFiniteLimitsOp {C : Type u₁} [] {D : Type u₂} [] (F : ) :

If F : C ⥤ D preserves finite colimits, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves finite limits.

Instances For
def CategoryTheory.Limits.preservesFiniteLimitsLeftOp {C : Type u₁} [] {D : Type u₂} [] (F : ) :

If F : C ⥤ Dᵒᵖ preserves finite colimits, then F.left_op : Cᵒᵖ ⥤ D preserves finite limits.

Instances For
def CategoryTheory.Limits.preservesFiniteLimitsRightOp {C : Type u₁} [] {D : Type u₂} [] (F : ) :

If F : Cᵒᵖ ⥤ D preserves finite colimits, then F.right_op : C ⥤ Dᵒᵖ preserves finite limits.

Instances For

If F : Cᵒᵖ ⥤ Dᵒᵖ preserves finite colimits, then F.unop : C ⥤ D preserves finite limits.

Instances For

If F : C ⥤ D preserves finite limits, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves finite colimits.

Instances For
def CategoryTheory.Limits.preservesFiniteColimitsLeftOp {C : Type u₁} [] {D : Type u₂} [] (F : ) :

If F : C ⥤ Dᵒᵖ preserves finite limits, then F.left_op : Cᵒᵖ ⥤ D preserves finite colimits.

Instances For
def CategoryTheory.Limits.preservesFiniteColimitsRightOp {C : Type u₁} [] {D : Type u₂} [] (F : ) :

If F : Cᵒᵖ ⥤ D preserves finite limits, then F.right_op : C ⥤ Dᵒᵖ preserves finite colimits.

Instances For

If F : Cᵒᵖ ⥤ Dᵒᵖ preserves finite limits, then F.unop : C ⥤ D preserves finite colimits.

Instances For