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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Cᵒᵖ) (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimit K.leftOp F] : CategoryTheory.Limits.PreservesLimit K F.op

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesLimitLeftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Cᵒᵖ) (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesColimit K.leftOp F] : CategoryTheory.Limits.PreservesLimit K F.leftOp

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesLimitRightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesColimit K.op F] : CategoryTheory.Limits.PreservesLimit K F.rightOp

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesLimitUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesColimit K.op F] : CategoryTheory.Limits.PreservesLimit K F.unop

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesColimitOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Cᵒᵖ) (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimit K.leftOp F] : CategoryTheory.Limits.PreservesColimit K F.op

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesColimitLeftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Cᵒᵖ) (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesLimit K.leftOp F] : CategoryTheory.Limits.PreservesColimit K F.leftOp

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesColimitRightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesLimit K.op F] : CategoryTheory.Limits.PreservesColimit K F.rightOp

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesColimitUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C) (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesLimit K.op F] : CategoryTheory.Limits.PreservesColimit K F.unop

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesLimitsOfShapeOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfShape Jᵒᵖ F] : CategoryTheory.Limits.PreservesLimitsOfShape J F.op

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

Equations

• CategoryTheory.Limits.preservesLimitsOfShapeOp J F = { preservesLimit := fun {K : CategoryTheory.Functor J Cᵒᵖ} => CategoryTheory.Limits.preservesLimitOp K F }

def CategoryTheory.Limits.preservesLimitsOfShapeLeftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesColimitsOfShape Jᵒᵖ F] : CategoryTheory.Limits.PreservesLimitsOfShape J F.leftOp

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

Equations

• CategoryTheory.Limits.preservesLimitsOfShapeLeftOp J F = { preservesLimit := fun {K : CategoryTheory.Functor J Cᵒᵖ} => CategoryTheory.Limits.preservesLimitLeftOp K F }

def CategoryTheory.Limits.preservesLimitsOfShapeRightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesColimitsOfShape Jᵒᵖ F] : CategoryTheory.Limits.PreservesLimitsOfShape J F.rightOp

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

Equations

• CategoryTheory.Limits.preservesLimitsOfShapeRightOp J F = { preservesLimit := fun {K : CategoryTheory.Functor J C} => CategoryTheory.Limits.preservesLimitRightOp K F }

def CategoryTheory.Limits.preservesLimitsOfShapeUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesColimitsOfShape Jᵒᵖ F] : CategoryTheory.Limits.PreservesLimitsOfShape J F.unop

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

Equations

• CategoryTheory.Limits.preservesLimitsOfShapeUnop J F = { preservesLimit := fun {K : CategoryTheory.Functor J C} => CategoryTheory.Limits.preservesLimitUnop K F }

def CategoryTheory.Limits.preservesColimitsOfShapeOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfShape Jᵒᵖ F] : CategoryTheory.Limits.PreservesColimitsOfShape J F.op

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

Equations

• CategoryTheory.Limits.preservesColimitsOfShapeOp J F = { preservesColimit := fun {K : CategoryTheory.Functor J Cᵒᵖ} => CategoryTheory.Limits.preservesColimitOp K F }

def CategoryTheory.Limits.preservesColimitsOfShapeLeftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesLimitsOfShape Jᵒᵖ F] : CategoryTheory.Limits.PreservesColimitsOfShape J F.leftOp

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

Equations

• CategoryTheory.Limits.preservesColimitsOfShapeLeftOp J F = { preservesColimit := fun {K : CategoryTheory.Functor J Cᵒᵖ} => CategoryTheory.Limits.preservesColimitLeftOp K F }

def CategoryTheory.Limits.preservesColimitsOfShapeRightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesLimitsOfShape Jᵒᵖ F] : CategoryTheory.Limits.PreservesColimitsOfShape J F.rightOp

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

Equations

• CategoryTheory.Limits.preservesColimitsOfShapeRightOp J F = { preservesColimit := fun {K : CategoryTheory.Functor J C} => CategoryTheory.Limits.preservesColimitRightOp K F }

def CategoryTheory.Limits.preservesColimitsOfShapeUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : Type w) [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesLimitsOfShape Jᵒᵖ F] : CategoryTheory.Limits.PreservesColimitsOfShape J F.unop

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

Equations

• CategoryTheory.Limits.preservesColimitsOfShapeUnop J F = { preservesColimit := fun {K : CategoryTheory.Functor J C} => CategoryTheory.Limits.preservesColimitUnop K F }

def CategoryTheory.Limits.preservesLimitsOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimits F] : CategoryTheory.Limits.PreservesLimits F.op

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesLimitsLeftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesColimits F] : CategoryTheory.Limits.PreservesLimits F.leftOp

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesLimitsRightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesColimits F] : CategoryTheory.Limits.PreservesLimits F.rightOp

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesLimitsUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesColimits F] : CategoryTheory.Limits.PreservesLimits F.unop

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.perservesColimitsOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimits F] : CategoryTheory.Limits.PreservesColimits F.op

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesColimitsLeftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesLimits F] : CategoryTheory.Limits.PreservesColimits F.leftOp

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesColimitsRightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesLimits F] : CategoryTheory.Limits.PreservesColimits F.rightOp

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesColimitsUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesLimits F] : CategoryTheory.Limits.PreservesColimits F.unop

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesFiniteLimitsOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Limits.PreservesFiniteLimits F.op

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesFiniteLimitsLeftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Limits.PreservesFiniteLimits F.leftOp

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesFiniteLimitsRightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Limits.PreservesFiniteLimits F.rightOp

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesFiniteLimitsUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteColimits F] : CategoryTheory.Limits.PreservesFiniteLimits F.unop

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesFiniteColimitsOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.Limits.PreservesFiniteColimits F.op

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesFiniteColimitsLeftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.Limits.PreservesFiniteColimits F.leftOp

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesFiniteColimitsRightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.Limits.PreservesFiniteColimits F.rightOp

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.preservesFiniteColimitsUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteLimits F] : CategoryTheory.Limits.PreservesFiniteColimits F.unop

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

Equations

• One or more equations did not get rendered due to their size.