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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J Cᵒᵖ) (F : Functor C D) [PreservesColimit K.leftOp F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C D) [PreservesColimit K.op F.op] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J Cᵒᵖ) (F : Functor C Dᵒᵖ) [PreservesColimit K.leftOp F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C Dᵒᵖ) [PreservesColimit K.op F.leftOp] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor Cᵒᵖ D) [PreservesColimit K.op F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J Cᵒᵖ) (F : Functor Cᵒᵖ D) [PreservesColimit K.leftOp F.rightOp] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesColimit K.op F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J Cᵒᵖ) (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesColimit K.leftOp F.unop] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J Cᵒᵖ) (F : Functor C D) [PreservesLimit K.leftOp F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C D) [PreservesLimit K.op F.op] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J Cᵒᵖ) (F : Functor C Dᵒᵖ) [PreservesLimit K.leftOp F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C Dᵒᵖ) [PreservesLimit K.op F.leftOp] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor Cᵒᵖ D) [PreservesLimit K.op F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J Cᵒᵖ) (F : Functor Cᵒᵖ D) [PreservesLimit K.leftOp F.rightOp] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesLimit K.op F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J Cᵒᵖ) (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesLimit K.leftOp F.unop] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor C D) [PreservesColimitsOfShape Jᵒᵖ F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor C Dᵒᵖ) [PreservesColimitsOfShape Jᵒᵖ F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor Cᵒᵖ D) [PreservesColimitsOfShape Jᵒᵖ F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesColimitsOfShape Jᵒᵖ F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor C D) [PreservesLimitsOfShape Jᵒᵖ F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor C Dᵒᵖ) [PreservesLimitsOfShape Jᵒᵖ F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor Cᵒᵖ D) [PreservesLimitsOfShape Jᵒᵖ F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesLimitsOfShape Jᵒᵖ F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor C D) [PreservesColimitsOfShape Jᵒᵖ F.op] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor C Dᵒᵖ) [PreservesColimitsOfShape Jᵒᵖ F.leftOp] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor Cᵒᵖ D) [PreservesColimitsOfShape Jᵒᵖ F.rightOp] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesColimitsOfShape Jᵒᵖ F.unop] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor C D) [PreservesLimitsOfShape Jᵒᵖ F.op] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor C Dᵒᵖ) [PreservesLimitsOfShape Jᵒᵖ F.leftOp] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor Cᵒᵖ D) [PreservesLimitsOfShape Jᵒᵖ F.rightOp] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesLimitsOfShape Jᵒᵖ F.unop] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.rightOp] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesColimits F] : PreservesLimits F.op

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem CategoryTheory.Limits.preservesColimits_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesLimits F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesColimits F.op] : PreservesLimits F

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem CategoryTheory.Limits.preservesFiniteLimits_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesFiniteColimits F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [PreservesFiniteColimits F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [PreservesFiniteColimits F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesFiniteColimits F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesFiniteLimits F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [PreservesFiniteLimits F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [PreservesFiniteLimits F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesFiniteLimits F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesFiniteColimits F.op] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [PreservesFiniteColimits F.leftOp] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [PreservesFiniteColimits F.rightOp] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesFiniteColimits F.unop] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesFiniteLimits F.op] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [PreservesFiniteLimits F.leftOp] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [PreservesFiniteLimits F.rightOp] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesFiniteLimits F.unop] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesFiniteCoproducts F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [PreservesFiniteCoproducts F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [PreservesFiniteCoproducts F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesFiniteCoproducts F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [PreservesFiniteProducts F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [PreservesFiniteProducts F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [PreservesFiniteProducts F] : 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [PreservesFiniteProducts F] : PreservesFiniteCoproducts F.unop

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

theorem CategoryTheory.Limits.reflectsLimit_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J Cᵒᵖ) (F : Functor C D) [ReflectsColimit K.leftOp F] : ReflectsLimit K F.op

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

theorem CategoryTheory.Limits.reflectsLimit_of_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C D) [ReflectsColimit K.op F.op] : ReflectsLimit K F

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

theorem CategoryTheory.Limits.reflectsLimit_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J Cᵒᵖ) (F : Functor C Dᵒᵖ) [ReflectsColimit K.leftOp F] : ReflectsLimit K F.leftOp

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

theorem CategoryTheory.Limits.reflectsLimit_of_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C Dᵒᵖ) [ReflectsColimit K.op F.leftOp] : ReflectsLimit K F

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

