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 and vice versa.

theorem CategoryTheory.Limits.preservesLimit_op {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ᵒᵖ.

theorem CategoryTheory.Limits.preservesLimit_of_op {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.op] : CategoryTheory.Limits.PreservesLimit K F

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

theorem CategoryTheory.Limits.preservesLimit_leftOp {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ᵒᵖ.

theorem CategoryTheory.Limits.preservesLimit_of_leftOp {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.leftOp] : CategoryTheory.Limits.PreservesLimit K F

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

theorem CategoryTheory.Limits.preservesLimit_rightOp {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.

theorem CategoryTheory.Limits.preservesLimit_of_rightOp {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.rightOp] : CategoryTheory.Limits.PreservesLimit K F

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

theorem CategoryTheory.Limits.preservesLimit_unop {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.

theorem CategoryTheory.Limits.preservesLimit_of_unop {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.unop] : CategoryTheory.Limits.PreservesLimit K F

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

theorem CategoryTheory.Limits.preservesColimit_op {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ᵒᵖ.

theorem CategoryTheory.Limits.preservesColimit_of_op {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.op] : CategoryTheory.Limits.PreservesColimit K F

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

theorem CategoryTheory.Limits.preservesColimit_leftOp {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ᵒᵖ.

theorem CategoryTheory.Limits.preservesColimit_of_leftOp {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.leftOp] : CategoryTheory.Limits.PreservesColimit K F

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

theorem CategoryTheory.Limits.preservesColimit_rightOp {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.

theorem CategoryTheory.Limits.preservesColimit_of_rightOp {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.rightOp] : CategoryTheory.Limits.PreservesColimit K F

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

theorem CategoryTheory.Limits.preservesColimit_unop {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.

theorem CategoryTheory.Limits.preservesColimit_of_unop {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.unop] : CategoryTheory.Limits.PreservesColimit K F

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

theorem CategoryTheory.Limits.preservesLimitsOfShape_op {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.

theorem CategoryTheory.Limits.preservesLimitsOfShape_leftOp {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.

theorem CategoryTheory.Limits.preservesLimitsOfShape_rightOp {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.

theorem CategoryTheory.Limits.preservesLimitsOfShape_unop {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.

theorem CategoryTheory.Limits.preservesColimitsOfShape_op {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.

theorem CategoryTheory.Limits.preservesColimitsOfShape_leftOp {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.

theorem CategoryTheory.Limits.preservesColimitsOfShape_rightOp {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.

theorem CategoryTheory.Limits.preservesColimitsOfShape_unop {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.

theorem CategoryTheory.Limits.preservesLimitsOfShape_of_op {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.op] : CategoryTheory.Limits.PreservesLimitsOfShape J F

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

theorem CategoryTheory.Limits.preservesLimitsOfShape_of_leftOp {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.leftOp] : CategoryTheory.Limits.PreservesLimitsOfShape J F

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

theorem CategoryTheory.Limits.preservesLimitsOfShape_of_rightOp {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.rightOp] : CategoryTheory.Limits.PreservesLimitsOfShape J F

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

theorem CategoryTheory.Limits.preservesLimitsOfShape_of_unop {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.unop] : CategoryTheory.Limits.PreservesLimitsOfShape J F

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

theorem CategoryTheory.Limits.preservesColimitsOfShape_of_op {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.op] : CategoryTheory.Limits.PreservesColimitsOfShape J F

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

theorem CategoryTheory.Limits.preservesColimitsOfShape_of_leftOp {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.leftOp] : CategoryTheory.Limits.PreservesColimitsOfShape J F

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

theorem CategoryTheory.Limits.preservesColimitsOfShape_of_rightOp {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.rightOp] : CategoryTheory.Limits.PreservesColimitsOfShape J F

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

theorem CategoryTheory.Limits.preservesColimitsOfShape_of_unop {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.unop] : CategoryTheory.Limits.PreservesColimitsOfShape J F

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

theorem CategoryTheory.Limits.preservesLimitsOfSize_op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op

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

theorem CategoryTheory.Limits.preservesLimitsOfSize_leftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp

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

theorem CategoryTheory.Limits.preservesLimitsOfSize_rightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp

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

theorem CategoryTheory.Limits.preservesLimitsOfSize_unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop

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

theorem CategoryTheory.Limits.preservesColimitsOfSize_op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op

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

theorem CategoryTheory.Limits.preservesColimitsOfSize_leftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp

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

theorem CategoryTheory.Limits.preservesColimitsOfSize_rightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp

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

theorem CategoryTheory.Limits.preservesColimitsOfSize_unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop

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

theorem CategoryTheory.Limits.preservesLimitsOfSize_of_op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

theorem CategoryTheory.Limits.preservesLimitsOfSize_of_leftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

theorem CategoryTheory.Limits.preservesLimitsOfSize_of_rightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

theorem CategoryTheory.Limits.preservesLimitsOfSize_of_unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop] : CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

theorem CategoryTheory.Limits.preservesColimitsOfSize_of_op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op] : CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

theorem CategoryTheory.Limits.preservesColimitsOfSize_of_leftOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp] : CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

theorem CategoryTheory.Limits.preservesColimitsOfSize_of_rightOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp] : CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

theorem CategoryTheory.Limits.preservesColimitsOfSize_of_unop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop] : CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

theorem CategoryTheory.Limits.preservesLimits_op {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.

theorem CategoryTheory.Limits.preservesLimits_leftOp {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.

theorem CategoryTheory.Limits.preservesLimits_rightOp {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.

theorem CategoryTheory.Limits.preservesLimits_unop {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.

theorem CategoryTheory.Limits.perservesColimits_op {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.

theorem CategoryTheory.Limits.preservesColimits_leftOp {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.

theorem CategoryTheory.Limits.preservesColimits_rightOp {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.

theorem CategoryTheory.Limits.preservesColimits_unop {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.

theorem CategoryTheory.Limits.preservesLimits_of_op {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.op] : CategoryTheory.Limits.PreservesLimits F

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

theorem CategoryTheory.Limits.preservesLimits_of_leftOp {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.leftOp] : CategoryTheory.Limits.PreservesLimits F

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

theorem CategoryTheory.Limits.preservesLimits_of_rightOp {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.rightOp] : CategoryTheory.Limits.PreservesLimits F

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

theorem CategoryTheory.Limits.preservesLimits_of_unop {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.unop] : CategoryTheory.Limits.PreservesLimits F

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

theorem CategoryTheory.Limits.preservesColimits_of_op {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.op] : CategoryTheory.Limits.PreservesColimits F

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

theorem CategoryTheory.Limits.preservesColimits_of_leftOp {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.leftOp] : CategoryTheory.Limits.PreservesColimits F

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

theorem CategoryTheory.Limits.preservesColimits_of_rightOp {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.rightOp] : CategoryTheory.Limits.PreservesColimits F

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

theorem CategoryTheory.Limits.preservesColimits_of_unop {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.unop] : CategoryTheory.Limits.PreservesColimits F

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

theorem CategoryTheory.Limits.preservesFiniteLimits_op {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.

theorem CategoryTheory.Limits.preservesFiniteLimits_leftOp {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.

theorem CategoryTheory.Limits.preservesFiniteLimits_rightOp {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.

theorem CategoryTheory.Limits.preservesFiniteLimits_unop {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.

theorem CategoryTheory.Limits.preservesFiniteColimits_op {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.

theorem CategoryTheory.Limits.preservesFiniteColimits_leftOp {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.

theorem CategoryTheory.Limits.preservesFiniteColimits_rightOp {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.

theorem CategoryTheory.Limits.preservesFiniteColimits_unop {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.

theorem CategoryTheory.Limits.preservesFiniteLimits_of_op {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.op] : CategoryTheory.Limits.PreservesFiniteLimits F

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

theorem CategoryTheory.Limits.preservesFiniteLimits_of_leftOp {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.leftOp] : CategoryTheory.Limits.PreservesFiniteLimits F

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

theorem CategoryTheory.Limits.preservesFiniteLimits_of_rightOp {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.rightOp] : CategoryTheory.Limits.PreservesFiniteLimits F

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

theorem CategoryTheory.Limits.preservesFiniteLimits_of_unop {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.unop] : CategoryTheory.Limits.PreservesFiniteLimits F

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

theorem CategoryTheory.Limits.preservesFiniteColimits_of_op {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.op] : CategoryTheory.Limits.PreservesFiniteColimits F

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

theorem CategoryTheory.Limits.preservesFiniteColimits_of_leftOp {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.leftOp] : CategoryTheory.Limits.PreservesFiniteColimits F

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

theorem CategoryTheory.Limits.preservesFiniteColimits_of_rightOp {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.rightOp] : CategoryTheory.Limits.PreservesFiniteColimits F

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

theorem CategoryTheory.Limits.preservesFiniteColimits_of_unop {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.unop] : CategoryTheory.Limits.PreservesFiniteColimits F

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

theorem CategoryTheory.Limits.preservesFiniteProducts_op {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.

theorem CategoryTheory.Limits.preservesFiniteProducts_leftOp {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.

theorem CategoryTheory.Limits.preservesFiniteProducts_rightOp {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.

theorem CategoryTheory.Limits.preservesFiniteProducts_unop {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.

theorem CategoryTheory.Limits.preservesFiniteCoproducts_op {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.

theorem CategoryTheory.Limits.preservesFiniteCoproducts_leftOp {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.

theorem CategoryTheory.Limits.preservesFiniteCoproducts_rightOp {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.

theorem CategoryTheory.Limits.preservesFiniteCoproducts_unop {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.