Limit preservation properties of Functor.op and related constructions

We formulate conditions about F which imply that F.op, F.unop, F.leftOp and F.rightOp 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.leftOp : 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.leftOp : Jᵒᵖ ⥤ C, then F.leftOp : 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.rightOp : 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.leftOp : 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.leftOp : Jᵒᵖ ⥤ C, then F.leftOp : 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.rightOp : 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.leftOp : 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.rightOp : 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.leftOp : 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.rightOp : 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.leftOp : 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.rightOp : 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.leftOp : 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.rightOp : 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.leftOp : 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.rightOp : 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.leftOp : 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.rightOp : 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.

def CategoryTheory.Limits.preservesFiniteProductsOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteCoproducts F] : CategoryTheory.Limits.PreservesFiniteProducts F.op

If F : C ⥤ D preserves finite coproducts, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves finite products.

Equations

• CategoryTheory.Limits.preservesFiniteProductsOp F = { preserves := fun (J : Type) (x : Fintype J) => CategoryTheory.Limits.preservesLimitsOfShapeOp (CategoryTheory.Discrete J) F }

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

If F : C ⥤ Dᵒᵖ preserves finite coproducts, then F.leftOp : Cᵒᵖ ⥤ D preserves finite products.

Equations

• CategoryTheory.Limits.preservesFiniteProductsLeftOp F = { preserves := fun (J : Type) (x : Fintype J) => CategoryTheory.Limits.preservesLimitsOfShapeLeftOp (CategoryTheory.Discrete J) F }

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

If F : Cᵒᵖ ⥤ D preserves finite coproducts, then F.rightOp : C ⥤ Dᵒᵖ preserves finite products.

Equations

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

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

If F : Cᵒᵖ ⥤ Dᵒᵖ preserves finite coproducts, then F.unop : C ⥤ D preserves finite products.

Equations

• CategoryTheory.Limits.preservesFiniteProductsUnop F = { preserves := fun (J : Type) (x : Fintype J) => CategoryTheory.Limits.preservesLimitsOfShapeUnop (CategoryTheory.Discrete J) F }

def CategoryTheory.Limits.preservesFiniteCoproductsOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteProducts F] : CategoryTheory.Limits.PreservesFiniteCoproducts F.op

If F : C ⥤ D preserves finite products, then F.op : Cᵒᵖ ⥤ Dᵒᵖ preserves finite coproducts.

Equations

• CategoryTheory.Limits.preservesFiniteCoproductsOp F = { preserves := fun (J : Type) (x : Fintype J) => CategoryTheory.Limits.preservesColimitsOfShapeOp (CategoryTheory.Discrete J) F }

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

If F : C ⥤ Dᵒᵖ preserves finite products, then F.leftOp : Cᵒᵖ ⥤ D preserves finite coproducts.

Equations

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

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

If F : Cᵒᵖ ⥤ D preserves finite products, then F.rightOp : C ⥤ Dᵒᵖ preserves finite coproducts.

Equations

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

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

If F : Cᵒᵖ ⥤ Dᵒᵖ preserves finite products, then F.unop : C ⥤ D preserves finite coproducts.

Equations

• CategoryTheory.Limits.preservesFiniteCoproductsUnop F = { preserves := fun (J : Type) (x : Fintype J) => CategoryTheory.Limits.preservesColimitsOfShapeUnop (CategoryTheory.Discrete J) F }