theorem CategoryTheory.Limits.reflectsLimit_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor Cᵒᵖ D) [ReflectsColimit K.op F] : ReflectsLimit K F.rightOp

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

theorem CategoryTheory.Limits.reflectsLimit_of_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J Cᵒᵖ) (F : Functor Cᵒᵖ D) [ReflectsColimit K.leftOp F.rightOp] : ReflectsLimit K F

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

theorem CategoryTheory.Limits.reflectsLimit_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor Cᵒᵖ Dᵒᵖ) [ReflectsColimit K.op F] : ReflectsLimit K F.unop

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

theorem CategoryTheory.Limits.reflectsLimit_of_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J Cᵒᵖ) (F : Functor Cᵒᵖ Dᵒᵖ) [ReflectsColimit K.leftOp F.unop] : ReflectsLimit K F

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

theorem CategoryTheory.Limits.reflectsColimit_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J Cᵒᵖ) (F : Functor C D) [ReflectsLimit K.leftOp F] : ReflectsColimit K F.op

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

theorem CategoryTheory.Limits.reflectsColimit_of_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C D) [ReflectsLimit K.op F.op] : ReflectsColimit K F

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

theorem CategoryTheory.Limits.reflectsColimit_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J Cᵒᵖ) (F : Functor C Dᵒᵖ) [ReflectsLimit K.leftOp F] : ReflectsColimit K F.leftOp

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

theorem CategoryTheory.Limits.reflectsColimit_of_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor C Dᵒᵖ) [ReflectsLimit K.op F.leftOp] : ReflectsColimit K F

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

theorem CategoryTheory.Limits.reflectsColimit_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor Cᵒᵖ D) [ReflectsLimit K.op F] : ReflectsColimit K F.rightOp

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

theorem CategoryTheory.Limits.reflectsColimit_of_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J Cᵒᵖ) (F : Functor Cᵒᵖ D) [ReflectsLimit K.leftOp F.rightOp] : ReflectsColimit K F

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

theorem CategoryTheory.Limits.reflectsColimit_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J C) (F : Functor Cᵒᵖ Dᵒᵖ) [ReflectsLimit K.op F] : ReflectsColimit K F.unop

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

theorem CategoryTheory.Limits.reflectsColimit_of_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {J : Type w} [Category.{w', w} J] (K : Functor J Cᵒᵖ) (F : Functor Cᵒᵖ Dᵒᵖ) [ReflectsLimit K.leftOp F.unop] : ReflectsColimit K F

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

theorem CategoryTheory.Limits.reflectsLimitsOfShape_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor C D) [ReflectsColimitsOfShape Jᵒᵖ F] : ReflectsLimitsOfShape J F.op

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

theorem CategoryTheory.Limits.reflectsLimitsOfShape_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor C Dᵒᵖ) [ReflectsColimitsOfShape Jᵒᵖ F] : ReflectsLimitsOfShape J F.leftOp

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

theorem CategoryTheory.Limits.reflectsLimitsOfShape_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor Cᵒᵖ D) [ReflectsColimitsOfShape Jᵒᵖ F] : ReflectsLimitsOfShape J F.rightOp

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

theorem CategoryTheory.Limits.reflectsLimitsOfShape_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor Cᵒᵖ Dᵒᵖ) [ReflectsColimitsOfShape Jᵒᵖ F] : ReflectsLimitsOfShape J F.unop

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

theorem CategoryTheory.Limits.reflectsColimitsOfShape_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor C D) [ReflectsLimitsOfShape Jᵒᵖ F] : ReflectsColimitsOfShape J F.op

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

theorem CategoryTheory.Limits.reflectsColimitsOfShape_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor C Dᵒᵖ) [ReflectsLimitsOfShape Jᵒᵖ F] : ReflectsColimitsOfShape J F.leftOp

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

theorem CategoryTheory.Limits.reflectsColimitsOfShape_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor Cᵒᵖ D) [ReflectsLimitsOfShape Jᵒᵖ F] : ReflectsColimitsOfShape J F.rightOp

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

theorem CategoryTheory.Limits.reflectsColimitsOfShape_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor Cᵒᵖ Dᵒᵖ) [ReflectsLimitsOfShape Jᵒᵖ F] : ReflectsColimitsOfShape J F.unop

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

theorem CategoryTheory.Limits.reflectsLimitsOfShape_of_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor C D) [ReflectsColimitsOfShape Jᵒᵖ F.op] : ReflectsLimitsOfShape J F

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

theorem CategoryTheory.Limits.reflectsLimitsOfShape_of_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor C Dᵒᵖ) [ReflectsColimitsOfShape Jᵒᵖ F.leftOp] : ReflectsLimitsOfShape J F

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

theorem CategoryTheory.Limits.reflectsLimitsOfShape_of_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor Cᵒᵖ D) [ReflectsColimitsOfShape Jᵒᵖ F.rightOp] : ReflectsLimitsOfShape J F

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

theorem CategoryTheory.Limits.reflectsLimitsOfShape_of_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor Cᵒᵖ Dᵒᵖ) [ReflectsColimitsOfShape Jᵒᵖ F.unop] : ReflectsLimitsOfShape J F

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

theorem CategoryTheory.Limits.reflectsColimitsOfShape_of_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor C D) [ReflectsLimitsOfShape Jᵒᵖ F.op] : ReflectsColimitsOfShape J F

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

theorem CategoryTheory.Limits.reflectsColimitsOfShape_of_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor C Dᵒᵖ) [ReflectsLimitsOfShape Jᵒᵖ F.leftOp] : ReflectsColimitsOfShape J F

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

theorem CategoryTheory.Limits.reflectsColimitsOfShape_of_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor Cᵒᵖ D) [ReflectsLimitsOfShape Jᵒᵖ F.rightOp] : ReflectsColimitsOfShape J F

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

theorem CategoryTheory.Limits.reflectsColimitsOfShape_of_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (J : Type w) [Category.{w', w} J] (F : Functor Cᵒᵖ Dᵒᵖ) [ReflectsLimitsOfShape Jᵒᵖ F.unop] : ReflectsColimitsOfShape J F

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem CategoryTheory.Limits.reflectsLimits_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsColimits F] : ReflectsLimits F.op

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

theorem CategoryTheory.Limits.reflectsLimits_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [ReflectsColimits F] : ReflectsLimits F.leftOp

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

theorem CategoryTheory.Limits.reflectsLimits_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [ReflectsColimits F] : ReflectsLimits F.rightOp

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

theorem CategoryTheory.Limits.reflectsLimits_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [ReflectsColimits F] : ReflectsLimits F.unop

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

theorem CategoryTheory.Limits.reflectsColimits_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsLimits F] : ReflectsColimits F.op

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

theorem CategoryTheory.Limits.reflectsColimits_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [ReflectsLimits F] : ReflectsColimits F.leftOp

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

theorem CategoryTheory.Limits.reflectsColimits_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [ReflectsLimits F] : ReflectsColimits F.rightOp

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

theorem CategoryTheory.Limits.reflectsColimits_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [ReflectsLimits F] : ReflectsColimits F.unop

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

theorem CategoryTheory.Limits.reflectsLimits_of_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsColimits F.op] : ReflectsLimits F

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

theorem CategoryTheory.Limits.reflectsLimits_of_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [ReflectsColimits F.leftOp] : ReflectsLimits F

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

theorem CategoryTheory.Limits.reflectsLimits_of_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [ReflectsColimits F.rightOp] : ReflectsLimits F

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

theorem CategoryTheory.Limits.reflectsLimits_of_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [ReflectsColimits F.unop] : ReflectsLimits F

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

theorem CategoryTheory.Limits.reflectsColimits_of_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsLimits F.op] : ReflectsColimits F

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

theorem CategoryTheory.Limits.reflectsColimits_of_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [ReflectsLimits F.leftOp] : ReflectsColimits F

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

theorem CategoryTheory.Limits.reflectsColimits_of_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [ReflectsLimits F.rightOp] : ReflectsColimits F

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

theorem CategoryTheory.Limits.reflectsColimits_of_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [ReflectsLimits F.unop] : ReflectsColimits F

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

theorem CategoryTheory.Limits.reflectsFiniteLimits_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsFiniteColimits F] : ReflectsFiniteLimits F.op

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

theorem CategoryTheory.Limits.reflectsFiniteLimits_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [ReflectsFiniteColimits F] : ReflectsFiniteLimits F.leftOp

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

theorem CategoryTheory.Limits.reflectsFiniteLimits_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [ReflectsFiniteColimits F] : ReflectsFiniteLimits F.rightOp

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

theorem CategoryTheory.Limits.reflectsFiniteLimits_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [ReflectsFiniteColimits F] : ReflectsFiniteLimits F.unop

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

theorem CategoryTheory.Limits.reflectsFiniteColimits_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsFiniteLimits F] : ReflectsFiniteColimits F.op

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

theorem CategoryTheory.Limits.reflectsFiniteColimits_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [ReflectsFiniteLimits F] : ReflectsFiniteColimits F.leftOp

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

theorem CategoryTheory.Limits.reflectsFiniteColimits_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [ReflectsFiniteLimits F] : ReflectsFiniteColimits F.rightOp

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

theorem CategoryTheory.Limits.reflectsFiniteColimits_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [ReflectsFiniteLimits F] : ReflectsFiniteColimits F.unop

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

theorem CategoryTheory.Limits.reflectsFiniteLimits_of_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsFiniteColimits F.op] : ReflectsFiniteLimits F

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

theorem CategoryTheory.Limits.reflectsFiniteLimits_of_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [ReflectsFiniteColimits F.leftOp] : ReflectsFiniteLimits F

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

theorem CategoryTheory.Limits.reflectsFiniteLimits_of_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [ReflectsFiniteColimits F.rightOp] : ReflectsFiniteLimits F

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

theorem CategoryTheory.Limits.reflectsFiniteLimits_of_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [ReflectsFiniteColimits F.unop] : ReflectsFiniteLimits F

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

theorem CategoryTheory.Limits.reflectsFiniteColimits_of_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsFiniteLimits F.op] : ReflectsFiniteColimits F

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

theorem CategoryTheory.Limits.reflectsFiniteColimits_of_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [ReflectsFiniteLimits F.leftOp] : ReflectsFiniteColimits F

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

theorem CategoryTheory.Limits.reflectsFiniteColimits_of_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [ReflectsFiniteLimits F.rightOp] : ReflectsFiniteColimits F

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

theorem CategoryTheory.Limits.reflectsFiniteColimits_of_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [ReflectsFiniteLimits F.unop] : ReflectsFiniteColimits F

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

theorem CategoryTheory.Limits.reflectsFiniteProducts_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsFiniteCoproducts F] : ReflectsFiniteProducts F.op

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

theorem CategoryTheory.Limits.reflectsFiniteProducts_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [ReflectsFiniteCoproducts F] : ReflectsFiniteProducts F.leftOp

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

theorem CategoryTheory.Limits.reflectsFiniteProducts_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [ReflectsFiniteCoproducts F] : ReflectsFiniteProducts F.rightOp

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

theorem CategoryTheory.Limits.reflectsFiniteProducts_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [ReflectsFiniteCoproducts F] : ReflectsFiniteProducts F.unop

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

theorem CategoryTheory.Limits.reflectsFiniteCoproducts_op {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [ReflectsFiniteProducts F] : ReflectsFiniteCoproducts F.op

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

theorem CategoryTheory.Limits.reflectsFiniteCoproducts_leftOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C Dᵒᵖ) [ReflectsFiniteProducts F] : ReflectsFiniteCoproducts F.leftOp

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

theorem CategoryTheory.Limits.reflectsFiniteCoproducts_rightOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ D) [ReflectsFiniteProducts F] : ReflectsFiniteCoproducts F.rightOp

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

theorem CategoryTheory.Limits.reflectsFiniteCoproducts_unop {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor Cᵒᵖ Dᵒᵖ) [ReflectsFiniteProducts F] : ReflectsFiniteCoproducts F.unop

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